--- a/src/Sequents/S43.thy Thu Feb 28 14:10:54 2013 +0100
+++ b/src/Sequents/S43.thy Thu Feb 28 14:22:14 2013 +0100
@@ -32,17 +32,17 @@
in [(@{const_syntax S43pi}, s43pi_tr')] end
*}
-axioms
+axiomatization where
(* Definition of the star operation using a set of Horn clauses *)
(* For system S43: gamma * == {[]P | []P : gamma} *)
(* delta * == {<>P | <>P : delta} *)
- lstar0: "|L>"
- lstar1: "$G |L> $H ==> []P, $G |L> []P, $H"
- lstar2: "$G |L> $H ==> P, $G |L> $H"
- rstar0: "|R>"
- rstar1: "$G |R> $H ==> <>P, $G |R> <>P, $H"
- rstar2: "$G |R> $H ==> P, $G |R> $H"
+ lstar0: "|L>" and
+ lstar1: "$G |L> $H ==> []P, $G |L> []P, $H" and
+ lstar2: "$G |L> $H ==> P, $G |L> $H" and
+ rstar0: "|R>" and
+ rstar1: "$G |R> $H ==> <>P, $G |R> <>P, $H" and
+ rstar2: "$G |R> $H ==> P, $G |R> $H" and
(* Set of Horn clauses to generate the antecedents for the S43 pi rule *)
(* ie *)
@@ -54,22 +54,22 @@
(* and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj *)
(* and 1<=i<=k and k<j<=k+m *)
- S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia"
+ S43pi0: "S43pi $L;; $R;; $Lbox; $Rdia" and
S43pi1:
"[| (S43pi <>P,$L'; $L;; $R; $Lbox;$Rdia); $L',P,$L,$Lbox |- $R,$Rdia |] ==>
- S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia"
+ S43pi $L'; <>P,$L;; $R; $Lbox;$Rdia" and
S43pi2:
"[| (S43pi $L';; []P,$R'; $R; $Lbox;$Rdia); $L',$Lbox |- $R',P,$R,$Rdia |] ==>
- S43pi $L';; $R'; []P,$R; $Lbox;$Rdia"
+ S43pi $L';; $R'; []P,$R; $Lbox;$Rdia" and
(* Rules for [] and <> for S43 *)
- boxL: "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G"
- diaR: "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G"
+ boxL: "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" and
+ diaR: "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" and
pi1:
"[| $L1,<>P,$L2 |L> $Lbox; $L1,<>P,$L2 |R> $Ldia; $R |L> $Rbox; $R |R> $Rdia;
S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
- $L1, <>P, $L2 |- $R"
+ $L1, <>P, $L2 |- $R" and
pi2:
"[| $L |L> $Lbox; $L |R> $Ldia; $R1,[]P,$R2 |L> $Rbox; $R1,[]P,$R2 |R> $Rdia;
S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>