Lines Matching defs:t2
26 % | T if t1 was the last time before t2 that f was T %
27 % LAST (t1,t2) f = < %
33 % LAST (t1,t2) f = (t1 <= t2) /\ (f t1) /\ !t. t1<t /\ t<=t2 ==> ~(f t) %
40 "LAST (t1,t2) f =
41 (t1 <= t2) /\ (f t1) /\ !t. (t1<t) /\ (t<=t2) ==> ~(f t)");;
86 % | T if f is T an even number of times between t1 and t2%
87 % PTY (t1,t2) f = < %
88 % | F if f is T an odd number of times between t1 and t2 %
94 % PTY (t1,t2) f = PARITY (t2-t1) (\t. f(t+t1)) %
102 (`PTY`, "PTY (t1,t2) f = PARITY (t2-t1) (\t. f(t+t1))");;
110 % PTY (t1, SUC t2) f = (f(SUC t2) => ~PTY(t1,t2)f | PTY(t1,t2)f) %
139 (!t1 t2 f.
140 (t1 <= t2) ==>
141 (PTY (t1, SUC t2) f = (f(SUC t2) => ~PTY(t1,t2)f | PTY(t1,t2)f)))",
148 THEN REWRITE_TAC[SYM(ASSUME "(SUC t2) - t1 = SUC(t2 - t1)")]
149 THEN ASSUME_TAC(SPEC "t2:num" LESS_EQ_SUC_REFL)
177 % !t1 t2. LAST(t1,t2)reset ==> (out t2 = PTY(t1,t2)in) %
186 !t1 t2. LAST(t1,t2)reset ==> (out t2 = PTY(t1,t2)in)");;
348 % t1 <= t2 ==> %
349 % LAST(t1,t2)reset ==> %
350 % (out t2 = PTY(t1,t2)in) %
356 let th2 = SPECL["t2-t1";"t1:num"]th1
360 let th4 = REWRITE_RULE[MATCH_MP SUB_ADD (ASSUME "t1<=t2")]th3
378 THEN ASM_CASES_TAC "t1<=t2"