Lines Matching defs:f3
102 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`,
106 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`,
196 val f3 = mk_pabs(mk_pair(args,v),N)
197 val th1 = ISPECL [f1,f2,f3] LET_SEQ_PAR_THM
284 (* RecConvert (|- f x = if f1 x then f2 x else f(f3 x)) *)
285 (* (|- TOTAL(f1,f2,f3)) *)