Searched refs:f2 (Results 176 - 200 of 315) sorted by relevance

1234567891011>>

/seL4-l4v-10.1.1/HOL4/src/quotient/src/
H A Dquotient_sumScript.sml270 !f1 f2 g1 g2.
271 (R1 ===> R2) f1 f2 /\ (R3 ===> R4) g1 g2 ==>
272 ((R1 +++ R3) ===> (R2 +++ R4)) (f1 ++ g1) (f2 ++ g2)���),
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/
H A Ddecidable_separationLogicScript.sml455 ``(!f1 f2 f3. DISJOINT (FDOM f1) (FDOM f2) ==> (((f1 SUBMAP (FUNION f2 f3)) = (f1 SUBMAP f3)))) /\
456 (!f1 f2 f3. DISJOINT (FDOM f1) (FDOM f3 DIFF (FDOM f2)) ==> (((f1 SUBMAP (FUNION f2 f3)) = (f1 SUBMAP f2))))``,
464 ``!f1 f2 f3. (f1 SUBMAP f2) \/ ((DISJOINT (FDOM f1) (FDOM f2) /\ (f
[all...]
/seL4-l4v-10.1.1/HOL4/examples/category/
H A DlimitScript.sml455 qmatch_rename_tac `f1 = f2` >>
456 first_x_assum (qspecl_then [`FST f1.map`,`FST f2.map`] assume_tac) >>
457 qsuff_tac `FST f1.map = FST f2.map` >- (
460 Cases_on `f1.map` >> Cases_on `f2.map` >> srw_tac [][] >>
498 `���f1 f2 f3. ���c a b. is_category c ��� a ��� c.obj ��� b ��� c.obj ��� (���l. is_limit (product_diagram c a b) l) ���
499 f2 c a b :- f1 c a b ��� a -:c ���
503 ���!m. m :- p ��� f1 c a b -:c ��� (f2 c a b o m -:c = p1) ��� (f3 c a b o m -:c = p2)`,
H A Dnat_transScript.sml612 `���f1 f2 n. is_nat_trans n ��� is_functor f1 ��� is_functor f2 ��� (f1 ���> f2) ��� (f1.dom = ntcod n) ���
613 (functor_nt (f2 ��� f1) n = functor_nt f2 (functor_nt f1 n))`,
773 qmatch_abbrev_tac `g##(g1 o f1 -:g.dom) = g##(g2 o f2 -:g.dom)` >>
779 `f2 ���> g2 -:g.dom` by (
781 srw_tac [][Abbr`f2`,Abbr`g2`] >>
785 qspecl_then [`g`,`g.dom`,`g.cod`,`f2`,`g2`] mp_tac morf_comp >>
788 `g##f2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/
H A Dcompile.sig82 (* RecConvert (|- f x = if f1 x then f2 x else f(f3 x)) (|- TOTAL(f1,f2,f3)) *)
118 (* Extract totality predicate of the form TOTAL (f1,f2,f3) for a recursive *)
119 (* function of the form f(x) = if f1(x) then f2(x) else f (f3(x)) *)
181 (* |- TOTAL(f1,f2,f3) *)
183 (* |- TOTAL((\x. f1 x), (\x. f2 x), (\x. f3 x)) *)
312 (* |- <circuit> ===> DEV f2 *)
/seL4-l4v-10.1.1/isabelle/src/Tools/Metis/src/
H A Dproblems.sml1684 ({FinPath . (pair . R . s) . f2 . n} \/
1685 ~{FinPath . (pair . R . s) . f1 . n} \/ ~(f1 . gv7034 = f2 . gv7034)) /\
1686 (~{FinPath . (pair . R . s) . f2 . n} \/
1687 {FinPath . (pair . R . s) . f1 . n} \/ ~(f1 . gv7034 = f2 . gv7034)) /\
1688 (~{FinPath . (pair . R . s) . f2 . n} \/
1690 ({FinPath . (pair . R . s) . f2 . n} \/
1693 f1 . x = f2 . x \/
1695 {FinPath . (pair . R . s) . f2 . n} /\
1696 {R . (pair . (f2 . n) . (f2
[all...]
/seL4-l4v-10.1.1/l4v/isabelle/src/Tools/Metis/src/
H A Dproblems.sml1684 ({FinPath . (pair . R . s) . f2 . n} \/
1685 ~{FinPath . (pair . R . s) . f1 . n} \/ ~(f1 . gv7034 = f2 . gv7034)) /\
1686 (~{FinPath . (pair . R . s) . f2 . n} \/
1687 {FinPath . (pair . R . s) . f1 . n} \/ ~(f1 . gv7034 = f2 . gv7034)) /\
1688 (~{FinPath . (pair . R . s) . f2 . n} \/
1690 ({FinPath . (pair . R . s) . f2 . n} \/
1693 f1 . x = f2 . x \/
1695 {FinPath . (pair . R . s) . f2 . n} /\
1696 {R . (pair . (f2 . n) . (f2
[all...]
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.2/
H A DHSLScript.sml378 `!S1 S2 in_f1 f1 f2 out_f1 out_f2.
379 CSPEC S1 (in_f1,f1,out_f1) /\ CSPEC S2 (out_f1,f2,out_f2)
381 CSPEC (Sc S1 S2) (in_f1, sc f1 f2,out_f2)`,
388 `!cond St Sf cond_f in_f f1 f2 out_f.
389 CSPEC St (in_f,f1,out_f) /\ CSPEC Sf (in_f,f2,out_f) /\
392 CSPEC (Cj cond St Sf) (in_f, cj cond_f f1 f2, out_f)`,
/seL4-l4v-10.1.1/HOL4/examples/HolBdd/
H A DMachineTransitionScript.sml694 ``(!m. m <= n+1 ==> (f1 m = f2 m)) = (!m. m <= n ==> (f1 m = f2 m)) /\ (f1(n+1) = f2(n+1))``,
711 ``!f1 f2 n.
712 (!m. m <= n ==> (f1 m = f2 m)) ==> (FinPath(R,s) f1 n = FinPath(R,s) f2 n)``,
/seL4-l4v-10.1.1/HOL4/examples/elliptic/swsep/
H A DswsepLib.sml250 val f_depend_term = ``!f1 f2.
251 (!q. MEM q ^input_regs_list ==> (f1 (FST q) = f2 (FST q))) ==>
252 !r. MEM r ^oregs_words ==> (^f f1 r = ^f f2 r)``
/seL4-l4v-10.1.1/HOL4/src/num/theories/
H A Dprim_recScript.sml326 * fun (SUC m) x1 ... xn = f2(fun m x1 ... xn, m, x1, ... ,xn)
332 * fun (SUC m) = \x1 ... xn. f2(fun m x1 ... xn, m, x1, ... ,xn)
333 * = (\f m x1 ... xn. f2(f x1 ... xn, m, x1, ... ,xn))(fun m)m
339 * (\f m x1 ... xn. f2(f x1 ... xn, m, x1, ... ,xn))
/seL4-l4v-10.1.1/HOL4/src/rational/
H A DfracLib.sml371 FRAC_CALC_CONV ``frac_add f1 f2``;
372 FRAC_CALC_CONV ``frac_add f1 ( frac_sub (abs_frac(4i,5i)) f2)``;
373 FRAC_CALC_CONV ``frac_add f1 ( frac_div (abs_frac(4i,5i)) f2)``;
374 FRAC_CALC_CONV ``frac_add (frac_ainv f1) ( frac_mul f2 (frac_minv f3))``;
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/src/powerpc/
H A Dppc_closure.S60 stfd %f2, 56(%r1)
151 lfd %f2,112+8(%r1)
/seL4-l4v-10.1.1/HOL4/examples/ARM_security_properties/
H A Dswitching_lemmaScript.sml1027 let f2 = (((if (s2.psrs (0,CPSR)).M = 22w then
1037 ((? a b a' b'. (f2 s1 = ValueState a b) /\ (f2 s2 = ValueState a' b')
1041 (?e. (f2 s1 =Error e) /\ (f2 s2 = Error e)))
1070 let f2 = (((if (s2.psrs (0,CPSR)).M = 22w then
1081 ((? a b a' b'. (f2 s1 = ValueState a b) /\ (f2 s2 = ValueState a' b')
1084 (?e. (f2 s1 = Error e) /\ (f2 s
[all...]
/seL4-l4v-10.1.1/HOL4/examples/formal-languages/context-free/
H A DpegexecScript.sml88 | AP (appf2 f2 k) i (SOME v1 :: SOME v2 :: r) =>
89 AP k i (SOME (f2 v2 v1) :: r)
/seL4-l4v-10.1.1/HOL4/src/finite_map/
H A DfmaptreeScript.sml95 ``(FTNode i1 f1 = FTNode i2 f2) = (i1 = i2) /\ (f1 = f2)``,
/seL4-l4v-10.1.1/HOL4/src/tactictoe/src/
H A DtttPredict.sml210 fun f2 x = exists_tid x andalso uptodate_tid x andalso dmem x revdict function
212 first_test_n f2 n l1
/seL4-l4v-10.1.1/HOL4/examples/machine-code/hoare-triple/
H A DtailrecLib.sml99 fun leaves_inl body f1 f2 = ftree2tm (leaves (tm2ftree body) (fn tm =>
102 else f2 (cdr (fst (dest_pair tm)),snd (dest_pair tm))))
/seL4-l4v-10.1.1/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dppc_seq_monadScript.sml161 (PREAD_S f (PWRITE_S f2 b s) = if f = f2 then b else PREAD_S f s)``,
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/tools/
H A Dpsl_lemmataScript.sml922 (F_SERE_FREE (F_AND(f1,f2)) = F_SERE_FREE f1 /\ F_SERE_FREE f2)
930 (F_SERE_FREE (F_UNTIL(f1,f2)) = F_SERE_FREE f1 /\ F_SERE_FREE f2)
958 [`P`,`\(f1,f2). P f1 /\ P f2`]
2339 (IS_TOP_BOTTOM_WELL_BEHAVED (F_AND(f1,f2)) = IS_TOP_BOTTOM_WELL_BEHAVED f1 /\ IS_TOP_BOTTOM_WELL_BEHAVED f2)
2347 (IS_TOP_BOTTOM_WELL_BEHAVED (F_UNTIL(f1,f2)) = IS_TOP_BOTTOM_WELL_BEHAVED f1 /\ IS_TOP_BOTTOM_WELL_BEHAVED f2)
[all...]
/seL4-l4v-10.1.1/HOL4/tools/Holmake/
H A DHolmake_tools.sml360 fun file_compare (f1, f2) = String.compare (fromFile f1, fromFile f2)
706 fun (f1 forces_update_of f2) = let
710 (not (FileSys.access(f2, [])) orelse FileSys.modTime f1 > FileSys.modTime f2)
/seL4-l4v-10.1.1/HOL4/examples/acl2/examples/
H A DfmapExample.sml1349 (``(!f f1 f2 a. outcome_case f f1 f2 (RESULT a) = f a) /\
1350 (!f f1 f2 a. outcome_case f f1 f2 (ERROR a) = f1 a) /\
1351 (!f f1 f2 a. outcome_case f f1 f2 (TIMEOUT a) = f2 a)``,
1357 ``!f f1 f2 b x y.
1358 outcome_case f f1 f2 (if b then x else y) =
1359 if b then outcome_case f f1 f2
[all...]
/seL4-l4v-10.1.1/HOL4/src/pred_set/src/more_theories/
H A DwellorderScript.sml886 ``BIJ f1 (elsOf w1) (elsOf w2) /\ BIJ f2 (elsOf w1) (elsOf w2) /\
888 (!x y. (x,y) WIN w1 ==> (f2 x, f2 y) WIN w2) ==>
889 !x. x IN elsOf w1 ==> (f1 x = f2 x)``,
893 first_x_assum (qspec_then `elsOf w1 INTER {x | f1 x <> f2 x}` mp_tac) >>
896 Cases_on `f1 min = f2 min` >> simp[] >>
897 Cases_on `(f1 min, f2 min) WIN w2` >| [
898 `?a. (f2 a = f1 min) /\ a IN elsOf w1` by metis_tac [BIJ_IFF_INV] >>
901 `(f2 min, f1 min) WIN w2` by metis_tac [BIJ_IFF_INV, WIN_trichotomy] >>
902 `?a. (f1 a = f2 mi
[all...]
/seL4-l4v-10.1.1/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dautomaton_formulaScript.sml62 [`P`,`\(f1,f2). P f1 /\ P f2`]
99 [`P0`,`\(A, f). P0 f`,`\(f1,f2). P0 f1 /\ P0 f2`]
1001 ``!A1 f1 A2 f2. (A_USED_STATE_VARS_COMPATIBLE (A_NDET(A1, f1)) (A_NDET(A2, f2))) ==>
1002 ((AUTOMATON_EQUIV (A_AND(A_NDET(A1, f1), A_NDET(A2, f2))) (A_NDET((PRODUCT_SEMI_AUTOMATON A1 A2), A_AND(f1,f2)))))``,
1034 SUBGOAL_TAC `(DISJOINT (A_USED_INPUT_VARS f2) A1.S) /\
1070 SUBGOAL_TAC `(DISJOINT (A_USED_INPUT_VARS f2) A
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/
H A Djit_incrementalScript.sml483 ?f2. x86_write_jump_pre(w,a + 5w,df,f) /\
484 (x86_write_jump(w,a + 5w,df,f) = (df,f2)) /\
485 (CODE_LOOP 0 j cs * r) (fun2set (f2,df))``,
607 ?f2. x86_write_jump_cond_pre(v,w,a + 5w,df,f) /\
608 (x86_write_jump_cond(v,w,a + 5w,df,f) = (df,f2)) /\
609 (CODE_LOOP 0 j cs * r) (fun2set (f2,df))``,
686 ?f2 bs. x86_encodes_jump_pre (a,n2w i,df,f) /\
687 (x86_encodes_jump (a,n2w i,df,f) = (a+5w,n2w i,df,f2)) /\
688 (SEP_BYTES_IN_MEM a bs * r) (fun2set (f2,df)) /\
800 ``!p cs c j f f2 d
[all...]

Completed in 162 milliseconds

1234567891011>>