1 (* Title: 91/Modal/ex/S43thms |
|
2 ID: $Id$ |
|
3 Author: Martin Coen |
|
4 Copyright 1991 University of Cambridge |
|
5 *) |
|
6 |
|
7 (* Theorems of system S43 *) |
|
8 |
|
9 try "|- <>[]P --> []<>P"; |
|
10 try "|- <>[]P --> [][]<>P"; |
|
11 try "|- [](<>P | <>Q) --> []<>P | []<>Q"; |
|
12 try "|- <>[]P & <>[]Q --> <>([]P & []Q)"; |
|
13 try "|- []([]P --> []Q) | []([]Q --> []P)"; |
|
14 try "|- [](<>P --> <>Q) | [](<>Q --> <>P)"; |
|
15 try "|- []([]P --> Q) | []([]Q --> P)"; |
|
16 try "|- [](P --> <>Q) | [](Q --> <>P)"; |
|
17 try "|- [](P --> []Q-->R) | [](P | ([]R --> Q))"; |
|
18 try "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)"; |
|
19 try "|- []([]P | Q) & [](P | []Q) --> []P | []Q"; |
|
20 try "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)"; |
|
21 try "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q"; |
|
22 try "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)"; |
|
23 try "|- <>[]<>P <-> []<>P"; |
|
24 try "|- []<>[]P <-> <>[]P"; |
|
25 |
|
26 (* These are from Hailpern, LNCS 129 *) |
|
27 |
|
28 try "|- [](P & Q) <-> []P & []Q"; |
|
29 try "|- <>(P | Q) <-> <>P | <>Q"; |
|
30 try "|- <>(P --> Q) <-> []P --> <>Q"; |
|
31 |
|
32 try "|- [](P --> Q) --> <>P --> <>Q"; |
|
33 try "|- []P --> []<>P"; |
|
34 try "|- <>[]P --> <>P"; |
|
35 try "|- []<>[]P --> []<>P"; |
|
36 try "|- <>[]P --> <>[]<>P"; |
|
37 try "|- <>[]P --> []<>P"; |
|
38 try "|- []<>[]P <-> <>[]P"; |
|
39 try "|- <>[]<>P <-> []<>P"; |
|
40 |
|
41 try "|- []P | []Q --> [](P | Q)"; |
|
42 try "|- <>(P & Q) --> <>P & <>Q"; |
|
43 try "|- [](P | Q) --> []P | <>Q"; |
|
44 try "|- <>P & []Q --> <>(P & Q)"; |
|
45 try "|- [](P | Q) --> <>P | []Q"; |
|
46 try "|- [](P | Q) --> []<>P | []<>Q"; |
|
47 try "|- <>[]P & <>[]Q --> <>(P & Q)"; |
|
48 try "|- <>[](P & Q) <-> <>[]P & <>[]Q"; |
|
49 try "|- []<>(P | Q) <-> []<>P | []<>Q"; |
|