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 diaR "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" |
27 diaR "$E |- $F,P,$G,<>P ==> $E |- $F, <>P, $G" |
27 diaL |
28 diaL |
28 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; \ |
29 "[| $E |L> $E'; $F |L> $F'; $G |R> $G'; \ |
29 \ $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G" |
30 \ $E', P, $F' |- $G'|] ==> $E, <>P, $F |- $G" |
30 end |
31 end |