Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Sequents/Modal/S43thms.ML
author wenzelm
Sat, 03 Feb 2001 15:22:57 +0100
changeset 11045 971a50fda146
parent 6252 935f183bf406
permissions -rw-r--r--
fixed syntax of 'split_format';
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6252
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset 
     1
 
(*  Title:      91/Modal/ex/S43thms
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset 
     2
 
    ID:         $Id$
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset 
     3
 
    Author:     Martin Coen
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset 
     4
 
    Copyright   1991  University of Cambridge
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset 
     5
 
*)
935f183bf406 examples made separate dirs;
wenzelm
parents:
diff changeset 
     6
 












935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




     7


(* Theorems of system S43 *)













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




     8














935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




     9


try "|- <>[]P --> []<>P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    10


try "|- <>[]P --> [][]<>P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    11


try "|- [](<>P | <>Q) --> []<>P | []<>Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    12


try "|- <>[]P & <>[]Q --> <>([]P & []Q)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    13


try "|- []([]P --> []Q) | []([]Q --> []P)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    14


try "|- [](<>P --> <>Q) | [](<>Q --> <>P)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    15


try "|- []([]P --> Q) | []([]Q --> P)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    16


try "|- [](P --> <>Q) | [](Q --> <>P)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    17


try "|- [](P --> []Q-->R) | [](P | ([]R --> Q))";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    18


try "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    19


try "|- []([]P | Q) & [](P | []Q) --> []P | []Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    20


try "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    21


try "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    22


try "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    23


try "|- <>[]<>P <-> []<>P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    24


try "|- []<>[]P <-> <>[]P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    25














935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    26


(* These are from Hailpern, LNCS 129 *)













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    27














935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    28


try "|- [](P & Q) <-> []P & []Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    29


try "|- <>(P | Q) <-> <>P | <>Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    30


try "|- <>(P --> Q) <-> []P --> <>Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    31














935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    32


try "|- [](P --> Q) --> <>P --> <>Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    33


try "|- []P --> []<>P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    34


try "|- <>[]P --> <>P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    35


try "|- []<>[]P --> []<>P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    36


try "|- <>[]P --> <>[]<>P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    37


try "|- <>[]P --> []<>P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    38


try "|- []<>[]P <-> <>[]P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    39


try "|- <>[]<>P <-> []<>P";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    40














935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    41


try "|- []P | []Q --> [](P | Q)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    42


try "|- <>(P & Q) --> <>P & <>Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    43


try "|- [](P | Q) --> []P | <>Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    44


try "|- <>P & []Q --> <>(P & Q)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    45


try "|- [](P | Q) --> <>P | []Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    46


try "|- [](P | Q) --> []<>P | []<>Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    47


try "|- <>[]P & <>[]Q --> <>(P & Q)";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    48


try "|- <>[](P & Q) <-> <>[]P & <>[]Q";













935f183bf406
examples made separate dirs;



wenzelm


parents: 

diff
changeset




    49


try "|- []<>(P | Q) <-> []<>P | []<>Q";















isabelle