Searched refs:f2 (Results 26 - 50 of 315) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/parser.mosmlyacc/
H A DData.sml52 | F_AND of fl * fl (* f1 \wedge f2 *)
54 | F_U of fl * fl (* [f1 U f2] *)
62 | F_OR of fl * fl (* f1 \vee f2 *)
63 | F_IMP of fl * fl (* f1 \rightarrow f2 *)
64 | F_IFF of fl * fl (* f1 \leftrightarrow f2 *)
68 | F_W of fl * fl (* [f1 W f2] *)
74 | F_STRONG_UNTIL of fl * fl (* [f1 until! f2] *)
75 | F_WEAK_UNTIL of fl * fl (* [f1 until f2] *)
76 | F_STRONG_UNTIL_INC of fl * fl (* [f1 until!_ f2] *)
77 | F_WEAK_UNTIL_INC of fl * fl (* [f1 until_ f2] *)
[all...]
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/parser/
H A DParserTools.sml123 | flToTerm(F_AND(f1,f2)) =
124 ``F_AND(^(flToTerm f1), ^(flToTerm f2))``
127 | flToTerm(F_U(f1,f2)) =
128 ``F_U(^(flToTerm f1), ^(flToTerm f2))``
141 | flToTerm(F_OR(f1,f2)) =
142 ``F_OR(^(flToTerm f1), ^(flToTerm f2))``
143 | flToTerm(F_IMP(f1,f2)) =
144 ``F_IMP(^(flToTerm f1), ^(flToTerm f2))``
145 | flToTerm(F_IFF(f1,f2)) =
146 ``F_IFF(^(flToTerm f1), ^(flToTerm f2))``
[all...]
/seL4-l4v-10.1.1/l4v/tools/autocorres/tests/examples/
H A Dcondition_guard.c38 void f2(struct ure *p) { function
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/testsuite/libffi.call/
H A Dmany.c14 static float ABI_ATTR 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
18 (double) f1, (double) f2, (double) f3, (double) f4, (double) f5,
23 return f1+f2+f3+f4+f5+f6+f7+f8+f9+f10+f11+f12+f13;
/seL4-l4v-10.1.1/HOL4/src/new-datatype/
H A DNDDB.sml74 val sum_prod_duality = prove(``!f1 f2.
75 (prod_retrieve f1 f2) =
76 (combin$C (sum_retrieve (combin$C f1) (combin$C f2)))``,
109 prove(``!f1 g1 f2 g2.
110 ((sum_retrieve g1 g2)o h) o ((sum_map f1 f2)o h) =
111 ((sum_retrieve (g1 o f1) (g2 o f2)) o h)``
119 val sum_inj_pair_thm = prove(``!f1 g1 f2 g2.
121 (inj_pair f2 g2) ==>
122 (inj_pair (sum_map f1 f2) (sum_retrieve g1 g2))``,
130 val sum_retrieve_map_thm = prove(``!f1 g1 f2 g
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A DtailrecScript.sml19 TAILREC f1 (f2:'a->'b) g x = f2 (WHILE g f1 x)`;
64 ``!f1 (f2:'a->'b) g x. TAILREC f1 f2 g x = if g x then TAILREC f1 f2 g (f1 x) else f2 x``,
79 ``(f1 = f1') /\ (f2 = (f2':'a->'b)) /\ (g = g') /\ (s = s') ==>
80 (TAILREC f1 f2 g = TAILREC f1' f2'
[all...]
/seL4-l4v-10.1.1/HOL4/examples/HolCheck/
H A Dctl2muTools.sml33 | "B_AND" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
34 in mu_conj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
35 (*``^(ctl2mu_aux prop_type f1) /\ ^(ctl2mu_aux prop_type f2)`` *)
36 | "B_OR" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
37 in mu_disj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
38 (*``^(ctl2mu_aux prop_type f1) \/ ^(ctl2mu_aux prop_type f2)`` *)
43 | "C_AND" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
44 in mu_conj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 cons) end
45 | "C_OR" => let val (f1,f2) = pairSyntax.dest_pair (List.hd args)
46 in mu_disj (ctl2mu_aux f1 cons) (ctl2mu_aux f2 con
[all...]
/seL4-l4v-10.1.1/HOL4/src/rational/
H A DfracUtils.sml48 dest_frac ``frac_add f1 f2``;
49 dest_frac ``frac_add (frac_sub f1 f2) f3``;
62 extract_frac ``frac_add f1 f2 = sub f1 f2``;
63 extract_frac ``!f1 f2. nmr (frac_add f1 f2) = frac_dnm (frac_sub f1 f2)``;
64 extract_frac ``frac_nmr (frac_add f1 f2) = frac_dnm (frac_sub f1 f2)``;
H A DfracScript.sml62 val les_abs_def = Define`les_abs f1 f2 = frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1`;
65 val frac_add_def = Define `frac_add f1 f2 = abs_frac(frac_nmr f1 * frac_dnm f2 + frac_nmr f2 * frac_dnm f1, frac_dnm f1*frac_dnm f2)`;
66 val frac_sub_def = Define `frac_sub f1 f2 = frac_add f1 (frac_ainv f2)`;
67 val frac_mul_def = Define `frac_mul f1 f2
[all...]
/seL4-l4v-10.1.1/HOL4/src/tfl/examples/
H A DctlScript.sml106 /\ (IS_CTL (E ((STATE f1) U (STATE f2))) = IS_CTL f1 /\ IS_CTL f2)
107 /\ (IS_CTL (E ((STATE f1) R (STATE f2))) = IS_CTL f1 /\ IS_CTL f2)
111 /\ (IS_CTL (A ((STATE f1) U (STATE f2))) = IS_CTL f1 /\ IS_CTL f2)
112 /\ (IS_CTL (A ((STATE f1) R (STATE f2))) = IS_CTL f1 /\ IS_CTL f2)
117 /\ (IS_CTL (f1 \/ f2) = IS_CTL f1 /\ IS_CTL f2)
[all...]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dfull_ltlScript.sml59 [`P`,`\(f1,f2). P f1 /\ P f2`]
71 (LTL_SEM_TIME t v (LTL_AND (f1,f2)) =
72 LTL_SEM_TIME t v f1 /\ LTL_SEM_TIME t v f2)
80 (LTL_SEM_TIME t v (LTL_SUNTIL(f1,f2)) =
81 ?k. (k >= t) /\ (LTL_SEM_TIME k v f2) /\ (!j. (t <= j /\ j < k) ==> (LTL_SEM_TIME j v f1)))
86 (LTL_SEM_TIME t v (LTL_PSUNTIL(f1,f2)) =
87 ?k. (k <= t) /\ (LTL_SEM_TIME k v f2) /\ (!j. (k < j /\ j <= t) ==> (LTL_SEM_TIME j v f1)))`;
114 `LTL_OR(f1,f2) = LTL_NOT (LTL_AND((LTL_NOT f1),(LTL_NOT f2)))`;
[all...]
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/
H A DfixedPointScript.sml136 ``fnsum f1 f2 X = f1 X UNION f2 X``);
143 ``!f1 f2. monotone f1 /\ monotone f2 ==> monotone (fnsum f1 f2)``,
147 `f2 X SUBSET f2 Y` by PROVE_TAC [] THEN
182 ``!f1 f2. monotone f1 /\ monotone f2 ==>
183 lfp f1 SUBSET lfp (fnsum f1 f2) /\
[all...]
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.01/official-semantics/
H A DUnclockedSemanticsScript.sml126 (OLD_UF_SEM w (F_AND(f1,f2)) =
127 OLD_UF_SEM w f1 /\ OLD_UF_SEM w f2)
132 (OLD_UF_SEM w (F_UNTIL(f1,f2)) =
134 OLD_UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). OLD_UF_SEM (RESTN w j) f1)
178 (UF_SEM w (F_AND(f1,f2)) =
179 UF_SEM w f1 /\ UF_SEM w f2)
184 (UF_SEM w (F_UNTIL(f1,f2)) =
186 UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). UF_SEM (RESTN w j) f1)
230 (O_SEM M (O_AND(f1,f2)) s = O_SEM M f1 s /\ O_SEM M f2
[all...]
H A DRewritesScript.sml116 (F_INIT_CLOCK_COMP c (F_AND(f1,f2)) =
117 F_AND(F_INIT_CLOCK_COMP c f1, F_INIT_CLOCK_COMP c f2))
122 (F_INIT_CLOCK_COMP c (F_UNTIL(f1,f2)) =
124 F_AND(F_BOOL c, F_INIT_CLOCK_COMP c f2)))
154 (F_CLOCK_COMP c (F_AND(f1,f2)) =
155 F_AND(F_CLOCK_COMP c f1, F_CLOCK_COMP c f2))
160 (F_CLOCK_COMP c (F_UNTIL(f1,f2)) =
162 F_AND(F_BOOL c, F_CLOCK_COMP c f2)))
H A DClockedSemanticsScript.sml112 (OLD_F_SEM w c (F_AND(f1,f2)) =
113 OLD_F_SEM w c f1 /\ OLD_F_SEM w c f2)
121 (OLD_F_SEM w c (F_UNTIL(f1,f2)) =
125 OLD_F_SEM (RESTN w k) c f2 /\
182 (OLD_F_SEM w c (F_AND(f1,f2)) =
183 OLD_F_SEM w c f1 /\ OLD_F_SEM w c f2)
191 (OLD_F_SEM w c (F_UNTIL(f1,f2)) =
194 OLD_F_SEM (RESTN w k) c f2 /\
251 (F_SEM w c (F_AND(f1,f2)) =
252 F_SEM w c f1 /\ F_SEM w c f2)
[all...]
H A DSyntaxScript.sml57 | F_AND of fl # fl (* f1 \wedge f2 *)
59 | F_UNTIL of fl # fl (* [f1 U f2] *)
73 | O_AND of obe # obe (* f1 \wedge f2 *)
75 | O_EU of obe # obe (* E[f1 U f2] *)
/seL4-l4v-10.1.1/HOL4/src/boss/theory_tests/
H A Dtheory1Script.sml26 val f2_def = Define`f2 n = n + 1`;
31 ``f2 = SUC``,
/seL4-l4v-10.1.1/HOL4/src/integer/
H A DDeepSyntaxScript.sml19 `(eval_form (Conjn f1 f2) x = eval_form f1 x /\ eval_form f2 x) /\
20 (eval_form (Disjn f1 f2) x = eval_form f1 x \/ eval_form f2 x) /\
29 `(neginf (Conjn f1 f2) = Conjn (neginf f1) (neginf f2)) /\
30 (neginf (Disjn f1 f2) = Disjn (neginf f1) (neginf f2)) /\
39 `(posinf (Conjn f1 f2) = Conjn (posinf f1) (posinf f2)) /\
[all...]
/seL4-l4v-10.1.1/HOL4/tools/cmp/
H A Dcmp.sml15 [f1, f2] => (f1, f2)
/seL4-l4v-10.1.1/l4v/tools/c-parser/testfiles/
H A Dinner_fncalls.c38 int f2(int x) function
H A Dparse_addr.c34 int *f2(void) function
H A Dparse_forloop.c42 int f2(int *a) function
/seL4-l4v-10.1.1/HOL4/examples/dev/
H A DcompileScript.sml99 (* Seq f1 f2 f1 followed by f2 in series *)
100 (* Par f1 f2 f1 in parallel with f2 *)
101 (* Ite f1 f2 f3 if f1 then f2 else f3 *)
102 (* Rec f1 f2 f3 tail recursion with test f1, base f2 and step f3 *)
106 Define `Seq f1 f2 = \x. f2(f
[all...]
/seL4-l4v-10.1.1/HOL4/src/tactictoe/examples/
H A Dttt_demoScript.sml88 ``(MAP f1 ls = MAP f2 ls) /\ MEM x ls ==> (f1 x = f2 x)``,
89 (* ttt ([],``(MAP f1 ls = MAP f2 ls) /\ MEM x ls ==> (f1 x = f2 x)``); *)
/seL4-l4v-10.1.1/HOL4/examples/PSL/1.1/official-semantics/
H A DRewritesScript.sml99 (F_CLOCK_COMP c (F_AND(f1,f2)) =
100 F_AND(F_CLOCK_COMP c f1, F_CLOCK_COMP c f2))
105 (F_CLOCK_COMP c (F_UNTIL(f1,f2)) =
107 F_AND(F_WEAK_BOOL c, F_CLOCK_COMP c f2)))

Completed in 175 milliseconds

1234567891011>>