Searched refs:f2 (Results 126 - 150 of 315) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DCFL_RulesScript.sml322 `!ir1 ir2 pre_p1 post_p1 post_p2 stk_f in_f1 f1 f2 out_f1 out_f2.
324 PSPEC ir1 (pre_p1,post_p1) stk_f (in_f1,f1,out_f1) /\ PSPEC ir2 (post_p1,post_p2) stk_f (out_f1,f2,out_f2)
326 PSPEC (SC ir1 ir2) (pre_p1,post_p2) stk_f (in_f1,f2 o f1,out_f2)`,
334 `!cond ir_t ir_f pre_p post_p stk_f cond_f in_f f1 f2 out_f.
337 PSPEC ir_f (pre_p, post_p) stk_f (in_f,f2,out_f) /\ (!st. cond_f (in_f st) = eval_il_cond cond st)
339 PSPEC (CJ cond ir_t ir_f) (pre_p,post_p) stk_f (in_f, (\v.if cond_f v then f1 v else f2 v), out_f)`,
520 `!ir1 ir2 pre_p1 post_p1 post_p2 stk vi1 f1 vo1 f2 vo2.
522 VSPEC ir1 (pre_p1,post_p1) stk (vi1,f1,vo1) /\ VSPEC ir2 (post_p1,post_p2) stk (vo1,f2,vo2)
524 VSPEC (SC ir1 ir2) (pre_p1,post_p2) stk (vi1,f2 o f1,vo2)`,
531 `!cond ir_t ir_f pre_p post_p stk cond_f iv f1 f2 o
[all...]
/seL4-l4v-10.1.1/HOL4/src/datatype/inftree/
H A DinftreeScript.sml66 ((iNd b1 f1 = iNd b2 f2 : ('a,'b,'c)inftree) = (b1 = b2) /\ (f1 = f2))``,
78 Q_TAC SUFF_TAC `from_inftree (f1 x) = from_inftree (f2 x)`
/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient_optionScript.sml243 !a1 a2 f1 f2.
244 (R1 ===> R2) f1 f2 /\ (OPTION_REL R1) a1 a2 ==>
245 (OPTION_REL R2) (OPTION_MAP f1 a1) (OPTION_MAP f2 a2)���),
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/
H A DibmLib.sml390 (!f1 f1' f2 f2'.
392 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f2 f2' ==>
393 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE (F_AND (f1, f2)) (F_AND (f1', f2'))) /\
398 (!f1 f1' f2 f2'.
400 UF_EQUIVALENT___INFINITE_TOP_BOTTOM_FREE f2 f2'
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/
H A DinlineCompile.sml94 val f2 = mk_pabs(args,rand t2) value
96 (Term`TOTAL(^fb,^f1,^f2)`,
234 val (f2,f3) = dest_pair f2f3 value
237 val f2th = Convert_CONV f2
245 val f2' = (snd o dest_eq o concl) (inline f2th)
248 in prove(``^(concl totalth) = TOTAL( ^f1', ^f2' ,^f3')``,
H A Dcompile.sml62 (* Make an application TOTAL f1 f2 f3 *)
119 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`,
123 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`,
144 val f2 = mk_pabs(args,t2) value
146 val th2 = PBETA_CONV (mk_comb(f2,args))
147 val th3 = ISPECL [f1,f2] Par_de
171 val f2 = mk_pabs(args,t2) value
202 val f2 = mk_pabs(mk_pair(args,v),N) value
220 val f2 = mk_pabs(args,M) value
242 val f2 = mk_pabs(args,t2) value
386 val f2 = mk_pabs(args,rand t2) value
436 val f2 = mk_pabs(args,rand t2) value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A DprogScript.sml294 ``!f1 (f2:'a->'b) g p res res' c m.
296 (!x y. ~g x /\ p x /\ (y = f2 x) ==> SPEC m (res x) c (res' y)) ==>
297 (!x. TAILREC_PRE f1 g p x ==> SPEC m (res x) c (res' (TAILREC f1 f2 g x)))``,
302 ``!f1 (f2:'a->'b) g p res res' c m.
304 (!z x y. ~g x /\ p x /\ (y = f2 x) ==> SPEC m (res z x) c (res' z y)) ==>
305 (!z x. TAILREC_PRE f1 g p x ==> SPEC m (res z x) c (res' z (TAILREC f1 f2 g x)))``,
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DgrammarScript.sml324 rw[] >> qabbrev_tac `f2 = snils ++ fss` >>
325 `MAP ptree_fringe ptl = f1 ++ [xp ++ [x]] ++ f2` by simp[Abbr`f2`] >>
331 f2 = MAP ptree_fringe pt2 ���
336 `FLAT f2 = FLAT fss` by simp[Abbr`f2`, rich_listTheory.FLAT_APPEND] >>
340 disch_then (qxchl [`f1`, `f2`, `fpx`, `fs`] strip_assume_tac) >>
350 f2 = MAP ptree_fringe pt2 ���
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/common/
H A DtripleScript.sml26 case_sum f1 f2 x = case x of INL y => f1 y | INR y => f2 y`
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DPEGParse.sml53 | choice(e1,e2,f1,f2) => pe e1 inp stk (appf1(f1,k)) (returnTo(inp,stk,ksym(e2,appf1(f2,k),fk)))
/seL4-l4v-10.1.1/HOL4/src/prekernel/
H A DDep.sml118 fun pp_couple (f1,f2) (a1,a2) =
121 f2 a2; add_string ")";
/seL4-l4v-10.1.1/HOL4/tools/
H A Dbuildutils.sig39 (* [check_against f1 f2] checks to see if file f1 is older than file f2
/seL4-l4v-10.1.1/graph-refine/
H A Dstack_logic.py694 fun_offs[f] = max ([offs for (f2, offs) in fcall_offs
695 if f2 == f])
846 fs = set.union (set ([f for f in graph if [f2 for f2 in graph[f]
847 if f2 in fs2]]),
848 set ([f2 for f in fs2 for f2 in graph[f]]), fs2)
850 entries = list (fs - set ([f2 for f in graph for f2 in graph[f]]))
867 if [f2 fo
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/tests/inputs/
H A Dencap1.lisp34 (defun f2 (x)
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/test/
H A Dbackend_test.sml18 f2 = \x. if x = (0w:word32) then x
/seL4-l4v-10.1.1/HOL4/src/1/
H A DboolLib.sml203 (COMB(f1,x1), COMB (f2,x2)) =>
204 if aconv f1 f2 then recurse (pRight :: p) x1 x2
205 else if aconv x1 x2 then recurse (pLeft :: p) f1 f2
206 else recurse (pLeft :: p) f1 f2 @ recurse (pRight :: p) x1 x2
/seL4-l4v-10.1.1/HOL4/src/combin/
H A DcombinScript.sml213 `!f1 f2 a b c. ~(b = c) ==> ~((a =+ b) f = (a =+ c) f)`,
234 `!f1 f2 a b c.
235 ((a =+ b) f1 = (a =+ c) f2) ==>
236 (b = c) /\ !v. (a =+ v) f1 = (a =+ v) f2`,
/seL4-l4v-10.1.1/HOL4/examples/unification/triangular/nominal/
H A DnunifDefScript.sml157 Q.ABBREV_TAC `f2 = \n. FST (SND (f n))` THEN
158 `!n. FST (SND (f n)) = f2 n` by SRW_TAC [][Abbr`f2`] THEN
164 sysvars (f1 n) (f2 n) (f3 n) ��� sysvars (f1 m) (f2 m) (f3 m)`
181 (sysvars (f1 n) (f2 n) (f3 n) = sysvars (f1 m) (f2 m) (f3 m))`
185 sysvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m))
187 sysvars (f1 m) (f2 m) (f3 m)`
190 (sysvars (f1 (f' m)) (f2 (
[all...]
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/encap/
H A Dexample.lisp32 (defun f2 (x)
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/mips/
H A Dn32.S249 s.d $f2, 8(t4)
257 s.s $f2, 4(t4)
265 s.s $f2, 8(t4)
273 s.d $f2, 8(t4)
376 3 - return value high (v1 or $f2)
483 l.d $f2, V1_OFF2($sp)
489 l.s $f2, V1_OFF2($sp)
495 l.s $f2, V1_OFF2($sp)
501 l.d $f2, V1_OFF2($sp)
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/
H A Dsysv.S90 lfd %f2,-16-(8*4)-(7*8)(%r28)
137 stfd %f2,8(%r30)
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A DSubst.sml213 | matchList sub ((Term.Fn (f1,args1), Term.Fn (f2,args2)) :: rest) =
214 if Name.equal f1 f2 andalso length args1 = length args2 then
240 | solve' sub (Term.Fn (f1,args1)) (Term.Fn (f2,args2)) rest =
241 if Name.equal f1 f2 andalso length args1 = length args2 then
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A DSubst.sml213 | matchList sub ((Term.Fn (f1,args1), Term.Fn (f2,args2)) :: rest) =
214 if Name.equal f1 f2 andalso length args1 = length args2 then
240 | solve' sub (Term.Fn (f1,args1)) (Term.Fn (f2,args2)) rest =
241 if Name.equal f1 f2 andalso length args1 = length args2 then
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/
H A Ddecidable_separationLogicLibScript.sml572 ``!f1 f2 C pf sf pf' sf'.
574 LIST_DS_ENTAILS C (SAFE_MAP F f1 PF_TURN_EQ pf, sf) (SAFE_MAP F f2 PF_TURN_EQ pf', sf')``,
866 (SF_TRIVIAL_FILTER_PRED (sf_bin_tree (f1,f2) e) = (e = dse_nil)) /\
961 ``!f1 f2 f3 f4 f5 c1 c2 pfL sfL pfL' sfL'.
963 LIST_DS_ENTAILS (c1, (POS_FILTER f1 (\x. (FST x = SND x)) c2)) (POS_FILTER f2 PF_TRIVIAL_FILTER_PRED pfL, POS_FILTER f3 SF_TRIVIAL_FILTER_PRED sfL) (POS_FILTER f4 PF_TRIVIAL_FILTER_PRED pfL',POS_FILTER f5 SF_TRIVIAL_FILTER_PRED sfL')``,
1255 ``!f1 f2 c1 c2 pfL sfL pfL' sfL'.
1257 LIST_DS_ENTAILS (c1,c2) (HYPOTHESIS_RULE_MAP c1 [] pfL 0 f1 pfL,sfL) (HYPOTHESIS_RULE_MAP c1 pfL pfL' 0 f2 pfL',sfL')``,
1319 ``!e f1 f2 f1' f2' n m c1 c2 pfL sfL pfL' sfL'.
1320 (((f1' = f1) /\ (f2'
[all...]
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/riscv/src/
H A Driscv.spec3204 ; f2 = FPRS(rs2)
3205 ; res = match FP32_Compare(f1, f2)
3208 case FP_GT => f2
3209 case FP_UN => if ( (FP32_IsSignalingNan(f1) or FP32_IsSignalingNan(f2))
3210 or (f1 == RV32_CanonicalNan and f2 == RV32_CanonicalNan))
3212 else -- either f1 or f2 should be a quiet NaN
3213 if f1 == RV32_CanonicalNan then f2 else f1
3223 ; f2 = FPRS(rs2)
3224 ; res = match FP32_Compare(f1, f2)
3225 { case FP_LT => f2
[all...]

Completed in 133 milliseconds

1234567891011>>