Searched refs:f2 (Results 226 - 250 of 315) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/executable-semantics/
H A DExecuteSemanticsScript.sml286 * Executable semantics of [f1 U f2]
287 * w |= [f1 U f2]
289 * |w| > 0 And (w |= f2 Or (w |= f1 And w^1 |= [f1 U f2]))
294 ``UF_SEM w (F_UNTIL(f1,f2)) =
297 (UF_SEM w f2
299 (UF_SEM w f1 /\ UF_SEM (RESTN w 1) (F_UNTIL(f1,f2))))``,
309 Cases_on `UF_SEM (FINITE l) f2`
341 Cases_on `UF_SEM (INFINITE f) f2`
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/
H A Duser_lemma_basicsScript.sml355 ``! f1 f2 k inv2 comb_inv uf uy.
359 (preserve_relation_mmu_abs f2 (assert_mode k) (comb_inv) uf uy) ==>
360 (preserve_relation_mmu (f1 >>= (f2)) (assert_mode k) comb_inv uf uy)
391 THEN Cases_on `f2 a b`
392 THEN Cases_on `f2 a' b'`
/seL4-l4v-10.1.1/HOL4/src/metis/
H A DmlibMeson.sml510 val (f1, f2) = Df (expands ancestors) (g1, g2)
515 (fn () => f1 (f2 c o reward n2) s)
516 (fn () => f2 (spend (n1 + 1) f1 (c o swivelp l1 l2) o reward n2) s) ()
H A DmlibTermorder.sml171 and g (Fn (f1,a1)) (Fn (f2,a2)) rest =
172 (case precedence ((f1, length a1), (f2, length a2)) of LESS => Less
H A DmlibModel.sml454 | comparep (FnP (f1 |-> n1), FnP (f2 |-> n2)) =
455 lex_order fp_compare Int.compare ((f1,n1),(f2,n2))
/seL4-l4v-10.1.1/HOL4/src/portableML/
H A DPortable.sml294 fun lex_cmp (c1, c2) (f1, f2) (x1, x2) =
296 EQUAL => c2 (f2 x1, f2 x2)
/seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/x64/model/
H A Dx64.sml1741 val (f2,r2) = value
1744 ( process_float_flags[f1,f2]; write'XMM(BitsN.@@(r1,r2),dst) )
1754 val (f2,r2) = value
1761 ( process_float_flags[f1,f2,f3,f4]
1831 val (f2,r2) = value
1834 ( process_float_flags[f1,f2]; write'XMM(BitsN.@@(r1,r2),dst) )
1844 val (f2,r2) = value
1851 ( process_float_flags[f1,f2,f3,f4]
1947 val (f2,d2) = sse_from_int32 32 (mode,BitsN.bits(95,64) x) value
1951 ( process_float_flags[(false,f1),(false,f2),(fals
1965 val (f2,w2) = sse_to_int64 32 (mode,BitsN.bits(63,0) x) value
1983 val (f2,r2) = FPConvert.fp64_to_fp32_with_flags(mode,q1) value
1985 val f2 = (FP64.isSubnormal(BitsN.bits(63,0) x),f2) value
2002 val (f2,w2) = sse_to_int32 32 (mode,BitsN.bits(95,64) x) value
2022 val f2 = value
2374 val (f2,r2) = sse_sqrt64(BitsN.bits(63,0) x) value
2400 val (f2,r2) = sse_sqrt32(BitsN.bits(95,64) x) value
[all...]
/seL4-l4v-10.1.1/HOL4/src/0/
H A DTerm.sml279 let fun f1 (Comb(Rator,Rand)) = (f2 Rator) orelse (f2 Rand)
280 | f1 (Abs(_,Body)) = f2 Body
281 | f1 (t as Clos _) = f2 (push_clos t)
283 and f2 t = term_eq t tm orelse f1 t function
284 in f2
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/lambda/
H A DliftScript.sml817 ���!f1 f2 x.
818 ($= ===> ALPHA) f1 f2 ==>
819 (variant x (FV1 ((f1 x):^term)) = variant x (FV1 (f2 x)))���,
831 ���!f1 f2 :var->^term.
832 ($= ===> ALPHA) f1 f2 ==>
833 ALPHA (Abs1 f1) (Abs1 f2)���,
/seL4-l4v-10.1.1/graph-refine/
H A Dproblem.py610 f2 = f + ', shape=doubleoctagon'
612 f2 = f + ', shape=Mdiamond'
614 % (c_nm, c, f2))
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A Dctl2muScript.sml354 val CTL2MU_AND_LEM = prove(``!(M: ('prop,'state) kripke_structure) f1 f2 . C_SEM M (C_AND(f1,f2)) = C_SEM M f1 INTER C_SEM M f2``,
362 val CTL2MU_OR_LEM = prove(``!(M: ('prop,'state) kripke_structure) f1 f2 . C_SEM M (C_NOT(C_AND(C_NOT f1,C_NOT f2))) = C_SEM M f1 UNION C_SEM M f2``,
/seL4-l4v-10.1.1/HOL4/src/floating-point/
H A Dmachine_ieeeLib.sml351 fun f2 v = wordsSyntax.mk_n2w (Term.mk_var (v, numSyntax.num), ty2) function
352 val l = all_combs (List.map f1 vs) (List.map f2 vs)
/seL4-l4v-10.1.1/HOL4/src/parse/
H A DFCNet.sml360 | (COMB(f1, x1), COMB(f2, x2)) =>
361 RM (TMP (f1, f2) :: TMP (x1, x2) :: rest) theta0
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DregexpMatch.sml255 fun pair_compare (f1, f2) ((x1,y1), (x2,y2)) =
257 EQUAL => f2 (y1, y2)
/seL4-l4v-10.1.1/HOL4/examples/logic/ltl/
H A DconcrGBArepScript.sml896 (��(eL1,f1) (eL2,f2). eL1.edge_grp = eL2.edge_grp)
935 (��(eL1,f1) (eL2,f2). eL1.edge_grp = eL2.edge_grp)
983 ((eL2:�� edgeLabelAA),(f2:�� ltl_frml)).
987 (f2:�� edgeLabelAA # num).
988 (FST f2).edge_grp ��� (FST f1).edge_grp)`
991 (f2:�� edgeLabelAA # �� ltl_frml).
992 (FST f2).edge_grp ��� (FST f1).edge_grp)`
1133 (��(eL1,f1) (eL2,f2).
/seL4-l4v-10.1.1/HOL4/examples/theorem-prover/lisp-runtime/garbage-collector/
H A Dstop_and_copyScript.sml692 ?h2 f2. gc_inv (h1,roots1,h2,f2) (b,i,j2,e,b2,e2,m2,z UNION (D1(CUT(j,j2)m2))) /\ j <= j2 /\
695 (!a. ~(f a = a) ==> (f2 a = f a)) /\
696 (!a. a IN ADDR_SET [x2] ==> ~(f2 a = a)) /\
697 ([x2] = ADDR_MAP f2 [x]) /\ full_heap j j2 m2 /\ c``,
881 `h2`,`f2`,`m3`,`j3`,`xs4`,`j4`,`m4`])
897 \\ `f2 (f2 n) = n` by FULL_SIMP_TAC std_ss [gc_inv_def,FUN_EQ_THM,abs_gc_inv_def,LET_DEF]
/seL4-l4v-10.1.1/HOL4/examples/Crypto/Serpent/Reference/
H A DSerpent_Reference_TransformationScript.sml649 val transCompose_def = Define `transCompose f1 f2 = \x. FLAT (MAP f1 (f2 x))`;
/seL4-l4v-10.1.1/HOL4/src/list/src/
H A DlistScript.sml463 ``!f1 f2 l. (MAP f1 l = MAP f2 l) = (!e. MEM e l ==> (f1 e = f2 e))``,
1431 ``!l1 l2 f1 f2.
1434 (ZIP (l1, MAP f2 l2) = MAP (\p. (FST p, f2 (SND p))) (ZIP (l1, l2)))``,
1806 ``!f1 f2 l1 l2. (MAP f1 l1 = MAP f2 l2) =
1808 (EVERY2 (\x y. f1 x = f2 y) l1 l2)``,
2346 (���!f1 f2
[all...]
/seL4-l4v-10.1.1/HOL4/src/meson/src/
H A DmesonLib.sml359 | Fnapp(f2,args2) =>
360 if f1 = f2
387 | Fnapp(f2,args2) =>
388 if f1 = f2 then Lib.all2 (fol_eq insts) args1 args2
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dxprop_logicScript.sml56 [`P`,`\(f1,f2). P f1 /\ P f2`]
128 `XP_COND(c, f1, f2) = XP_AND(XP_IMPL(c, f1), XP_IMPL(XP_NOT c, f2))`;
/seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/
H A DswsepScript.sml2241 (!f1 f2. (!q. MEM q input_regs_list ==> (f1 (FST q) = f2 (FST q))) ==>
2242 (!r. MEM r oregs_words ==> (f f1 r = f f2 r))) /\
2476 Q.PAT_ASSUM `!f1 f2. P f1 f2` (fn thm => MATCH_MP_TAC
2816 (!f1 f2. (!q. MEM q input_regs_list ==> (f1 (FST q) = f2 (FST q))) ==>
2817 (!r. MEM r oregs_words ==> (f f1 r = f f2 r))) /\
2879 Q.PAT_ASSUM `!f1 f2. P f1 f2` (f
[all...]
/seL4-l4v-10.1.1/HOL4/polyml/basis/
H A DOS.sml1037 fun leqPoll((p1, f1): poll_desc) ((p2, f2): poll_desc) =
1038 case compare(f1, f2) of
1043 fun merge ((p1, f1) :: (p2, f2) :: rest) =
1044 if compare(f1, f2) = EQUAL
1046 else (p1, f1) :: merge((p2, f2) :: rest)
/seL4-l4v-10.1.1/HOL4/src/quotient/Manual/
H A Dquotient.tex850 %{\tt ?- \verb+~+(?f1 f2 x. $E^2$ f1 f2 $\wedge$ \verb+~+$E$ (f1 x) (f2 x)},
851 %{\tt ?- !f1 f2 x. $E^2$ f1 f2 $\Rightarrow$ $E$ (f1 x) (f2 x)}
852 %(take ${\tt f1}\ z = f^? x$, and ${\tt f2}\ z = f^? y$),
863 %{\tt |- \verb+~+(?f1 f2 x. f1 = f2 $\wedge$ \verb+~+(f1 x = f2
[all...]
/seL4-l4v-10.1.1/HOL4/src/quotient/examples/sigma/
H A DliftScript.sml1234 ���!f1 f2 x.
1235 ($= ===> ALPHA_obj) f1 f2 ==>
1236 (variant x (FV_obj1 (f1 x)) = variant x (FV_obj1 (f2 x)))���,
1248 ���!f1 f2 :var->obj1.
1249 ($= ===> ALPHA_obj) f1 f2 ==>
1250 ALPHA_method (ABS1 f1) (ABS1 f2)���,
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/model_check/
H A DmodelCheckLib.sml595 fun model_check___psl_equivalent f1 f2 =
597 val thm = psl_equivalent2ks_fair_emptyness true f1 f2

Completed in 216 milliseconds

1234567891011>>