Searched refs:a1 (Results 1 - 25 of 249) sorted by relevance

12345678910

/seL4-l4v-master/HOL4/examples/dev/sw/working/0.1/
H A DILTheory.sig180 (?a0 a1.
182 (\a0 a1.
184 (FCONS a0 (FCONS a1 (\n. BOTTOM)))) a0 a1) /\
185 'CTL_STRUCTURE' a0 /\ 'CTL_STRUCTURE' a1) \/
186 (?a0 a1 a2.
188 (\a0 a1 a2.
190 (FCONS a1 (FCONS a2 (\n. BOTTOM)))) a0 a1 a2) /\
191 'CTL_STRUCTURE' a1 /\ 'CTL_STRUCTUR
[all...]
/seL4-l4v-master/l4v/tools/c-parser/testfiles/
H A Djiraver443a.c16 static int a1; variable
22 return &a1;
/seL4-l4v-master/HOL4/examples/STE/Examples/
H A DAnd.sml22 val a1 = (T, "i0", ``v1:bool``, 0, 1); value
25 val A = TF [a1, a2];
34 val a1 = (T, "i0", ``v1:bool``, 0, 1); value
36 val A = TF [a1];
44 val a1 = (T, "i0", ``v1:bool``, 0, 1); value
47 val A = TF [a1,a2];
H A DOr.sml21 val a1 = (T, "i0", ``v1:bool``, 0, 1); value
24 val A = TF [a1, a2];
34 val a1 = (T, "i0", ``v1:bool``, 0, 1); value
36 val A = TF [a1];
47 val a1 = (T, "i0", ``v1:bool``, 0, 1); value
50 val A = TF [a1,a2];
H A DComparator.sml17 else if (node = "a1") then X
22 (Xnor (s "a1")(s "b1"))
29 (s_b' node = (s_b "a0" = s_b "b0") /\ (s_b "a1" = s_b "b1"))`;
49 THEN Cases_on `s_b "a1"`
75 THEN FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a1"``)
81 THEN Cases_on `s "a1"` THEN Cases_on `s' "a1"`
96 val a1 = (T, "a1", ``a1 value
116 val a1 = (T, "a1", ``T:bool``, 0, 1); value
136 val a1 = (T, "a1", ``a1:bool``, 0, 1); value
156 val a1 = (T, "a1", ``v1:bool``, 0, 1); value
176 val a1 = (T, "a1", ``T:bool``, 0, 1); value
196 val a1 = (T, "a1", ``F:bool``, 0, 1); value
216 val a1 = (T, "a1", ``F:bool``, 0, 1); value
236 val a1 = (T, "a1", ``F:bool``, 0, 1); value
[all...]
H A DComparator-for-STE-Reduction.sml27 else if (node = "a1") then X
35 Xnor (s "a1")(s "b1")
40 (Xnor (s "a1")(s "b1"))
56 else if (node = "a1") then X
60 else if (node = "i1") then Xnor (s "a1")(s "b1")
84 val a1 = (T, "a1", ``a1:bool``, 0, 1); value
87 val out = (T, "out", ``xnor a0 b0 /\ xnor a1 b1``, 1, 2);
88 val A = TF [a0,a1,b
[all...]
H A DMux.sml18 else if (node = "a1") then X
32 (And (s "a1")(s "ctrl"))
45 (s_b' "out1" = s_b "a1")
86 THENL [fl [] THEN Cases_on `s_b "a1"`
92 fl [] THEN Cases_on `s_b "a1"`
124 FIRST_ASSUM(STRIP_ASSUME_TAC o SPEC ``"a1"``)
127 THEN Cases_on `s "a1"` THEN Cases_on `s' "a1"`
141 val a1 = (T, "a1", value
166 val a1 = (T, "a1", ``va1:bool``, 0, 1); value
189 val a1 = (T, "a1", ``va1:bool``, 0, 1); value
[all...]
/seL4-l4v-master/HOL4/src/rational/
H A DfracScript.sml91 * |- !a1 b1 a2 b2. 0<b1 ==> 0<b2 ==>
92 * ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) )
99 ``!a1 b1 a2 b2. 0i < b1 ==> 0i < b2 ==>
100 ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) )``,
125 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
126 * (~(abs_frac(a1,b1) = abs_frac(a2,b2)) = ~(a1=a2) \/ ~(b1=b2))
129 val FRAC_NOT_EQ = store_thm("FRAC_NOT_EQ", ``!a1 b
[all...]
H A DfracLib.sml29 * (abs_frac (a1,b1) = abs_frac (a2,b2)
31 * 0<b1, 0<b2 |- (abs_frac (a1,b1) = abs_frac (a1,b1))
32 * = (a1 = a2) /\ (b1 = b2) : thm
41 val (a1,b1) = dest_pair lha; value
44 UNDISCH_ALL (SPECL[a1,b1,a2,b2] FRAC_EQ)
51 * ~((abs_frac (a1,b1) = abs_frac (a2,b2))
53 * 0<b1, 0<b2 |- ~(abs_frac (a1,b1) = abs_frac (a2,b2))
54 * = ~(a1 = a2) \/ ~(b1 = b2)
63 val (a1,b value
83 val (a1,b1) = dest_pair lha; value
273 (filter (fn x => let val (a1,a2,a3) = x in a1 ~~ frac_nmr_tm end) value
277 (filter (fn x => let val (a1,a2,a3) = x in a1 ~~ frac_dnm_tm end) value
550 val (a1,b1) = dest_pair args; value
[all...]
/seL4-l4v-master/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dinfinite_pathScript.sml311 ``!t v a1 a2. (EQUIV_ON_PATH_RESTN t v a1 a2) =
312 (IMP_ON_PATH_RESTN t v a1 a2 /\ IMP_ON_PATH_RESTN t v a2 a1)``,
438 ``!v t a1 a2. NOT_ON_PATH_RESTN t v a1 ==> IMP_ON_PATH_RESTN t v a1 a2``,
447 ``!v t a1 a2. NOT_ON_PATH_RESTN t v a2 ==> BEFORE_ON_PATH_RESTN_STRONG t v a1 a2``,
456 ``!v t t2 a1 a
[all...]
H A DrltlScript.sml455 ``!f v a1 a2 r t. (PROP_LOGIC_EQUIVALENT a1 a2) ==>
456 (((RLTL_SEM_TIME t v a1 r f) = (RLTL_SEM_TIME t v a2 r f)) /\
457 ((RLTL_SEM_TIME t v r a1 f) = (RLTL_SEM_TIME t v r a2 f)))``,
463 `(!s. P_SEM s (P_OR (a1,P_AND (p_2,P_NOT r))) = P_SEM s (P_OR (a2,P_AND (p_2,P_NOT r)))) /\
464 (!s. P_SEM s (P_OR (r,P_AND (p_2,P_NOT a1))) = P_SEM s (P_OR (r,P_AND (p_2,P_NOT a2))))`
473 ``!f v a1 a2 r1 r2 t. (PROP_LOGIC_EQUIVALENT a1 a2) ==>
475 ((RLTL_SEM_TIME t v a1 r1 f) = (RLTL_SEM_TIME t v a2 r2 f))``,
705 ``!f t v a1 a
[all...]
H A Dautomaton_formulaScript.sml265 `A_USED_STATE_VARS_COMPATIBLE a1 a2 =
266 (DISJOINT (A_USED_INPUT_VARS a1) (A_USED_STATE_VARS a2) /\
267 DISJOINT (A_USED_INPUT_VARS a2) (A_USED_STATE_VARS a1) /\
268 DISJOINT (A_USED_STATE_VARS a1) (A_USED_STATE_VARS a2))`;
272 !a1 a2. VARDISJOINT_AUTOMATON_FORMULA (A_AND(a1, a2)) ==>
273 A_USED_STATE_VARS_COMPATIBLE a1 a2
285 `AUTOMATON_EQUIV a1 a2 = !v. A_SEM v a1 <=> A_SEM v a2`;
290 (!a1 a
[all...]
/seL4-l4v-master/HOL4/src/new-datatype/
H A DNDSupportScript.sml21 (sum_retrieve f1 _ (INL a1) (b1, _) = f1 a1 b1)
25 (prod_retrieve f1 _ (a1, _) (INL b1) = f1 a1 b1)
/seL4-l4v-master/HOL4/examples/lambda/other-models/
H A DdiagsScript.sml24 (!a1 a2 n b ty. (n, a1, a2, b, ty) IN Fa ==>
25 liftrel b ty (R n) (f a1) (f a2)) ==>
27 (!a1 a2 n b ty. (n, INL a1, INL a2, b, ty) IN G ==>
28 liftrel b ty (R n) (f a1) (f a2)) /\
249 ?a1 a2. R1 a1 a2 /\ (b1 = f a1) /\ (b2 = f a2)
317 `!n a1 a
[all...]
/seL4-l4v-master/HOL4/src/compute/examples/
H A DSort.sml22 | Tas2Ln (Br (n,a1,a2)) = n::(fusion (Tas2Ln a1) (Tas2Ln a2))
26 | insTas (Br(m,a1,a2)) n =
27 if (inf_egal n m) then Br(n,a2,insTas a1 m) else Br(m,a2,insTas a1 n)
H A DMergeSort.sml51 /\ (Tree2List (Nd n a1 a2) = n :: merge (Tree2List a1) (Tree2List a2)) `
56 /\ (insTree (Nd m a1 a2) n =
57 if (le_nat n m) then Nd n a2 (insTree a1 m)
58 else Nd m a2 (insTree a1 n)) `
/seL4-l4v-master/HOL4/src/combin/
H A Dcombinpp.sml12 fun cAPP l (a1, a2) = Absyn.APP(l,a1,a2)
16 APP(l, a1, a2) =>
17 (case a1 of
26 SOME(l, a1, a2) => (a1,a2)
60 | APP(l,a1,a2) =>
62 NONE => APP(l, upd_processor G a1, upd_processor G a2)
/seL4-l4v-master/seL4/include/arch/riscv/arch/
H A Dsbi.h54 register register_t a1 asm("a1") = arg_1;
60 : "r"(a0), "r"(a1), "r"(a2), "r"(a7)
/seL4-l4v-master/seL4/include/arch/riscv/arch/machine/
H A Dregisterset.h38 a1 = 10, msgInfoRegister = 10, enumerator in enum:_register
143 [seL4_UnknownSyscall_A1] = a1,\
170 [seL4_TimeoutReply_a1] = a1, \
/seL4-l4v-master/seL4/src/arch/riscv/machine/
H A Dregisterset.c29 a0, a1, a2, a3, a4, a5, a6, a7,
/seL4-l4v-master/HOL4/src/quotient/src/
H A Dquotient_sumScript.sml59 `(($+++ R1 R2) (INL (a1:'a)) (INL (a2:'a)) = R1 a1 a2) /\
61 (($+++ R1 R2) (INL a1) (INR b2) = F) /\
160 !a1 a2.
161 R1 a1 a2 ==>
162 (R1 +++ R2) (INL a1) (INL a2)���),
212 !a1 a2.
213 (R1 +++ R2) a1 a2 ==>
214 (ISL a1 = ISL a2)���),
237 !a1 a
[all...]
/seL4-l4v-master/HOL4/examples/acl2/examples/M1/
H A Dcomplex_rationalScript.sml67 `COMPLEX_ADD (com a1 b1) (com a2 b2) =
68 com (a1+a2) (b1+b2)`;
80 `COMPLEX_SUB (com a1 b1) (com a2 b2) =
81 com (a1-a2) (b1-b2)`;
93 `COMPLEX_MULT (com a1 b1) (com a2 b2) =
94 com ((a1*a2)-(b1*b2)) ((b1*a2)+(a1*b2))`;
/seL4-l4v-master/HOL4/examples/acl2/examples/acl2-hol-ltl-paper-example/
H A Dcomplex_rationalScript.sml67 `COMPLEX_ADD (com a1 b1) (com a2 b2) =
68 com (a1+a2) (b1+b2)`;
80 `COMPLEX_SUB (com a1 b1) (com a2 b2) =
81 com (a1-a2) (b1-b2)`;
93 `COMPLEX_MULT (com a1 b1) (com a2 b2) =
94 com ((a1*a2)-(b1*b2)) ((b1*a2)+(a1*b2))`;
/seL4-l4v-master/HOL4/examples/acl2/ml/
H A Dcomplex_rationalScript.sml67 `COMPLEX_ADD (com a1 b1) (com a2 b2) =
68 com (a1+a2) (b1+b2)`;
80 `COMPLEX_SUB (com a1 b1) (com a2 b2) =
81 com (a1-a2) (b1-b2)`;
93 `COMPLEX_MULT (com a1 b1) (com a2 b2) =
94 com ((a1*a2)-(b1*b2)) ((b1*a2)+(a1*b2))`;
/seL4-l4v-master/HOL4/examples/elliptic/
H A Delliptic_exampleScript.sml230 let a1 = ex1_field_elt example1_curve.a1 in
236 let y = ~y1 - a1 * x1 - a3
248 let a1 = ex1_field_elt example1_curve.a1 in
256 let d = & 2 * y1 + a1 * x1 + a3
259 let l = (& 3 * x1 ** 2w + & 2 * a2 * x1 + a4 - a1 * y1) / d in
261 let x = l ** 2w + a1 * l - a2 - &2 * x1 in
262 let y = ~(l + a1) * x - m - a3
276 let a1
[all...]

Completed in 215 milliseconds

12345678910