src/Sequents/Modal/S43thms.ML

--- a/src/Sequents/Modal/S43thms.ML	Mon Nov 20 21:23:12 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,49 +0,0 @@
-(*  Title:      91/Modal/ex/S43thms
-    ID:         $Id$
-    Author:     Martin Coen
-    Copyright   1991  University of Cambridge
-*)
-
-(* Theorems of system S43 *)
-
-try "|- <>[]P --> []<>P";
-try "|- <>[]P --> [][]<>P";
-try "|- [](<>P | <>Q) --> []<>P | []<>Q";
-try "|- <>[]P & <>[]Q --> <>([]P & []Q)";
-try "|- []([]P --> []Q) | []([]Q --> []P)";
-try "|- [](<>P --> <>Q) | [](<>Q --> <>P)";
-try "|- []([]P --> Q) | []([]Q --> P)";
-try "|- [](P --> <>Q) | [](Q --> <>P)";
-try "|- [](P --> []Q-->R) | [](P | ([]R --> Q))";
-try "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)";
-try "|- []([]P | Q) & [](P | []Q) --> []P | []Q";
-try "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)";
-try "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q";
-try "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)";
-try "|- <>[]<>P <-> []<>P";
-try "|- []<>[]P <-> <>[]P";
-
-(* These are from Hailpern, LNCS 129 *)
-
-try "|- [](P & Q) <-> []P & []Q";
-try "|- <>(P | Q) <-> <>P | <>Q";
-try "|- <>(P --> Q) <-> []P --> <>Q";
-
-try "|- [](P --> Q) --> <>P --> <>Q";
-try "|- []P --> []<>P";
-try "|- <>[]P --> <>P";
-try "|- []<>[]P --> []<>P";
-try "|- <>[]P --> <>[]<>P";
-try "|- <>[]P --> []<>P";
-try "|- []<>[]P <-> <>[]P";
-try "|- <>[]<>P <-> []<>P";
-
-try "|- []P | []Q --> [](P | Q)";
-try "|- <>(P & Q) --> <>P & <>Q";
-try "|- [](P | Q) --> []P | <>Q";
-try "|- <>P & []Q --> <>(P & Q)";
-try "|- [](P | Q) --> <>P | []Q";
-try "|- [](P | Q) --> []<>P | []<>Q";
-try "|- <>[]P & <>[]Q --> <>(P & Q)";
-try "|- <>[](P & Q) <-> <>[]P & <>[]Q";
-try "|- []<>(P | Q) <-> []<>P | []<>Q";