Lines Matching refs:prefix
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)``,