Searched refs:f2 (Results 51 - 75 of 315) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/
H A DSyntaxScript.sml56 | F_AND of fl # fl (* f1 and f2 *)
60 | F_UNTIL of fl # fl (* [f1 U f2] *)
72 | O_AND of obe # obe (* f1 and f2 *)
74 | O_EU of obe # obe (* E[f1 U f2] *)
H A DUnclockedSemanticsScript.sml209 (UF_SEM v (F_AND(f1,f2)) =
210 UF_SEM v f1 /\ UF_SEM v f2)
235 (UF_SEM v (F_UNTIL(f1,f2)) =
237 UF_SEM (RESTN v k) f2 /\ !j :: (LESS k). UF_SEM (RESTN v j) f1)
271 (UF_SEM v (F_AND(f1,f2)) =
272 UF_SEM v f1 /\ UF_SEM v f2)
297 (UF_SEM v (F_UNTIL(f1,f2)) =
299 UF_SEM (RESTN v k) f2 /\ !j :: (LESS k). UF_SEM (RESTN v j) f1)
353 (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/
H A Dmany2_win32.c13 float f2,
26 return ((f1/f2+f3/f4+f5/f6+f7/f8+f9/f10+f11/f12) * f13);
12 fastcall_many(float f1, float f2, float f3, float f4, float f5, float f6, float f7, float f8, float f9, float f10, float f11, float f12, float f13) argument
H A Dmany_win32.c13 float f2,
26 return ((f1/f2+f3/f4+f5/f6+f7/f8+f9/f10+f11/f12) * f13);
12 stdcall_many(float f1, float f2, float f3, float f4, float f5, float f6, float f7, float f8, float f9, float f10, float f11, float f12, float f13) argument
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DjrhCore.sml27 val conjn_rwt = prove(``!f1 f2 x. eval_form f1 x /\ eval_form f2 x =
28 eval_form (Conjn f1 f2) x``, tac)
29 val disjn_rwt = prove(``!f1 f2 x. eval_form f1 x \/ eval_form f2 x =
30 eval_form (Disjn f1 f2) x``, tac)
58 (* i.e., c1 /\ c2 = eval_form f1 x /\ eval_form f2 x *)
190 ``(eval_form (neginf (Conjn f1 f2)) x = eval_form (neginf f1) x /\
191 eval_form (neginf f2) x) /\
192 (eval_form (neginf (Disjn f1 f2))
[all...]
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A DindexedListsScript.sml67 ``!l1 l2 f1 f2.
68 l1 = l2 /\ (!x n. MEM x l2 ==> f1 n x = f2 n x) ==>
69 MAPi f1 l1 = MAPi f2 l2``,
74 ``l1 = l2 ==> (!x n. (x = EL n l2) ==> n < LENGTH l2 ==> f1 n x = f2 n x) ==>
75 MAPi f1 l1 = MAPi f2 l2``,
76 map_every qid_spec_tac [`f1`, `f2`, `l2`] >> Induct_on `l1` >>
108 ``(!m. m < n ==> f1 m = f2 m) ==> GENLIST f1 n = GENLIST f2 n``,
109 map_every qid_spec_tac [`f1`, `f2`] >> Induct_on `n` >>
135 (!n e a. n < LENGTH l2 ==> MEM e l2 ==> f1 n e a = f2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/
H A DANF.sml106 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`,
110 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`,
141 val f2 = mk_pabs(args,t2) value
143 val th2 = PBETA_CONV (mk_comb(f2,args))
144 val th3 = ISPECL [f1,f2] Par_def
145 val ptm = mk_pabs(args, mk_pair(mk_comb(f1,args),mk_comb(f2,arg
168 val f2 = mk_pabs(args,t2) value
199 val f2 = mk_pabs(args,M) value
219 val f2 = mk_pabs(args,t2) value
365 val f2 = mk_pabs(args,rand t2) value
[all...]
H A DcpsScript.sml15 `Seq (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`;
19 `Par f1 f2 = \x. (f1 x, f2 x)`;
23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`;
27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`;
304 ``!f f1 f2 f3.
305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x))
307 ==> (f:'a->'b = Rec f1 f2 f
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DANF.sml106 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`,
110 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`,
141 val f2 = mk_pabs(args,t2) value
143 val th2 = PBETA_CONV (mk_comb(f2,args))
144 val th3 = ISPECL [f1,f2] Par_def
145 val ptm = mk_pabs(args, mk_pair(mk_comb(f1,args),mk_comb(f2,arg
168 val f2 = mk_pabs(args,t2) value
199 val f2 = mk_pabs(args,M) value
219 val f2 = mk_pabs(args,t2) value
365 val f2 = mk_pabs(args,rand t2) value
[all...]
H A DcpsScript.sml15 `Seq (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`;
19 `Par f1 f2 = \x. (f1 x, f2 x)`;
23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`;
27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`;
304 ``!f f1 f2 f3.
305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x))
307 ==> (f:'a->'b = Rec f1 f2 f
[all...]
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/
H A DformParseScript.sml163 ������s1 s2 f1 f2 top1 top2.
164 (s1 = s2) ��� (���s. LENGTH s < LENGTH s1 ��� (f1 s = f2 s)) ���
166 (parseFGX f1 top1 s1 = parseFGX f2 top2 s2)���,
175 rename [���option_CASE (f2 s')���, ���f1 _ = f2 _���] >>
176 reverse (Cases_on ���f2 s'���) >> simp[UNIT_DEF]
177 >- (rename [���f2 s' = SOME p���] >> Cases_on ���p��� >> simp[]) >>
185 >- (rename [���option_CASE (f2 s2)���, ���f1 _ = f2 _���] >> Cases_on ���f2 s
[all...]
/seL4-l4v-10.1.1/HOL4/src/finite_map/
H A Dfinite_mapScript.sml498 (`!x y (f1:('a,'b)fmap) f2.
499 (f1 = f2) ==>
500 ((\f.FUPDATE f (x,y)) f1 = (\f. FUPDATE f (x,y)) f2)`,
745 ``!f1 f2 s1 s2.
746 (DRESTRICT f1 s1 = DRESTRICT f2 s2) =
747 (DRESTRICT f1 s1 SUBMAP f2 /\ DRESTRICT f2 s2 SUBMAP f1 /\
748 (s1 INTER FDOM f1 = s2 INTER FDOM f2))``,
886 ``!f1 f2 m. DISJOINT (FDOM f1) (FDOM f2)
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw2/
H A DnestedCases.sml37 `num_case b f2 z =
39 else let v = destruct_suc z in f2 v`,
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DParseDatatype_dtype.sml19 fun pr (f1,f2) (a,b) = "(" ^ f1 a ^ "," ^ f2 b ^ ")"
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/
H A Dheap_wrap.c32 void f2(struct thing *t) { function
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/
H A Darrays.c21 i10 *f2(void) function
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A DctlScript.sml61 | C_AND of ctl # ctl (* f1 \wedge f2 *)
63 | C_EU of ctl # ctl (* E[f1 U f2] *)
343 (C_SEM M (C_AND(f1,f2)) s = C_SEM M f1 s /\ C_SEM M f2 s) /\
345 (C_SEM M (C_EU(f1,f2)) s = CEU M (C_SEM M f1, C_SEM M f2) s) /\
360 val C_AU_def = Define `C_AU ((f1: 'prop ctl),(f2: 'prop ctl)) = C_AND(C_NOT(C_EU(C_NOT f2,C_AND(C_NOT f1,C_NOT f2))),C_NOT(C_EG(C_NOT f2)))`;
[all...]
/seL4-l4v-10.1.1/HOL4/src/boss/theory_tests/
H A Dgithub112Script.sml6 val f2_def = Define `(f2 x y = case (x, y) of (0, _) => SOME 1 | _ => NONE)`
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DcpsScript.sml15 `Seq (f1:'a->'b) (f2:'b->'c) = \x. f2(f1 x)`;
19 `Par f1 f2 = \x. (f1 x, f2 x)`;
23 `Ite f1 f2 f3 = \x. if f1 x then f2 x else f3 x`;
27 `Rec (x:'a) = if f1 x then f2 x else Rec (f3 x)`;
304 ``!f f1 f2 f3.
305 (!x:'a. f x = if f1(x) then f2(x) else f(f3 x))
307 ==> (f:'a->'b = Rec f1 f2 f
[all...]
H A DANF.sml106 (`!f1 f2 f3. Seq (Par f1 f2) f3 = \x. let v = f2 x in f3 (f1 x,v)`,
110 (`!f2 f3. Seq (Par (\x.x) f2) f3 = \x. let v = f2 x in f3 (x,v)`,
141 val f2 = mk_pabs(args,t2) value
143 val th2 = PBETA_CONV (mk_comb(f2,args))
144 val th3 = ISPECL [f1,f2] Par_def
145 val ptm = mk_pabs(args, mk_pair(mk_comb(f1,args),mk_comb(f2,arg
168 val f2 = mk_pabs(args,t2) value
199 val f2 = mk_pabs(args,M) value
219 val f2 = mk_pabs(args,t2) value
365 val f2 = mk_pabs(args,rand t2) value
[all...]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/
H A DrltlScript.sml39 | RLTL_AND of rltl # rltl (* f1 and f2 *)
41 | RLTL_SUNTIL of rltl # rltl (* [f1 U f2] *)
58 [`P`,`\(f,b). P f`,`\(f1,f2). P f1 /\ P f2`]
70 (RLTL_SEM_TIME t v a r (RLTL_AND (f1,f2)) =
71 RLTL_SEM_TIME t v a r f1 /\ RLTL_SEM_TIME t v a r f2)
76 (RLTL_SEM_TIME t v a r (RLTL_SUNTIL(f1,f2)) =
77 ?k. (k >= t) /\ (RLTL_SEM_TIME k v a r f2) /\ (!j. (t <= j /\ j < k) ==> (RLTL_SEM_TIME j v a r f1)))
109 `RLTL_OR(f1,f2) = RLTL_NOT (RLTL_AND((RLTL_NOT f1),(RLTL_NOT f2)))`;
[all...]
/seL4-l4v-10.1.1/HOL4/examples/category/
H A DYonedaScript.sml61 `(TypedGraphFun (t2,t3) f2) o (TypedGraphFun (t1,t2) f1) -:ens_cat U =
62 (TypedGraphFun (t4,t3) f1) o (TypedGraphFun (t1,t4) f2) -:ens_cat U` >>
65 (���x. x ��� t2 ��� f2 x ��� t3) ���
66 (���x. x ��� t1 ��� f2 x ��� t4)` by (
89 srw_tac [][Abbr`f1`,Abbr`f2`] >>
383 qmatch_abbrev_tac `(f1 o f2 -:ens_cat (homs c) = f3 o f4 -:ens_cat (homs c)) ��� X` >>
384 `IsTypedFun f2` by (
385 srw_tac [][Abbr`f2`] >>
412 `f2 ���> f1 -:ens_cat (homs c)` by (
413 fsrw_tac [][Abbr`f2`,hom_de
[all...]
/seL4-l4v-10.1.1/HOL4/examples/real-to-float/
H A DdaisyScript.sml42 (eval_F c env (Add f1 f2) = c.add (eval_F c env f1) (eval_F c env f2)) /\
43 (eval_F c env (Div f1 f2) = c.div (eval_F c env f1) (eval_F c env f2))`
46 (eval_C c env (LessEq f1 f2) = c.less_eq (eval_F c env f1) (eval_F c env f2))`
190 (f_str (Add f1 f2) = "(" ++ f_str f1 ++ " + " ++ f_str f2 ++ ")") /\
194 (c_str (LessEq f1 f2) = "(" ++ f_str f1 ++ " <= " ++ f_str f2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/
H A Dinference_rulesScript.sml445 THEN Cases_on `f2 a b`
446 THEN Cases_on `f2 a' b'`
482 ``! f1 f2 k k' invr23 uf uy.
486 (preserve_relation_mmu_abs f2 (assert_mode k) (assert_mode k') uf uy) ==>
487 (preserve_relation_mmu (f1 >>= (f2)) (assert_mode k) invr23 uf uy)
495 ``! f1 f2 k k' uf uy.
498 (preserve_relation_mmu_abs f2 (assert_mode k') (assert_mode k') uf uy) ==>
499 (preserve_relation_mmu (f1 >>= (f2)) (assert_mode k) (assert_mode k') uf uy)
506 ``! f1 f2 k k' comb_inv uf uy.
510 (preserve_relation_mmu_abs f2 (assert_mod
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/common/
H A DdecoderScript.sml114 (((DT >> f1) ++ (DF >> f2)) (g,F::b) = f2 (g,b)) /\
115 (((DF >> f2) ++ (DT >> f1)) (g,F::b) = f2 (g,b)) /\
116 (((DT >> f1) ++ (DF >> f2)) (g,T::b) = f1 (g,b)) /\
117 (((DF >> f2) ++ (DT >> f1)) (g,T::b) = f1 (g,b)) /\

Completed in 216 milliseconds

1234567891011>>