/seL4-l4v-master/HOL4/examples/Crypto/RC6/ |
H A D | RC6Script.sml | 296 `!i S1 L1 a1 b1 S2 L2 a2 b2. 297 LENGTH (setKeys i S1 L1 a1 b1) = LENGTH (setKeys i S2 L2 a2 b2)`
|
/seL4-l4v-master/HOL4/examples/miller/ho_prover/ |
H A D | unifyTools.sml | 188 (COMB (a1, b1), COMB (a2, b2)) => 190 val s1 = ((bvs1, a1), (bvs2, a2))
|
/seL4-l4v-master/HOL4/examples/AI_tasks/ |
H A D | mleCombinLib.sml | 50 let val (a1,a2) = pair_of_list argl in a2 :: strip_cA_aux a1 end value
|
/seL4-l4v-master/HOL4/src/simp/src/ |
H A D | selftest.sml | 169 ([a1], [a2]) => aconv a1 asm andalso aconv a2 asm
|
/seL4-l4v-master/HOL4/examples/elliptic/ |
H A D | fieldTools.sml | 802 val (a1,a2) = value 805 | SOME (_,a1,a2) => (a1,a2) 812 val (at,an) = dest_field_power a1 824 val (ac,bc) = hcf_power_conv2 f (a1,b1) 894 val (f,a1,b1) = dest_field_div x1
|
/seL4-l4v-master/HOL4/src/finite_maps/ |
H A D | fmapalTacs.sml | 38 some_some = |- !l2 l1 cmp b2 b1 a2 a1. 39 merge cmp ((a1,b1)::l1) ((a2,b2)::l2) = 40 case apto cmp a1 a2 of 41 LESS => (a1,b1)::merge cmp l1 ((a2,b2)::l2) 42 | EQUAL => (a1,b1)::merge cmp l1 l2 43 | GREATER => (a2,b2)::merge cmp ((a1,b1)::l1) l2 *)
|
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | problems.sml | 1101 ~(i a1 * a1 = i b1 * b1) \/ ~(i b2 * b2 * a2 = a2) \/ 1113 ~(i a1 * a1 = i b1 * b1) \/ ~(i b2 * b2 * a2 = a2) \/ 1133 ~(inverse a1 * a1 = inverse b1 * b1) \/ ~(inverse b2 * b2 * a2 = a2) \/
|
H A D | Term.sml | 128 | (Fn (f1,a1), Fn (f2,a2)) => 132 (case Int.compare (length a1, length a2) of 134 | EQUAL => cmp (a1 @ tms1) (a2 @ tms2)
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | problems.sml | 1101 ~(i a1 * a1 = i b1 * b1) \/ ~(i b2 * b2 * a2 = a2) \/ 1113 ~(i a1 * a1 = i b1 * b1) \/ ~(i b2 * b2 * a2 = a2) \/ 1133 ~(inverse a1 * a1 = inverse b1 * b1) \/ ~(inverse b2 * b2 * a2 = a2) \/
|
H A D | Term.sml | 128 | (Fn (f1,a1), Fn (f2,a2)) => 132 (case Int.compare (length a1, length a2) of 134 | EQUAL => cmp (a1 @ tms1) (a2 @ tms2)
|
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/ |
H A D | lisp_gcScript.sml | 1815 \\ `?a1 a2 a3 a4 a5. x = (a1,a2,a3,a4,a5)` by METIS_TAC [PAIR] 1819 \\ `ok_state (i,e,a2::TL rs,l,u,m) /\ a1 IN RANGE (if u then 1 + l else 1,i)` by 1823 \\ `(h' = a1) /\ (b a1 <> 0)` by METIS_TAC [ONE_ONE_DEF,ONTO_DEF,bijection_def] 1824 \\ `(a1 <> 0)` by METIS_TAC [ONE_ONE_DEF,ONTO_DEF,bijection_def] 1825 \\ `a1 IN RANGE (if u then 1 + l else 1,i)` by METIS_TAC [] 1839 \\ Q.EXISTS_TAC `reachables [b a1; FST q2; FST q3; FST q4; FST q5; FST q6] (ch_set h)` 1843 (Q.EXISTS_TAC `b a1` \\ FULL_SIMP_TAC std_ss [reachable_def] THENL [ 1853 \\ `a1 < [all...] |
/seL4-l4v-master/HOL4/src/pred_set/src/more_theories/ |
H A D | cardinalScript.sml | 470 [`a1`, `a2`, `s1`, `f1`, `s2`, `f2`] >> 472 qmatch_abbrev_tac `(XX1 = XX2) ==> (a1 = a2)` >> 473 `XX1 = f1 a1` 488 >- (`f1 a1 = f2 a1` by metis_tac[] >> 489 `a1 IN s2` by metis_tac [SUBSET_DEF] >> 806 ``(a1:'a1 set) =~ (a2:'a2 set) ==> 807 (b1:'b1 set) =~ (b2:'b2 set) ==> (a1 ** b1 =~ a2 ** b2)``, 824 `?a. a IN a1 /\ ( [all...] |
H A D | ordinalScript.sml | 1079 (!x y. x <= y ==> f x <= f y) /\ a1 < a2 /\ f a1 <= c /\ c < f a2 ==> 1080 ?b. a1 <= b /\ b < a2 /\ f b <= c /\ c < f b^+``, 1082 qabbrev_tac `mu = oleast a. c < f a /\ a1 < a` >> 1083 `c < f mu /\ a1 < mu /\ (!a. a < mu ==> f a <= c \/ a <= a1)` 1092 `d <= a1` by metis_tac[] >> 1093 `f d <= f a1` by metis_tac[] >> 1098 `a1 <= d` by metis_tac[ordlt_SUC_DISCRETE, ordle_lteq] >>
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/x64/model/ |
H A D | x64Script.sml | 7638 Let(Var("a1", 7663 Var("a1", 7682 Var("a1", 7702 Var("a1", 7833 Let(Var("a1", 7857 Var("a1", 7876 Var("a1", 8402 bVar"a1", 8433 bVar"a1", 8453 bVar"a1", [all...] |
/seL4-l4v-master/HOL4/examples/logic/ltl/ |
H A D | ltl2waaScript.sml | 52 rename [���(a1,e1) ��� trans �� f1���, ���a = a1 ��� a2���, ���(a2,e2) ��� trans �� f2���] 55 (a1 = BIGINTER a') ��� 101 >- (fs[d_conj_def] >> qexists_tac `{s}` >> qexists_tac `{a1 ��� ��}` 104 >- (`���a1' e1'. 105 ((a1 ��� �� = a1' ��� ��) ��� (e1 ��� {U f f'} = e1' ��� {U f f'})) ��� 106 (a1',e1') ��� trans �� f` suffices_by metis_tac[] 107 >> qexists_tac `a1` >> qexists_tac `e1` >> fs[]) 110 >> qexists_tac `{s}` >> qexists_tac `{a1 ��� a [all...] |
H A D | concrltl2waaScript.sml | 43 (FOLDR (��a1 l. (MAP (\b1. f a1 b1) m2) ++l) [] m1) 53 (FOLDR (��a1 l. (MAP (\b1. f a1 b1) m2) ++l) [] m1) 376 >- (`MEM (a1,e1) (MAP (concr2AbstractEdge aP) (trans_concr f))` 458 >- (Cases_on `(a1 ��� a2,e1 ��� e2) ��� trans (POW aP) f'` >> fs[] 459 >> `MEM (a1,e1) (MAP (concr2AbstractEdge aP) (trans_concr f))` 612 >- (`MEM (a1,e1) (MAP (concr2AbstractEdge aP) (trans_concr f'))` 644 >- (`MEM (a1,e1) (MAP (concr2AbstractEdge aP) (trans_concr f'))` 654 >> `a1 ��� a [all...] |
H A D | gbaSimplScript.sml | 13 trans_implies accTrans q (a1,q1) (a2,q2) 14 = (q1 = q2) ��� a2 ��� a1 15 ��� !t. t ��� accTrans ==> ((q,a2,q2) ��� t ==> (q,a1,q1) ��� t)`;
|
/seL4-l4v-master/HOL4/src/quotient/src/ |
H A D | quotientScript.sml | 1172 !a1 a2 b1 b2 c1 c2. 1173 (a1 = a2) /\ R b1 b2 /\ R c1 c2 1174 ==> R (COND a1 b1 c1) (COND a2 b2 c2)���), 1471 R a1 a2 /\ R b1 b2 ==> 1472 ((a1 = b1) ==> R a2 b2)���), 1484 (R a1 b1 ==> R a2 b2) ==> 1485 ((a1 = b1) ==> R a2 b2)���),
|
/seL4-l4v-master/HOL4/examples/lambda/basics/ |
H A D | generic_termsScript.sml | 1237 ���a1 a2 n bv r1 r2 ts us p. 1238 a1 ��� A ��� a1 ��� supp ppm p ��� a2 ��� A ��� a2 ��� GFVl ts ��� a2 ��� supp ppm p ��� 1241 genind vp lp n (GLAM a1 bv ts us) ==> 1242 (lf a2 bv (listpm (fn_pmact ppm dpm) [(a2,a1)] r1) r2 1243 (gtpml [(a2,a1)] ts) us p = 1244 lf a1 bv r1 r2 ts us p)
|
/seL4-l4v-master/HOL4/src/quotient/choice/ |
H A D | quotientScript.sml | 559 `(($+++ R1 R2) (INL (a1:'a)) (INL (a2:'a)) = R1 a1 a2) /\ 561 (($+++ R1 R2) (INL a1) (INR b2) = F) /\
|
/seL4-l4v-master/HOL4/examples/ARM/v7/eval/ |
H A D | emit_eval.sml | 524 fun mem_compare ((a1, _), (a2, _)) = 525 if a1 = a2 then 527 else if numML.< a1 a2 then
|
/seL4-l4v-master/HOL4/examples/diningcryptos/ |
H A D | basic_leakage_examplesScript.sml | 36 val (a1,f1) = t1 state handle HOL_ERR _ => ALL_TAC state value 37 in if length a1 = 0 then (a1,f1) else t2 state end;
|
/seL4-l4v-master/HOL4/examples/l3-machine-code/riscv/prog/ |
H A D | riscv_progLib.sml | 547 (2147580458, "15e1", "addi\ta1,a1,-8\r"), 555 (2147580522, "0005c703", "lbu\ta4,0(a1)\r"), 557 (2147580528, "0585", "addi\ta1,a1,1\r"),
|
/seL4-l4v-master/HOL4/src/parse/ |
H A D | type_grammar.sml | 133 (INFIX(rlist1, a1), INFIX(rlist2, a2)) => let 135 if a1 = a2 then INFIX(Lib.union rlist1 rlist2, a1)
|
/seL4-l4v-master/HOL4/src/sort/ |
H A D | sortingScript.sml | 562 (`!P L a1 a2 l1 l2. 563 ((a1,a2) = PART P L l1 l2) 565 PERM (L ++ (l1 ++ l2)) (a1 ++ a2)`, 580 `!P L a1 a2 l1 l2. 581 ((a1,a2) = PART P L l1 l2) 583 !x. MEM x (L ++ (l1 ++ l2)) = MEM x (a1 ++ a2)`,
|