Lines Matching defs:f3
56 (* Make an application TOTAL f1 f2 f3 *)
113 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`,
117 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`,
215 val f3 = mk_pabs(mk_pair(args,v),N)
216 val th1 = ISPECL [f1,f2,f3] LET_SEQ_PAR_THM
311 (* RecConvert (|- f x = if f1 x then f2 x else f(f3 x)) (|- TOTAL(f1,f2,f3)) *)
421 (* Extract totality predicate of the form TOTAL (f1,f2,f3) for a recursive *)
422 (* function of the form f(x) = if f1(x) then f2(x) else f (f3(x)) *)
622 (* |- TOTAL(f1,f2,f3) *)
624 (* |- TOTAL((\x. f1 x), (\x. f2 x), (\x. f3 x)) *)