Lines Matching refs:f2
156 Q.ABBREV_TAC `f2 = \n. FST (SND (f n))` THEN
157 `!n. FST (SND (f n)) = f2 n` by SRW_TAC [][Abbr`f2`] THEN
163 `��n. allvars (f1 n) (f2 n) (f3 n)`]
181 (allvars (f1 n) (f2 n) (f3 n) = allvars (f1 m) (f2 m) (f3 m))`
185 allvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m))
187 allvars (f1 m) (f2 m) (f3 m)`
190 (allvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m)))
191 (allvars (f1 m) (f2 m) (f3 m))`
197 in allvars (f1 t) (f2 t) (f3 t)`
203 `\n. allvars (f1 n) (f2 n) (f3 n) DIFF (FDOM(f1 n))`, `m`]
213 (f2 (SUC n)) (f2 n)`
217 POP_ASSUM (Q.SPEC_THEN `\n. f2 (z+n+1)` MP_TAC) THEN