Lines Matching refs:f2
15 `sc (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`;
19 `cj f1 f2 f3 = \x. if f1 x then f2 x else f3 x`;
23 `tr (x:'a) = if f1 x then x else tr (f2 x)`;
33 ``!f f1 f2.
34 (!x:'a. f x = if f1(x) then x else f(f2 x))
35 ==> (?R. WF R /\ (!x. ~f1 x ==> R (f2 x) x))
36 ==> (f:'a->'a = tr f1 f2)``,
49 ``!f f1 f2 f3.
50 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x))
52 ==> (f:'a->'b = sc (tr f1 f3) f2)``,
59 Q.SPEC `\x. f x = sc (tr f1 f3) f2 x`) THEN