Searched refs:b2 (Results 1 - 25 of 258) sorted by relevance

1234567891011

/seL4-l4v-master/l4v/tools/c-parser/testfiles/
H A Djiraver254.c13 int g(_Bool b2) argument
15 return b2 > 3;
H A Dparse_addr.c19 int b2[10][10]; variable
33 int z = *f(b2[3]);
/seL4-l4v-master/HOL4/src/bag/
H A Dselftest.sml5 ���b5 + (b1: 'a bag) + b2 + b4 - (b2 + b1)���,
8 ���b5 + (b1: 'a bag) + b2 + b4 = b2 + b6 + b1���, ���(b4:'a bag) + b5 = b6���),
10 ���SUB_BAG b2 (b5 + (b1: 'a bag) + b2 + b4)���, ���{||} <= b1 + b4 + b5���)
H A DbagScript.sml32 `SUB_BAG b1 b2 = !x n. BAG_INN x n b1 ==> BAG_INN x n b2`);
36 `PSUB_BAG b1 b2 <=> SUB_BAG b1 b2 /\ ~(b1 = b2)`);
61 ``BAG_DIFF b1 (b2:'a bag) = \x. b1 x - b2 x``);
87 `BAG_INTER b1 b2 = (\x. if (b1 x < b2 x) then b1 x else b2
[all...]
H A DprimeFactorScript.sml96 (* can show p divides BAG_PROD b2, so p is also in b2 (because p is prime). *)
97 (* Let b1' = b1-p and b2' = b2-p. Then b1' = b2', by induction hypothesis. *)
98 (* Thus b1=b2. The argument uses a lemma derived from gcdTheory.P_EUCLIDES, *)
104 ``!n b1 b2.
106 (FINITE_BAG b2 /\ (!m. BAG_IN m b2 ==> prime m) /\ (n=BAG_GEN_PROD b2
[all...]
H A DbagSimpleLib.sml118 val (b1,b2) = dest_union b;
120 val t2 = mk_image (f, b2)
125 val finite_thm = EQ_MP (GSYM (ISPECL [b1,b2] bagTheory.FINITE_BAG_UNION))
127 val bag_thm' = MP (ISPECL [b1,b2,f] bagTheory.BAG_IMAGE_FINITE_UNION) finite_thm12
182 val (b1,b2) = dest_union b;
184 val (finite_thm2, card_thm2) = BAG_CARD_CONV___FINITE b2;
187 val finite_thm = EQ_MP (GSYM (ISPECL [b1,b2] bagTheory.FINITE_BAG_UNION))
189 val card_thm' = MP (ISPECL [b1,b2] bagTheory.BAG_CARD_UNION) finite_thm12
284 fun get_resort_lists___pred_pair p b1 b2 =
287 val l2 = fst (strip_insert b2);
[all...]
/seL4-l4v-master/HOL4/examples/HolCheck/examples/
H A Dmod16Script.sml79 val MOD16_PROJ_def = Define `MOD16_PROJ (b3,b2,b1,b0) i = if i = 0 then b0 else if i=1 then b1 else if i=2 then b2 else b3`
82 `MOD16_N2B' n k (b3,b2,b1,b0) =
85 else (if n >= 2**k then MOD16_PROJ (b3,b2,b1,b0) k else ~(MOD16_PROJ (b3,b2,b1,b0) k)) /\
86 MOD16_N2B' (if n >= 2**k then n-(2**k) else n) (k-1) (b3,b2,b1,b0)`;
91 val MOD16_N2B_def = Define `MOD16_N2B n (b3,b2,b1,b0) = MOD16_N2B' n 3 (b3,b2,b1,b0)`
93 val MOD16_N2B_15 = save_thm("MOD16_N2B_15",prove(``!b3 b2 b0 b1. MOD16_N2B 15 (b3,b2,b
[all...]
/seL4-l4v-master/HOL4/examples/dev/AES/curried/
H A DMultScript.sml41 `xtime (BYTE b7 b6 b5 b4 b3 b2 b1 b0)
43 if b7 then (BYTE b6 b5 b4 (~b3) (~b2) b1 (~b0) T)
44 else (BYTE b6 b5 b4 b3 b2 b1 b0 F)`;
62 `b1 ** b2 =
65 then b2 # (RightShift b1 ** xtime b2)
66 else (RightShift b1 ** xtime b2)`,
90 `IterConstMult (b1,b2,acc) =
91 if b1 = ZERO then (b1,b2,acc)
92 else IterConstMult (RightShift b1, xtime b2,
[all...]
H A Dword8Script.sml32 `(!x:word8. P x) = !b7 b6 b5 b4 b3 b2 b1 b0. P(BYTE b7 b6 b5 b4 b3 b2 b1 b0)`,
139 `BYTE_TO_NUM (BYTE b7 b6 b5 b4 b3 b2 b1 b0) =
141 16*B2N(b4) + 8*B2N(b3) + 4*B2N(b2) + 2*B2N(b1) + B2N(b0)`;
173 `LeftShift (BYTE b7 b6 b5 b4 b3 b2 b1 b0) = BYTE b6 b5 b4 b3 b2 b1 b0 F`;
176 `RightShift (BYTE b7 b6 b5 b4 b3 b2 b1 b0) = BYTE F b7 b6 b5 b4 b3 b2 b1`;
184 of (BYTE b7 b6 b5 b4 b3 b2 b1 b0) -> BYTE b6 b5 b4 b3 b2 b
[all...]
/seL4-l4v-master/HOL4/examples/dev/AES/tupled/
H A DMultScript.sml41 `xtime ((b7,b6,b5,b4,b3,b2,b1,b0) :word8)
43 if b7 then (b6,b5,b4,~b3,~b2,b1,~b0,T)
44 else (b6,b5,b4,b3,b2,b1,b0,F)`;
62 `b1 ** b2 =
65 then b2 # (RightShift b1 ** xtime b2)
66 else (RightShift b1 ** xtime b2)`,
91 `IterConstMult (b1,b2,acc) =
92 if b1 = ZERO then (b1,b2,acc)
93 else IterConstMult (RightShift b1, xtime b2,
[all...]
H A Dword8Script.sml29 `(!x:word8. P x) = !b7 b6 b5 b4 b3 b2 b1 b0. P(b7,b6,b5,b4,b3,b2,b1,b0)`,
133 `BYTE_TO_NUM (b7,b6,b5,b4,b3,b2,b1,b0) =
135 16*B2N(b4) + 8*B2N(b3) + 4*B2N(b2) + 2*B2N(b1) + B2N(b0)`;
167 `LeftShift (b7,b6,b5,b4,b3,b2,b1,b0):word8 = (b6,b5,b4,b3,b2,b1,b0,F)`;
170 `RightShift (b7,b6,b5,b4,b3,b2,b1,b0):word8 = (F,b7,b6,b5,b4,b3,b2,b1)`;
188 (b7,b6,b5,b4,b3,b2,b1,b0) =
199 (case BIT_COMPARE a2 b2
[all...]
/seL4-l4v-master/HOL4/examples/temporal_deep/src/translations/
H A DtranslationsLibScript.sml63 (* |- !b1 b2 DS l pf.
65 (l,b1,b2,pf) IN DS.B ==>
68 ((LTL_NOT l,b2,b1,(\sv. P_NOT (pf sv))) INSERT DS.B))
175 (prove (``!b1 b2 p.
178 {(LTL_PROP p,b1,b2,(\sv. p))} (P_USED_VARS p))``,
185 !b1 b2 DS l pf.
187 (DS.B = {(l,b2,b1,pf)}) ==>
190 {(LTL_NOT l,b1,b2,(\sv. P_NOT (pf sv)))})``,
194 Q_SPECL_NO_ASSUM 0 [`b2`, `b1`, `DS`, `l`, `pf`] THEN
207 !b1 b2 DS
[all...]
H A DtranslationsLib.sml72 fun getBindingFor b1 b2 l [] = (false, false, ``dummy:num``)
73 | getBindingFor b1 b2 l (h::l1) =
78 if ((l' ~~ l) andalso ((not b1) orelse a1) andalso ((not b2) orelse a2)) then
81 getBindingFor b1 b2 l l1
178 fun ltl2omega_internal2 b1 b2 l dsThm TSPECL =
189 fun addBindingFor b1 b2 l dsThm =
192 val (b1', b2', pf) = getBindingFor b1 b2 l dsB;
194 if (b1' orelse b2') then (b1', b2', p
[all...]
/seL4-l4v-master/HOL4/examples/temporal_deep/src/deep_embeddings/
H A Dxprop_logicScript.sml38 (XP_USED_CURRENT_VARS (XP_AND(b1,b2)) =
39 (XP_USED_CURRENT_VARS b1) UNION (XP_USED_CURRENT_VARS b2))`;
46 (XP_USED_X_VARS (XP_AND(b1,b2)) = (XP_USED_X_VARS b1) UNION (XP_USED_X_VARS b2))`;
56 (XP_VAR_RENAMING f (XP_AND(b1,b2)) = XP_AND(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2))`;
68 (XP_SEM (XP_AND (b1,b2)) (s1, s2) = ((XP_SEM b1 (s1, s2)) /\ (XP_SEM b2 (s1, s2))))`;
81 `XP_OR(b1, b2) = XP_NOT(XP_AND(XP_NOT b1, XP_NOT b2))`;
[all...]
H A Dprop_logicScript.sml39 (P_SEM s (P_AND(b1,b2)) = (P_SEM s b1 /\ P_SEM s b2))`;
49 `P_OR (b1, b2) = P_NOT (P_AND (P_NOT b1, P_NOT b2))`;
52 `P_IMPL (b1, b2) = P_OR (P_NOT b1, b2)`;
55 `P_COND (c, b1, b2) = P_AND (P_IMPL (c, b1), P_IMPL (P_NOT c, b2))`;
58 `P_EQUIV (b1, b2) = P_AND (P_IMPL (b1, b2), P_IMP
[all...]
/seL4-l4v-master/HOL4/examples/hfs/
H A DhfbScript.sml10 (���x1 x2 b1 b2.
11 hfb0_equiv x1 x2 ��� hfb0_equiv b1 b2 ���
12 hfb0_equiv (HF_I x1 b1) (HF_I x2 b2)) ���
/seL4-l4v-master/HOL4/src/new-datatype/
H A DNDSupportScript.sml22 /\ (sum_retrieve _ f2 (INR a2) (_, b2) = f2 a2 b2)`;
26 /\ (prod_retrieve _ f2 (_, a2) (INR b2) = f2 a2 b2)`;
/seL4-l4v-master/HOL4/examples/dev/AES/word8/
H A DMultScript.sml45 `b1 ** b2 =
48 then b2 ?? ((b1 >>> 1) ** xtime b2)
49 else ((b1 >>> 1) ** xtime b2)`,
70 `IterConstMult (b1,b2,acc) =
71 if b1 = 0w:word8 then (b1,b2,acc)
72 else IterConstMult (b1 >>> 1, xtime b2,
73 if word_lsb b1 then (b2 ?? acc) else acc)`;
89 `!b1 b2 acc. (b1 ** b2)
[all...]
/seL4-l4v-master/HOL4/examples/Crypto/AES/
H A DMultScript.sml44 `b1 ** b2 =
47 then b2 ?? ((b1 >>> 1) ** xtime b2)
48 else ((b1 >>> 1) ** xtime b2)`;
66 `IterConstMult (b1,b2,acc) =
67 if b1 = 0w:word8 then (b1,b2,acc)
68 else IterConstMult (b1 >>> 1, xtime b2,
69 if word_lsb b1 then (b2 ?? acc) else acc)`;
79 `!b1 b2 acc. (b1 ** b2)
[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
[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
42 val (a2,b2) = dest_pair rha;
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)
64 val (a2,b2)
553 val b2 = ``& ^b2x + 1i``; value
[all...]
/seL4-l4v-master/HOL4/src/num/arith/src/
H A DNorm_ineqs.sml102 (let val (c,b1,b2) =
104 in if (coeff1 = coeff2) then ((name1,coeff1)::c,b1,b2)
106 ((name1,coeff1)::c,b1,(name1,coeff2 - coeff1)::b2)
109 b2)
112 (let val (c,b1,b2) =
114 in (c,(name1,coeff1)::b1,b2)
116 else (let val (c,b1,b2) =
118 in (c,b1,(name2,coeff2)::b2)
/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/
H A Ddataabs.ml89 "!n b1 b2.
91 isBus n b2
93 !t1 t2. (b1 t1 = b2 t2) = (!m. m <= n ==> (b1 t1 m = b2 t2 m))",
H A Dtoplevel.ml39 ?phiA w1 b1 b2.
42 DISPLAY n (phiA,b2,display) /\
43 COUNT_IMP n (phiA,w1,b1,b2) /\
45 isBus n b2");;
90 WordVal n(WordAbs((b2 when (isHi phiA))((n' + sysinit) + 1)))";;
/seL4-l4v-master/HOL4/examples/machine-code/garbage-collectors/
H A Darm_improved_gcScript.sml188 ``~(RANGE (b2,e2) j) ==>
189 (ref_mem ((j =+ x) m) b2 e2 = ref_mem m b2 e2)``,
190 completeInduct_on `e2-b2` \\ REPEAT STRIP_TAC
192 \\ Cases_on `e2<=b2` \\ ASM_SIMP_TAC std_ss []
193 \\ `~(b2 = j)` by (FULL_SIMP_TAC std_ss [RANGE_def] \\ DECIDE_TAC)
195 \\ Q.ABBREV_TAC `y = MAX 1 (getLENGTH (m b2))`
197 \\ `e2 - (b2 + y) < e2 - b2` by DECIDE_TAC
198 \\ `~RANGE (b2
[all...]

Completed in 145 milliseconds

1234567891011