Searched refs:a1 (Results 126 - 150 of 249) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/Crypto/RC6/
H A DRC6Script.sml296 `!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 DunifyTools.sml188 (COMB (a1, b1), COMB (a2, b2)) =>
190 val s1 = ((bvs1, a1), (bvs2, a2))
/seL4-l4v-master/HOL4/examples/AI_tasks/
H A DmleCombinLib.sml50 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 Dselftest.sml169 ([a1], [a2]) => aconv a1 asm andalso aconv a2 asm
/seL4-l4v-master/HOL4/examples/elliptic/
H A DfieldTools.sml802 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 DfmapalTacs.sml38 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 Dproblems.sml1101 ~(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 DTerm.sml128 | (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 Dproblems.sml1101 ~(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 DTerm.sml128 | (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 Dlisp_gcScript.sml1815 \\ `?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 DcardinalScript.sml470 [`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 DordinalScript.sml1079 (!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 Dx64Script.sml7638 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 Dltl2waaScript.sml52 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 Dconcrltl2waaScript.sml43 (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 DgbaSimplScript.sml13 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 DquotientScript.sml1172 !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 Dgeneric_termsScript.sml1237 ���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 DquotientScript.sml559 `(($+++ 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 Demit_eval.sml524 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 Dbasic_leakage_examplesScript.sml36 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 Driscv_progLib.sml547 (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 Dtype_grammar.sml133 (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 DsortingScript.sml562 (`!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)`,

Completed in 366 milliseconds

12345678910