Searched refs:i2 (Results 51 - 75 of 114) sorted by relevance

12345

/seL4-l4v-master/HOL4/examples/machine-code/graph/
H A Dstack_analysisLib.sml130 val (i,(th1,i1,i2),thi2) = el 3 (rev thms)
133 fun approx_summary (i,(th1,i1,i2),thi2) =
135 then map tidy_up_summary (summary (i,(th1,i1,i2),thi2))
137 val res = map tidy_up_summary (summary (i,(th1,i1,i2),thi2))
/seL4-l4v-master/HOL4/examples/temporal_deep/src/translations/
H A Domega_automaton_translationsScript.sml62 (\((s1, i1),(s2, i2)). (s1, i1, s2, i2) IN A.R /\ i1 SUBSET A.I /\ i2 SUBSET A.I)
262 !(S1 :'a set) (S2 :'a set) (i1 :'a set) (i2 :'a set).
264 (IS_TRANSITION A' S1 i1 S2 i2 <=>
265 (S2 = {s2 | s2 IN A'.S /\ ?s1. s1 IN S1 /\ IS_TRANSITION A (g s1) i1 (g s2) i2})))`;
354 INPUT_RUN_STATE_UNION A' i2 S2 DIFF A.S UNION l'') =
355 XP_SEM A.R (INPUT_RUN_STATE_UNION A i1 l', INPUT_RUN_STATE_UNION A i2 l'')` THEN1 (
361 ((INPUT_RUN_STATE_UNION A' i2 S2 DIFF A.S UNION l'') INTER XP_USED_X_VARS A.R =
362 (INPUT_RUN_STATE_UNION A i2
[all...]
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/
H A Dcheney_gcScript.sml635 (cheney_step(i,j,e,m) = (i2,j2,e2,m2)) ==> (e2 = e) /\ j <= j2 /\
636 cheney_inv(b,b',i2,j2,j2,e2,f,m2,w,xx,r)``,
646 \\ Q.PAT_X_ASSUM `i + 1 = i2` (K ALL_TAC)
787 !i2 m2. (cheney(i,j,e,m) = (i2,m2)) ==>
788 cheney_inv(b,b',i2,i2,i2,e,f,m2,w,xx,r) /\ j <= i2) (i,j,e,m)``,
790 \\ `?i2 j
[all...]
H A Darm_cheney_allocScript.sml198 \\ `?i2 e2 rs2 l2 u2 m2. cheney_alloc_gc (i,e,rs,l,u,m) = (i2,e2,rs2,l2,u2,m2)` by METIS_TAC [PAIR]
203 \\ `ok_state (i2,e2,rs2,l2,u2,m2)` by METIS_TAC [cheney_collector_spec,cheney_alloc_gc_def]
/seL4-l4v-master/HOL4/src/finite_maps/
H A DfmaptreeScript.sml94 (FTNode i1 f1 = FTNode i2 f2) <=> (i1 = i2) /\ (f1 = f2)
/seL4-l4v-master/HOL4/src/meson/src/
H A DCanon_Port.sml26 fun tmi_eq (tm1,i1:int) (tm2,i2) = aconv tm1 tm2 andalso i1 = i2
H A DmesonLib.sml54 fun tmi_eq (tm1,i1:int) (tm2,i2) = aconv tm1 tm2 andalso i1 = i2
646 fun eek (x1,(i1,th1)) (x2,(i2,th2)) =
647 (x1=x2) andalso (i1=i2) andalso thm_eq th1 th2
701 fun key_eq (i1,tm1) (i2,tm2) = aconv tm1 tm2 andalso i1 = i2
/seL4-l4v-master/HOL4/src/coalgebras/
H A DcoalgAxiomsScript.sml205 ((P,pf):'p system,i1,i2) (:'d)
208 hom i2 (C,cf) (P,pf) /\ restr (i1 o f) A = restr (i2 o g) A /\
214 restr (u o i2) C = j2
244 Spushout A B C f g (P,i1,i2) (:'d) ==>
245 ?pf. Fpushout (A,af) (B,bf) (C,cf) f g ((P,pf),i1,i2) (:'d)
253 ���shom f A B /\ shom g A C /\ shom i1 B P /\ shom i2 C P���
255 Cases_on ���restr (i1 o f) A = restr (i2 o g) A��� >> simp[] >> reverse eq_tac
/seL4-l4v-master/HOL4/examples/elliptic/
H A DMap.sml578 | iterCompare kcmp vcmp (SOME i1) (SOME i2) =
579 keyIterCompare kcmp vcmp (readIterator i1) (readIterator i2) i1 i2
580 and keyIterCompare kcmp vcmp (k1,v1) (k2,v2) i1 i2 =
587 iterCompare kcmp vcmp (advanceIterator i1) (advanceIterator i2)
/seL4-l4v-master/HOL4/examples/dev/sw/
H A DIRSyntax.sml110 let val (i1,i2) = (index_of_exp s1, index_of_exp s2)
112 if i1 > i2 then GREATER
113 else if i1 = i2 then EQUAL
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DIRSyntax.sml110 let val (i1,i2) = (index_of_exp s1, index_of_exp s2)
112 if i1 > i2 then GREATER
113 else if i1 = i2 then EQUAL
/seL4-l4v-master/HOL4/examples/dev/sw/working/0.2/
H A DIRSyntax.sml110 let val (i1,i2) = (index_of_exp s1, index_of_exp s2)
112 if i1 > i2 then GREATER
113 else if i1 = i2 then EQUAL
/seL4-l4v-master/HOL4/src/datatype/
H A Dind_typeScript.sml247 !c1 i1 r1 c2 i2 r2. (CONSTR c1 i1 r1 :'a recspace = CONSTR c2 i2 r2) <=>
248 (c1 = c2) /\ (i1 = i2) /\ (r1 = r2)
/seL4-l4v-master/HOL4/polyml/mlsource/MLCompiler/CodeTree/
H A DCODETREE_REMOVE_REDUNDANT.sml106 and mergefield(l1 as ((f1 as (i1, u1)) :: tl1), l2 as (f2 as (i2, u2)) ::tl2) =
107 if i1 < i2 then f1 :: mergefield(tl1, l2)
108 else if i1 > i2 then f2 :: mergefield(l1, tl2)
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/ppc/
H A Dprog_ppcLib.sml215 | ((th1,i1,j1),SOME (th2,i2,j2)) => ((rename th1,i1,j1),SOME (rename th2,i2,j2))
/seL4-l4v-master/HOL4/examples/machine-code/instruction-set-models/x86/
H A Dx86_seq_monadScript.sml321 STRIP_TAC THEN `?r2 e2 s2 m2 i2. s = (r2,e2,s2,m2,i2)` by METIS_TAC [pairTheory.PAIR]
/seL4-l4v-master/HOL4/examples/miller/ho_prover/
H A Dho_discrimTools.sml77 | (BVAR i1, BVAR i2) => i1 = i2
/seL4-l4v-master/HOL4/src/postkernel/
H A DTheoryPP.sml215 val {theory as (name,i1,i2), parents=parents0, thydata, mldeps, axioms,
329 val {theory as (name,i1,i2), parents=parents0,
/seL4-l4v-master/HOL4/src/pattern_matches/
H A DpatternMatchesScript.sml943 (MAP2 (\i1 i2. i1 /\ i2) ip1 ip2)`;
948 (REDUNDANT_ROWS_INFOS_CONJ (i1 :: is1) (i2::is2) =
949 (i1 /\ i2) :: (REDUNDANT_ROWS_INFOS_CONJ is1 is2))``,
966 (MAP2 (\i1 i2. i1 \/ i2) ip1 ip2)`;
/seL4-l4v-master/HOL4/src/rational/
H A DfracScript.sml787 * |- !f1 f2 i1 i2. (frac_sgn f1 = i1) ==> (frac_sgn f2 = i2) ==>
788 * (frac_sgn (frac_mul f1 f2) = i1 * i2)
792 (*val FRAC_SGN_MUL = store_thm("FRAC_SGN_MUL", ``!f1 f2 i1 i2. (frac_sgn f1 = i1) ==> (frac_sgn f2 = i2) ==> (frac_sgn (frac_mul f1 f2) = i1 * i2)``,
/seL4-l4v-master/isabelle/src/Tools/Metis/src/
H A DKeyMap.sml963 | (SOME i1, SOME i2) =>
966 and (k2,v2) = readIterator i2
976 and io2 = advanceIterator i2
989 | (SOME i1, SOME i2) =>
992 and (k2,v2) = readIterator i2
998 and io2 = advanceIterator i2
H A DMap.sml955 | (SOME i1, SOME i2) =>
958 and (k2,v2) = readIterator i2
968 and io2 = advanceIterator i2
981 | (SOME i1, SOME i2) =>
984 and (k2,v2) = readIterator i2
990 and io2 = advanceIterator i2
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/
H A DKeyMap.sml963 | (SOME i1, SOME i2) =>
966 and (k2,v2) = readIterator i2
976 and io2 = advanceIterator i2
989 | (SOME i1, SOME i2) =>
992 and (k2,v2) = readIterator i2
998 and io2 = advanceIterator i2
H A DMap.sml955 | (SOME i1, SOME i2) =>
958 and (k2,v2) = readIterator i2
968 and io2 = advanceIterator i2
981 | (SOME i1, SOME i2) =>
984 and (k2,v2) = readIterator i2
990 and io2 = advanceIterator i2
/seL4-l4v-master/HOL4/examples/computability/kolmog/
H A Dplain_kolmog_inequalitiesScript.sml719 ������i2 b2. p2 = pair i2 b2���
723 qabbrev_tac���ARG = pair (n2bl N1) (pair (n2bl SIb_i) (pair a1 (pair i1 b1) ++ pair i2 b2))��� >>

Completed in 172 milliseconds

12345