49     (!a c.  OH_CONTEXT c ==> OH_CONTEXT (\t. prefix a (c t))) /\ (* OH_CONTEXT2 *)
86     (!a e.   CONTEXT e ==> CONTEXT (\t. prefix a (e t))) /\    (* CONTEXT3 *)
102   ``!a :'b Action. CONTEXT (\t. prefix a t)``,
204     (!a e.   GCONTEXT e ==> GCONTEXT (\t. prefix a (e t))) /\    (* GCONTEXT3 *)
207                         ==> GCONTEXT (\t. sum (prefix a1 (e1 t)) (* GCONTEXT4 *)
208                                               (prefix a2 (e2 t)))) /\
223   ``!a :'b Action. GCONTEXT (\t. prefix a t)``,
257       Know `CONTEXT (\t. (prefix a1 (e1 t)))`
259       Know `CONTEXT (\t. (prefix a2 (e2 t)))`
263       Know `CONTEXT (\t. (\t. (prefix a1 (e1 t))) t + (\t. (prefix a2 (e2 t))) t)`
416     (!a e.   CONTEXT e      ==> WG (\t. prefix a (e t))) /\      (* WG3 *)
428   ``!a :'b Action. WG (\t. prefix a t)``,
495     (!l e.   CONTEXT e      ==> SG (\t. prefix (label l) (e t))) /\ (* SG2 *)
496     (!a e.   SG e           ==> SG (\t. prefix a (e t))) /\         (* SG3 *)
540   ``!e. SG (\t. prefix tau (e t)) ==> SG e``,
553       qpat_x_assum `(\t. prefix tau (e t)) = X`
557       qpat_x_assum `(\t. prefix tau (e t)) = X`
562       qpat_x_assum `(\t. prefix tau (e t)) = X`
566       qpat_x_assum `(\t. prefix tau (e t)) = X`
570       qpat_x_assum `(\t. prefix tau (e t)) = X`
574       qpat_x_assum `(\t. prefix tau (e t)) = X`
620   ``!e e'. SG (\t. sum (prefix tau (e t)) (prefix tau (e' t))) ==> SG e /\ SG e'``,
640         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
644         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
648         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
651         `e1 = \t. prefix tau (e t)` by PROVE_TAC [] \\
655         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
659         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
663         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
684         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
688         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
692         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
695         `e2 = \t. prefix tau (e' t)` by PROVE_TAC [] \\
699         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
703         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
707         qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X`
712   ``!e e' L. SG (\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) ==> SG e``,
731       qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X`
735       qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X`
739       qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X`
742       `e1 = \t. prefix tau (e t)` by PROVE_TAC [] \\
746       qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X`
750       qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X`
754       qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X`
759   ``!e e' L. SG (\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) ==> SG e'``,
778       qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X`
782       qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X`
786       qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X`
789       `e2 = \t. prefix tau (e' t)` by PROVE_TAC [] \\
793       qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X`
797       qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X`
801       qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X`
816     (!a e.   SEQ e            ==> SEQ (\t. prefix a (e t))) /\     (* SEQ3 *)
823   ``!a :'b Action. SEQ (\t. prefix a t)``,
873     (!a e.            GSEQ e  ==> GSEQ (\t. prefix a (e t))) /\    (* GSEQ3 *)
875            GSEQ e1 /\ GSEQ e2 ==> GSEQ (\t. sum (prefix a1 (e1 t)) (* GSEQ4 *)
876                                                 (prefix a2 (e2 t))))`;
882   ``!a :'b Action. GSEQ (\t. prefix a t)``,
897       MP_TAC (Q.SPECL [`\t. (prefix a1 (e1 t))`, `\t. (prefix a2 (e2 t))`] CONTEXT4) \\
938         (!(l :'b Label) e. SEQ e ==> R (\t. prefix (label l) (e t))) /\
939         (!(a :'b Action) e. SG e /\ SEQ e /\ R e ==> R (\t. prefix a (e t))) /\
980         (!(l :'b Label) e. GSEQ e ==> R (\t. prefix (label l) (e t))) /\
981         (!(a :'b Action) e. SG e /\ GSEQ e /\ R e ==> R (\t. prefix a (e t))) /\
983                    ==> R (\t. sum (prefix tau (e1 t)) (prefix tau (e2 t)))) /\
985                    ==> R (\t. sum (prefix tau (e1 t)) (prefix (label l2) (e2 t)))) /\
987                    ==> R (\t. sum (prefix (label l1) (e1 t)) (prefix tau (e2 t)))) /\
989                    ==> R (\t. sum (prefix (label l1) (e1 t)) (prefix (label l2) (e2 t))))
1021         qpat_x_assum `!e1 e2. X ==> R (\t. prefix tau (e1 t) + prefix tau (e2 t))` MATCH_MP_TAC \\
1027         qpat_x_assum `!l2 e1 e2. X ==> R (\t. prefix tau (e1 t) + prefix (label l2) (e2 t))`
1034         qpat_x_assum `!l1 e1 e2. X ==> R (\t. prefix (label l1) (e1 t) + prefix tau (e2 t))`
1041         qpat_x_assum `!l1 l2 e1 e2. X ==> R (\t. prefix (label l1) (e1 t) + prefix (label l2) (e2 t))`
1067         IMP_RES_TAC (Q.SPECL [`\x. H (prefix (label l) (E x))`,
1068                               `\x. H' (prefix (label l) (E x))`] SG4) \\
1091                              `\x. (H :('a, 'b) CCS -> ('a, 'b) CCS) (prefix a (E x))`] SG3) \\
1095         IMP_RES_TAC (Q.SPECL [`\x. H (prefix a (E x))`, `\x. H' (prefix a (E x))`] SG4) \\
1106       POP_ASSUM (ASSUME_TAC o (Q.SPEC `\t. prefix a (E t)`)) \\
1164         IMP_RES_TAC (Q.SPECL [`\t. (prefix a1 (H (prefix (label l) (E t))))`,
1165                               `\t. (prefix a2 (H' (prefix (label l) (E t))))`] SG4) \\
1188                              `\x. (H :('a, 'b) CCS -> ('a, 'b) CCS) (prefix a (E x))`] SG3) \\
1196         IMP_RES_TAC (Q.SPECL [`\t. (prefix a1 (H (prefix a (E t))))`,
1197                               `\t. (prefix a2 (H' (prefix a (E t))))`] SG4) \\
1207       POP_ASSUM (ASSUME_TAC o (Q.SPEC `\t. prefix a (E t)`)) \\
1218         IMP_RES_TAC (Q.SPECL [`\t. (prefix tau (E t))`, `\t. (prefix tau (E' t))`] SG4) \\
1260         IMP_RES_TAC (Q.SPECL [`\t. (prefix tau (E t))`, `\t. (prefix (label l2) (e2 t))`] SG4) \\
1300         IMP_RES_TAC (Q.SPECL [`\t. (prefix (label l1) (e1 t))`, `\t. (prefix tau (E t))`] SG4) \\
1339         IMP_RES_TAC (Q.SPECL [`\t. (prefix (label l1) (e1 t))`,
1340                               `\t. (prefix (label l2) (e2 t))`] SG4) \\
1380     (!a e.   GCONTEXT e       ==> WGS (\t. prefix a (e t))) /\      (* WGS3 *)
1383                               ==> WGS (\t. sum (prefix a1 (e1 t))   (* WGS4 *)
1384                                                (prefix a2 (e2 t)))) /\
1398   ``!a :'b Action. WGS (\t. prefix a t)``,

Indexes created Tue Sep 03 12:52:19 MDT 2024