Stage work on pi-calculus

binghe · Mar 4, 2025 · 4343cb7 · 4343cb7
1 parent 1cd316e
commit 4343cb7
Show file tree

Hide file tree

Showing 2 changed files with 166 additions and 163 deletions.
diff --git a/examples/formal-languages/pi-calculus/open_bisimulationScript.sml b/examples/formal-languages/pi-calculus/open_bisimulationScript.sml
@@ -169,64 +169,64 @@ Inductive DTRANS :
 [DSUM2]
     !D P Q Rs. DTRANS D Q Rs ==> DTRANS D (Sum P Q) Rs
 
-[PAR1_I]
+[DPAR1_I]
     !D P P' Q a x.
        DTRANS D P (InputR (Name a) x P') /\ x # P /\ x # Q /\ x <> a ==>
        DTRANS D (Par P Q) (InputR (Name a) x (Par P' Q))
-[PAR1_BO]
+[DPAR1_BO]
     !D P P' Q a x.
        DTRANS D P (BoundOutput (Name a) x P') /\ x # P /\ x # Q /\ x <> a ==>
        DTRANS D (Par P Q) (BoundOutput (Name a) x (Par P' Q))
-[PAR1_FO]
+[DPAR1_FO]
     !D P P' Q a b.
        DTRANS D P (FreeOutput (Name a) (Name b) P') ==>
        DTRANS D (Par P Q) (FreeOutput (Name a) (Name b) (Par P' Q))
-[PAR1_T]
+[DPAR1_T]
     !D P P' Q. DTRANS D P (TauR P') ==> DTRANS D (Par P Q) (TauR (Par P' Q))
 
-[PAR2_I]
+[DPAR2_I]
     !D P Q Q' a x.
        DTRANS D Q (InputR (Name a) x Q') /\ x # Q /\ x # P /\ x <> a ==>
        DTRANS D (Par P Q) (InputR (Name a) x (Par P Q'))
-[PAR2_BO]
+[DPAR2_BO]
     !D P Q Q' a x.
        DTRANS D Q (BoundOutput (Name a) x Q') /\ x # Q /\ x # P /\ x <> a ==>
        DTRANS D (Par P Q) (BoundOutput (Name a) x (Par P Q'))
-[PAR2_FO]
+[DPAR2_FO]
     !D P Q Q' a b.
        DTRANS D Q (FreeOutput (Name a) (Name b) Q') ==>
        DTRANS D (Par P Q) (FreeOutput (Name a) (Name b) (Par P Q'))
-[PAR2_T]
+[DPAR2_T]
     !D P Q Q'. DTRANS D Q (TauR Q') ==> DTRANS D (Par P Q) (TauR (Par P Q'))
 
-[COMM1]
+[DCOMM1]
     !D P P' Q Q' a b x.
        DTRANS D P (InputR (Name a) x P') /\
        DTRANS D Q (FreeOutput (Name a) (Name b) Q') /\
        x # P /\ x # Q /\ x <> a /\ x <> b /\ x # Q' ==>
        DTRANS D (Par P Q) (TauR (Par (tpm [(x,b)] P') Q'))
-[COMM2]
+[DCOMM2]
     !D P P' Q Q' a b x.
        DTRANS D P (FreeOutput (Name a) (Name b) P') /\
        DTRANS D Q (InputR (Name a) x Q') /\
        x # Q /\ x # P /\ x <> a /\ x <> b /\ x # P' ==>
        DTRANS D (Par P Q) (TauR (Par P' (tpm [(x,b)] Q')))
-[CLOSE1]
+[DCLOSE1]
     !D P P' Q Q' a x y.
        DTRANS D P (InputR (Name a) x P') /\
        DTRANS D Q (BoundOutput (Name a) y Q') /\
        x # P /\ x # Q /\ y # P /\ y # Q /\
        x <> a /\ x # Q' /\ y <> a /\ y # P' /\ x <> y ==>
        DTRANS D (Par P Q) (TauR (Res y (Par (tpm [(x,y)] P') Q')))
-[CLOSE2]
+[DCLOSE2]
     !D P P' Q Q' a x y.
        DTRANS D P (BoundOutput (Name a) y P') /\
        DTRANS D Q (InputR (Name a) x Q') /\
        x # P /\ x # Q /\ y # P /\ y # Q /\
        x <> a /\ x # P' /\ y <> a /\ y # Q' /\ x <> y ==>
        DTRANS D (Par P Q) (TauR (Res y (Par P' (tpm [(x,y)] Q'))))
 
-[RES_I]
+[DRES_I]
     !D D' P P' a x y.
     (* begin extra antecedents *)
        distinction D /\
@@ -235,7 +235,7 @@ Inductive DTRANS :
        DTRANS D' P (InputR (Name a) x P') /\
        y <> a /\ y <> x /\ x # P /\ x <> a ==>
        DTRANS D (Res y P) (InputR (Name a) x (Res y P'))
-[RES_BO]
+[DRES_BO]
     !D D' P P' a x y.
     (* begin extra antecedents *)
        distinction D /\
@@ -244,7 +244,7 @@ Inductive DTRANS :
        DTRANS D' P (BoundOutput (Name a) x P') /\
        y <> a /\ y <> x /\ x # P /\ x <> a ==>
        DTRANS D (Res y P) (BoundOutput (Name a) x (Res y P'))
-[RES_FO]
+[DRES_FO]
     !D D' P P' a b y.
     (* begin extra antecedents *)
        distinction D /\
@@ -253,7 +253,7 @@ Inductive DTRANS :
        DTRANS D' P (FreeOutput (Name a) (Name b) P') /\
        y <> a /\ y <> b ==>
        DTRANS D (Res y P) (FreeOutput (Name a) (Name b) (Res y P'))
-[RES_T]
+[DRES_T]
     !D D' P P' y.
     (* begin extra antecedents *)
        distinction D /\