Searched refs:f5 (Results 26 - 35 of 35) sorted by relevance

12

/seL4-l4v-10.1.1/HOL4/src/meson/test/
H A Dselftest.sml2945 (!Z X. member(Z,first(X)) ==> little_set(f5(Z,X))) /\
2946 (!Z X. member(Z,first(X)) ==> equal(X,ordered_pair(f4(Z,X),f5(Z,X)))) /\
3077 (!U7 V7 W7. equal(U7,V7) ==> equal(f5(U7,W7),f5(V7,W7))) /\
3078 (!X7 Z7 Y7. equal(X7,Y7) ==> equal(f5(Z7,X7),f5(Z7,Y7))) /\
3292 (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) ==> topological_space(X,Vt) \/ element_of_collection(f3(X,Vt),Vt) \/ subset_collections(f5(X,Vt),Vt)) /\
3293 (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) /\ element_of_collection(union_of_members(f5(X,Vt)),Vt) ==> topological_space(X,Vt) \/ element_of_collection(f3(X,Vt),Vt)) /\
3294 (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) ==> topological_space(X,Vt) \/ element_of_collection(f4(X,Vt),Vt) \/ subset_collections(f5(X,Vt),Vt)) /\
3295 (!X Vt. equal_sets(union_of_members(Vt),X) /\ element_of_collection(empty_set,Vt) /\ element_of_collection(X,Vt) /\ element_of_collection(union_of_members(f5(
[all...]
/seL4-l4v-10.1.1/HOL4/examples/machine-code/just-in-time/
H A Djit_incrementalScript.sml1286 \\ `?f5. x86_encodes_jump (r3 + 0xDw,n2w (w2n c),df,f4) =
1287 (r3 + 0x12w,n2w (w2n c),df,f5)` by
1291 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH d)) cs ((n =+ SOME r3) j) (fun2set (f5,df))` by
1338 \\ Q.PAT_X_ASSUM `f2' = f5` (fn th => FULL_SIMP_TAC std_ss [th])
1398 \\ `?f5. x86_encodes_jump (r3 + 0xDw,n2w (w2n c),df,(r3 + 0x3w =+ 0x82w) f4) =
1399 (r3 + 0x12w,n2w (w2n c),df,f5)` by
1405 \\ `CODE_INV (r3 + n2w (INSTR_LENGTH d)) cs ((n =+ SOME r3) j) (fun2set (f5,df))` by
1454 \\ Q.PAT_X_ASSUM `f2' = f5` (fn th => FULL_SIMP_TAC std_ss [th])
/seL4-l4v-10.1.1/HOL4/src/tfl/src/
H A DDefn.sml1479 ``(f1 x = f2 (x-1) + f5 (x-1)) /\
1483 (f5 x = f6 (x-1)) /\
1484 (f6 x = f5(x-1) + f7(x-2)) /\
/seL4-l4v-10.1.1/HOL4/examples/decidable_separationLogic/src/
H A Ddecidable_separationLogicLib.sml621 val (f5, p5) = get_sf_trival_filter sf'; value
625 val thm = ISPECL [f1, f2,f3,f4, f5, c1, c2, pf, sf, pf', sf'] INFERENCE_TRIVIAL_FILTER;
H A Ddecidable_separationLogicLibScript.sml961 ``!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')``,
/seL4-l4v-10.1.1/HOL4/examples/dev/sw/working/0.1/
H A DILTheory.sml1394 V"f5"
3126 V"f5'"
/seL4-l4v-10.1.1/HOL4/src/bool/
H A DboolScript.sml3847 val f5 = UNDISCH (NOT_ELIM (EQ_MP f4 f0)) value
3848 val f6 = CCONTR (mk_neg(f_eq_g)) f5
/seL4-l4v-10.1.1/HOL4/src/pattern_matches/
H A DpatternMatchesLib.sml3835 fun pmi_genupdate f1 f2 f3 f4 f5 f6 f7 f8 f9
3841 pmi_has_double_bound_pat_vars = f5 (#pmi_has_double_bound_pat_vars pmi),
/seL4-l4v-10.1.1/HOL4/polyml/libpolyml/libffi/
H A Dtexinfo.tex9004 \gdef^^f5{\~o}
9124 \gdef^^f5{\H o}
H A Dconfigure17152 ?00??f5?:*:*:*) ax_gcc_arch="opteron k8" ;;

Completed in 180 milliseconds

12