src/Modal/ex/S43thms.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
Initial revision
     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";