18 rstar2 "$G |R> $H ==> P, $G |R> $H" |
18 rstar2 "$G |R> $H ==> P, $G |R> $H" |
19 |
19 |
20 (* Rules for [] and <> *) |
20 (* Rules for [] and <> *) |
21 |
21 |
22 boxR |
22 boxR |
23 "[| $E |L> $E'; $F |R> $F'; $G |R> $G'; \ |
23 "[| $E |L> $E'; $F |R> $F'; $G |R> $G'; |
24 \ $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G" |
24 $E' |- $F', P, $G'|] ==> $E |- $F, []P, $G" |
25 boxL "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G" |
25 boxL "$E,P,$F,[]P |- $G ==> $E, []P, $F |- $G" |
26 |
26 |
27 diaR "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" |
27 diaR "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" |
28 diaL |
28 diaL |
29 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; \ |
29 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; |
30 \ $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G" |
30 $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G" |
31 end |
31 end |