Lines Matching refs:a1
364 (!a1 a2 e1 e2.
366 ==> GCONTEXT (\t. sum (prefix a1 (e1 t)) (* GCONTEXT4 *)
417 Know `CONTEXT (\t. (prefix a1 (e1 t)))`
423 Know `CONTEXT (\t. (\t. (prefix a1 (e1 t))) t + (\t. (prefix a2 (e2 t))) t)`
1195 (!a1 a2 e1 e2.
1196 GSEQ e1 /\ GSEQ e2 ==> GSEQ (\t. sum (prefix a1 (e1 t)) (* GSEQ4 *)
1218 qpat_x_assum `CONTEXT e1` (ASSUME_TAC o (Q.SPEC `a1`) o (MATCH_MP CONTEXT3)) \\
1220 MP_TAC (Q.SPECL [`\t. (prefix a1 (e1 t))`, `\t. (prefix a2 (e2 t))`] CONTEXT4) \\
1342 Cases_on `a1` >> Cases_on `a2` >| (* 4 sub-goals here *)
1484 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\
1487 IMP_RES_TAC (Q.SPECL [`\t. (prefix a1 (H (prefix (label l) (E t))))`,
1516 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\
1519 IMP_RES_TAC (Q.SPECL [`\t. (prefix a1 (H (prefix a (E t))))`,
1556 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\
1559 IMP_RES_TAC (Q.SPECL [`\t. a1..(H (tau..(E t) + tau..(E' t)))`,
1596 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\
1599 IMP_RES_TAC (Q.SPECL [`\t. a1..(H (tau..(E t) + (label l2)..(e2 t)))`,
1638 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\
1641 IMP_RES_TAC (Q.SPECL [`\t. a1..(H ((label l2)..(e2 t) + tau..(E t)))`,
1679 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\
1682 IMP_RES_TAC (Q.SPECL [`\t. a1..(H ((label l1)..(e1 t) + (label l2)..(e2 t)))`,
1706 (!a1 a2 e1 e2.
1708 ==> WGS (\t. sum (prefix a1 (e1 t)) (* WGS4 *)
1764 MP_TAC (Q.SPECL [`a1`, `a2`, `(\x. (c :('a, 'b) context) (e x))`,