1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "num/bitrigesim.ma".
24 include "num/bool_lemmas.ma".
30 ndefinition bitrigesim_destruct_aux ≝
31 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
32 match eq_bit t1 t2 with [ true ⇒ P → P | false ⇒ P ].
34 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
42 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
45 ##[ ##1: #t2; nelim t2; nnormalize; napply refl_eq
46 ##| ##2: #t2; nelim t2; nnormalize; napply refl_eq
47 ##| ##3: #t2; nelim t2; nnormalize; napply refl_eq
48 ##| ##4: #t2; nelim t2; nnormalize; napply refl_eq
49 ##| ##5: #t2; nelim t2; nnormalize; napply refl_eq
50 ##| ##6: #t2; nelim t2; nnormalize; napply refl_eq
51 ##| ##7: #t2; nelim t2; nnormalize; napply refl_eq
52 ##| ##8: #t2; nelim t2; nnormalize; napply refl_eq
53 ##| ##9: #t2; nelim t2; nnormalize; napply refl_eq
54 ##| ##10: #t2; nelim t2; nnormalize; napply refl_eq
55 ##| ##11: #t2; nelim t2; nnormalize; napply refl_eq
56 ##| ##12: #t2; nelim t2; nnormalize; napply refl_eq
57 ##| ##13: #t2; nelim t2; nnormalize; napply refl_eq
58 ##| ##14: #t2; nelim t2; nnormalize; napply refl_eq
59 ##| ##15: #t2; nelim t2; nnormalize; napply refl_eq
60 ##| ##16: #t2; nelim t2; nnormalize; napply refl_eq
61 ##| ##17: #t2; nelim t2; nnormalize; napply refl_eq
62 ##| ##18: #t2; nelim t2; nnormalize; napply refl_eq
63 ##| ##19: #t2; nelim t2; nnormalize; napply refl_eq
64 ##| ##20: #t2; nelim t2; nnormalize; napply refl_eq
65 ##| ##21: #t2; nelim t2; nnormalize; napply refl_eq
66 ##| ##22: #t2; nelim t2; nnormalize; napply refl_eq
67 ##| ##23: #t2; nelim t2; nnormalize; napply refl_eq
68 ##| ##24: #t2; nelim t2; nnormalize; napply refl_eq
69 ##| ##25: #t2; nelim t2; nnormalize; napply refl_eq
70 ##| ##26: #t2; nelim t2; nnormalize; napply refl_eq
71 ##| ##27: #t2; nelim t2; nnormalize; napply refl_eq
72 ##| ##28: #t2; nelim t2; nnormalize; napply refl_eq
73 ##| ##29: #t2; nelim t2; nnormalize; napply refl_eq
74 ##| ##30: #t2; nelim t2; nnormalize; napply refl_eq
75 ##| ##31: #t2; nelim t2; nnormalize; napply refl_eq
76 ##| ##32: #t2; nelim t2; nnormalize; napply refl_eq
80 nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2.
81 #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
84 nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2.
85 #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
88 nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2.
89 #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
92 nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2.
93 #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
96 nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2.
97 #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
100 nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2.
101 #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
104 nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2.
105 #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
108 nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2.
109 #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
112 nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2.
113 #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
116 nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2.
117 #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
120 nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2.
121 #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
124 nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2.
125 #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
128 nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2.
129 #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
132 nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2.
133 #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
136 nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2.
137 #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
140 nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2.
141 #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
144 nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2.
145 #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
148 nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2.
149 #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
152 nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2.
153 #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
156 nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2.
157 #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
160 nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2.
161 #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
164 nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2.
165 #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
168 nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2.
169 #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
172 nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2.
173 #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
176 nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2.
177 #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
180 nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2.
181 #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
184 nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2.
185 #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
188 nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2.
189 #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
192 nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2.
193 #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
196 nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2.
197 #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
200 nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2.
201 #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
204 nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2.
205 #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
208 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
210 ##[ ##1: napply eqbit_to_eq1 ##| ##2: napply eqbit_to_eq2
211 ##| ##3: napply eqbit_to_eq3 ##| ##4: napply eqbit_to_eq4
212 ##| ##5: napply eqbit_to_eq5 ##| ##6: napply eqbit_to_eq6
213 ##| ##7: napply eqbit_to_eq7 ##| ##8: napply eqbit_to_eq8
214 ##| ##9: napply eqbit_to_eq9 ##| ##10: napply eqbit_to_eq10
215 ##| ##11: napply eqbit_to_eq11 ##| ##12: napply eqbit_to_eq12
216 ##| ##13: napply eqbit_to_eq13 ##| ##14: napply eqbit_to_eq14
217 ##| ##15: napply eqbit_to_eq15 ##| ##16: napply eqbit_to_eq16
218 ##| ##17: napply eqbit_to_eq17 ##| ##18: napply eqbit_to_eq18
219 ##| ##19: napply eqbit_to_eq19 ##| ##20: napply eqbit_to_eq20
220 ##| ##21: napply eqbit_to_eq21 ##| ##22: napply eqbit_to_eq22
221 ##| ##23: napply eqbit_to_eq23 ##| ##24: napply eqbit_to_eq24
222 ##| ##25: napply eqbit_to_eq25 ##| ##26: napply eqbit_to_eq26
223 ##| ##27: napply eqbit_to_eq27 ##| ##28: napply eqbit_to_eq28
224 ##| ##29: napply eqbit_to_eq29 ##| ##30: napply eqbit_to_eq30
225 ##| ##31: napply eqbit_to_eq31 ##| ##32: napply eqbit_to_eq32
229 nlemma eq_to_eqbit1 : ∀t2.t00 = t2 → eq_bit t00 t2 = true.
230 #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
233 nlemma eq_to_eqbit2 : ∀t2.t01 = t2 → eq_bit t01 t2 = true.
234 #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
237 nlemma eq_to_eqbit3 : ∀t2.t02 = t2 → eq_bit t02 t2 = true.
238 #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
241 nlemma eq_to_eqbit4 : ∀t2.t03 = t2 → eq_bit t03 t2 = true.
242 #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
245 nlemma eq_to_eqbit5 : ∀t2.t04 = t2 → eq_bit t04 t2 = true.
246 #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
249 nlemma eq_to_eqbit6 : ∀t2.t05 = t2 → eq_bit t05 t2 = true.
250 #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
253 nlemma eq_to_eqbit7 : ∀t2.t06 = t2 → eq_bit t06 t2 = true.
254 #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
257 nlemma eq_to_eqbit8 : ∀t2.t07 = t2 → eq_bit t07 t2 = true.
258 #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
261 nlemma eq_to_eqbit9 : ∀t2.t08 = t2 → eq_bit t08 t2 = true.
262 #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
265 nlemma eq_to_eqbit10 : ∀t2.t09 = t2 → eq_bit t09 t2 = true.
266 #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
269 nlemma eq_to_eqbit11 : ∀t2.t0A = t2 → eq_bit t0A t2 = true.
270 #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
273 nlemma eq_to_eqbit12 : ∀t2.t0B = t2 → eq_bit t0B t2 = true.
274 #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
277 nlemma eq_to_eqbit13 : ∀t2.t0C = t2 → eq_bit t0C t2 = true.
278 #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
281 nlemma eq_to_eqbit14 : ∀t2.t0D = t2 → eq_bit t0D t2 = true.
282 #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
285 nlemma eq_to_eqbit15 : ∀t2.t0E = t2 → eq_bit t0E t2 = true.
286 #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
289 nlemma eq_to_eqbit16 : ∀t2.t0F = t2 → eq_bit t0F t2 = true.
290 #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
293 nlemma eq_to_eqbit17 : ∀t2.t10 = t2 → eq_bit t10 t2 = true.
294 #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
297 nlemma eq_to_eqbit18 : ∀t2.t11 = t2 → eq_bit t11 t2 = true.
298 #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
301 nlemma eq_to_eqbit19 : ∀t2.t12 = t2 → eq_bit t12 t2 = true.
302 #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
305 nlemma eq_to_eqbit20 : ∀t2.t13 = t2 → eq_bit t13 t2 = true.
306 #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
309 nlemma eq_to_eqbit21 : ∀t2.t14 = t2 → eq_bit t14 t2 = true.
310 #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
313 nlemma eq_to_eqbit22 : ∀t2.t15 = t2 → eq_bit t15 t2 = true.
314 #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
317 nlemma eq_to_eqbit23 : ∀t2.t16 = t2 → eq_bit t16 t2 = true.
318 #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
321 nlemma eq_to_eqbit24 : ∀t2.t17 = t2 → eq_bit t17 t2 = true.
322 #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
325 nlemma eq_to_eqbit25 : ∀t2.t18 = t2 → eq_bit t18 t2 = true.
326 #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
329 nlemma eq_to_eqbit26 : ∀t2.t19 = t2 → eq_bit t19 t2 = true.
330 #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
333 nlemma eq_to_eqbit27 : ∀t2.t1A = t2 → eq_bit t1A t2 = true.
334 #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
337 nlemma eq_to_eqbit28 : ∀t2.t1B = t2 → eq_bit t1B t2 = true.
338 #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
341 nlemma eq_to_eqbit29 : ∀t2.t1C = t2 → eq_bit t1C t2 = true.
342 #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
345 nlemma eq_to_eqbit30 : ∀t2.t1D = t2 → eq_bit t1D t2 = true.
346 #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
349 nlemma eq_to_eqbit31 : ∀t2.t1E = t2 → eq_bit t1E t2 = true.
350 #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
353 nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true.
354 #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
357 nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
359 ##[ ##1: napply eq_to_eqbit1 ##| ##2: napply eq_to_eqbit2
360 ##| ##3: napply eq_to_eqbit3 ##| ##4: napply eq_to_eqbit4
361 ##| ##5: napply eq_to_eqbit5 ##| ##6: napply eq_to_eqbit6
362 ##| ##7: napply eq_to_eqbit7 ##| ##8: napply eq_to_eqbit8
363 ##| ##9: napply eq_to_eqbit9 ##| ##10: napply eq_to_eqbit10
364 ##| ##11: napply eq_to_eqbit11 ##| ##12: napply eq_to_eqbit12
365 ##| ##13: napply eq_to_eqbit13 ##| ##14: napply eq_to_eqbit14
366 ##| ##15: napply eq_to_eqbit15 ##| ##16: napply eq_to_eqbit16
367 ##| ##17: napply eq_to_eqbit17 ##| ##18: napply eq_to_eqbit18
368 ##| ##19: napply eq_to_eqbit19 ##| ##20: napply eq_to_eqbit20
369 ##| ##21: napply eq_to_eqbit21 ##| ##22: napply eq_to_eqbit22
370 ##| ##23: napply eq_to_eqbit23 ##| ##24: napply eq_to_eqbit24
371 ##| ##25: napply eq_to_eqbit25 ##| ##26: napply eq_to_eqbit26
372 ##| ##27: napply eq_to_eqbit27 ##| ##28: napply eq_to_eqbit28
373 ##| ##29: napply eq_to_eqbit29 ##| ##30: napply eq_to_eqbit30
374 ##| ##31: napply eq_to_eqbit31 ##| ##32: napply eq_to_eqbit32
378 nlemma decidable_bit1 : ∀x:bitrigesim.decidable (t00 = x).
379 #x; nnormalize; nelim x;
380 ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
381 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
385 nlemma decidable_bit2 : ∀x:bitrigesim.decidable (t01 = x).
386 #x; nnormalize; nelim x;
387 ##[ ##2: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
388 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
392 nlemma decidable_bit3 : ∀x:bitrigesim.decidable (t02 = x).
393 #x; nnormalize; nelim x;
394 ##[ ##3: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
395 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
399 nlemma decidable_bit4 : ∀x:bitrigesim.decidable (t03 = x).
400 #x; nnormalize; nelim x;
401 ##[ ##4: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
402 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
406 nlemma decidable_bit5 : ∀x:bitrigesim.decidable (t04 = x).
407 #x; nnormalize; nelim x;
408 ##[ ##5: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
409 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
413 nlemma decidable_bit6 : ∀x:bitrigesim.decidable (t05 = x).
414 #x; nnormalize; nelim x;
415 ##[ ##6: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
416 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
420 nlemma decidable_bit7 : ∀x:bitrigesim.decidable (t06 = x).
421 #x; nnormalize; nelim x;
422 ##[ ##7: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
423 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
427 nlemma decidable_bit8 : ∀x:bitrigesim.decidable (t07 = x).
428 #x; nnormalize; nelim x;
429 ##[ ##8: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
430 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
434 nlemma decidable_bit9 : ∀x:bitrigesim.decidable (t08 = x).
435 #x; nnormalize; nelim x;
436 ##[ ##9: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
437 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
441 nlemma decidable_bit10 : ∀x:bitrigesim.decidable (t09 = x).
442 #x; nnormalize; nelim x;
443 ##[ ##10: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
444 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
448 nlemma decidable_bit11 : ∀x:bitrigesim.decidable (t0A = x).
449 #x; nnormalize; nelim x;
450 ##[ ##11: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
451 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
455 nlemma decidable_bit12 : ∀x:bitrigesim.decidable (t0B = x).
456 #x; nnormalize; nelim x;
457 ##[ ##12: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
458 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
462 nlemma decidable_bit13 : ∀x:bitrigesim.decidable (t0C = x).
463 #x; nnormalize; nelim x;
464 ##[ ##13: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
465 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
469 nlemma decidable_bit14 : ∀x:bitrigesim.decidable (t0D = x).
470 #x; nnormalize; nelim x;
471 ##[ ##14: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
472 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
476 nlemma decidable_bit15 : ∀x:bitrigesim.decidable (t0E = x).
477 #x; nnormalize; nelim x;
478 ##[ ##15: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
479 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
483 nlemma decidable_bit16 : ∀x:bitrigesim.decidable (t0F = x).
484 #x; nnormalize; nelim x;
485 ##[ ##16: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
486 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
490 nlemma decidable_bit17 : ∀x:bitrigesim.decidable (t10 = x).
491 #x; nnormalize; nelim x;
492 ##[ ##17: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
493 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
497 nlemma decidable_bit18 : ∀x:bitrigesim.decidable (t11 = x).
498 #x; nnormalize; nelim x;
499 ##[ ##18: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
500 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
504 nlemma decidable_bit19 : ∀x:bitrigesim.decidable (t12 = x).
505 #x; nnormalize; nelim x;
506 ##[ ##19: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
507 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
511 nlemma decidable_bit20 : ∀x:bitrigesim.decidable (t13 = x).
512 #x; nnormalize; nelim x;
513 ##[ ##20: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
514 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
518 nlemma decidable_bit21 : ∀x:bitrigesim.decidable (t14 = x).
519 #x; nnormalize; nelim x;
520 ##[ ##21: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
521 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
525 nlemma decidable_bit22 : ∀x:bitrigesim.decidable (t15 = x).
526 #x; nnormalize; nelim x;
527 ##[ ##22: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
528 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
532 nlemma decidable_bit23 : ∀x:bitrigesim.decidable (t16 = x).
533 #x; nnormalize; nelim x;
534 ##[ ##23: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
535 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
539 nlemma decidable_bit24 : ∀x:bitrigesim.decidable (t17 = x).
540 #x; nnormalize; nelim x;
541 ##[ ##24: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
542 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
546 nlemma decidable_bit25 : ∀x:bitrigesim.decidable (t18 = x).
547 #x; nnormalize; nelim x;
548 ##[ ##25: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
549 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
553 nlemma decidable_bit26 : ∀x:bitrigesim.decidable (t19 = x).
554 #x; nnormalize; nelim x;
555 ##[ ##26: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
556 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
560 nlemma decidable_bit27 : ∀x:bitrigesim.decidable (t1A = x).
561 #x; nnormalize; nelim x;
562 ##[ ##27: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
563 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
567 nlemma decidable_bit28 : ∀x:bitrigesim.decidable (t1B = x).
568 #x; nnormalize; nelim x;
569 ##[ ##28: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
570 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
574 nlemma decidable_bit29 : ∀x:bitrigesim.decidable (t1C = x).
575 #x; nnormalize; nelim x;
576 ##[ ##29: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
577 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
581 nlemma decidable_bit30 : ∀x:bitrigesim.decidable (t1D = x).
582 #x; nnormalize; nelim x;
583 ##[ ##30: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
584 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
588 nlemma decidable_bit31 : ∀x:bitrigesim.decidable (t1E = x).
589 #x; nnormalize; nelim x;
590 ##[ ##31: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
591 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
595 nlemma decidable_bit32 : ∀x:bitrigesim.decidable (t1F = x).
596 #x; nnormalize; nelim x;
597 ##[ ##32: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
598 ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
602 nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
603 #x; nnormalize; nelim x;
604 ##[ ##1: napply decidable_bit1 ##| ##2: napply decidable_bit2
605 ##| ##3: napply decidable_bit3 ##| ##4: napply decidable_bit4
606 ##| ##5: napply decidable_bit5 ##| ##6: napply decidable_bit6
607 ##| ##7: napply decidable_bit7 ##| ##8: napply decidable_bit8
608 ##| ##9: napply decidable_bit9 ##| ##10: napply decidable_bit10
609 ##| ##11: napply decidable_bit11 ##| ##12: napply decidable_bit12
610 ##| ##13: napply decidable_bit13 ##| ##14: napply decidable_bit14
611 ##| ##15: napply decidable_bit15 ##| ##16: napply decidable_bit16
612 ##| ##17: napply decidable_bit17 ##| ##18: napply decidable_bit18
613 ##| ##19: napply decidable_bit19 ##| ##20: napply decidable_bit20
614 ##| ##21: napply decidable_bit21 ##| ##22: napply decidable_bit22
615 ##| ##23: napply decidable_bit23 ##| ##24: napply decidable_bit24
616 ##| ##25: napply decidable_bit25 ##| ##26: napply decidable_bit26
617 ##| ##27: napply decidable_bit27 ##| ##28: napply decidable_bit28
618 ##| ##29: napply decidable_bit29 ##| ##30: napply decidable_bit30
619 ##| ##31: napply decidable_bit31 ##| ##32: napply decidable_bit32
623 nlemma neqbit_to_neq1 : ∀t2.eq_bit t00 t2 = false → t00 ≠ t2.
624 #t2; ncases t2; nnormalize; #H;
625 ##[ ##1: napply (bool_destruct … H)
626 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
630 nlemma neqbit_to_neq2 : ∀t2.eq_bit t01 t2 = false → t01 ≠ t2.
631 #t2; ncases t2; nnormalize; #H;
632 ##[ ##2: napply (bool_destruct … H)
633 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
637 nlemma neqbit_to_neq3 : ∀t2.eq_bit t02 t2 = false → t02 ≠ t2.
638 #t2; ncases t2; nnormalize; #H;
639 ##[ ##3: napply (bool_destruct … H)
640 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
644 nlemma neqbit_to_neq4 : ∀t2.eq_bit t03 t2 = false → t03 ≠ t2.
645 #t2; ncases t2; nnormalize; #H;
646 ##[ ##4: napply (bool_destruct … H)
647 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
651 nlemma neqbit_to_neq5 : ∀t2.eq_bit t04 t2 = false → t04 ≠ t2.
652 #t2; ncases t2; nnormalize; #H;
653 ##[ ##5: napply (bool_destruct … H)
654 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
658 nlemma neqbit_to_neq6 : ∀t2.eq_bit t05 t2 = false → t05 ≠ t2.
659 #t2; ncases t2; nnormalize; #H;
660 ##[ ##6: napply (bool_destruct … H)
661 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
665 nlemma neqbit_to_neq7 : ∀t2.eq_bit t06 t2 = false → t06 ≠ t2.
666 #t2; ncases t2; nnormalize; #H;
667 ##[ ##7: napply (bool_destruct … H)
668 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
672 nlemma neqbit_to_neq8 : ∀t2.eq_bit t07 t2 = false → t07 ≠ t2.
673 #t2; ncases t2; nnormalize; #H;
674 ##[ ##8: napply (bool_destruct … H)
675 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
679 nlemma neqbit_to_neq9 : ∀t2.eq_bit t08 t2 = false → t08 ≠ t2.
680 #t2; ncases t2; nnormalize; #H;
681 ##[ ##9: napply (bool_destruct … H)
682 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
686 nlemma neqbit_to_neq10 : ∀t2.eq_bit t09 t2 = false → t09 ≠ t2.
687 #t2; ncases t2; nnormalize; #H;
688 ##[ ##10: napply (bool_destruct … H)
689 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
693 nlemma neqbit_to_neq11 : ∀t2.eq_bit t0A t2 = false → t0A ≠ t2.
694 #t2; ncases t2; nnormalize; #H;
695 ##[ ##11: napply (bool_destruct … H)
696 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
700 nlemma neqbit_to_neq12 : ∀t2.eq_bit t0B t2 = false → t0B ≠ t2.
701 #t2; ncases t2; nnormalize; #H;
702 ##[ ##12: napply (bool_destruct … H)
703 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
707 nlemma neqbit_to_neq13 : ∀t2.eq_bit t0C t2 = false → t0C ≠ t2.
708 #t2; ncases t2; nnormalize; #H;
709 ##[ ##13: napply (bool_destruct … H)
710 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
714 nlemma neqbit_to_neq14 : ∀t2.eq_bit t0D t2 = false → t0D ≠ t2.
715 #t2; ncases t2; nnormalize; #H;
716 ##[ ##14: napply (bool_destruct … H)
717 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
721 nlemma neqbit_to_neq15 : ∀t2.eq_bit t0E t2 = false → t0E ≠ t2.
722 #t2; ncases t2; nnormalize; #H;
723 ##[ ##15: napply (bool_destruct … H)
724 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
728 nlemma neqbit_to_neq16 : ∀t2.eq_bit t0F t2 = false → t0F ≠ t2.
729 #t2; ncases t2; nnormalize; #H;
730 ##[ ##16: napply (bool_destruct … H)
731 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
735 nlemma neqbit_to_neq17 : ∀t2.eq_bit t10 t2 = false → t10 ≠ t2.
736 #t2; ncases t2; nnormalize; #H;
737 ##[ ##17: napply (bool_destruct … H)
738 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
742 nlemma neqbit_to_neq18 : ∀t2.eq_bit t11 t2 = false → t11 ≠ t2.
743 #t2; ncases t2; nnormalize; #H;
744 ##[ ##18: napply (bool_destruct … H)
745 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
749 nlemma neqbit_to_neq19 : ∀t2.eq_bit t12 t2 = false → t12 ≠ t2.
750 #t2; ncases t2; nnormalize; #H;
751 ##[ ##19: napply (bool_destruct … H)
752 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
756 nlemma neqbit_to_neq20 : ∀t2.eq_bit t13 t2 = false → t13 ≠ t2.
757 #t2; ncases t2; nnormalize; #H;
758 ##[ ##20: napply (bool_destruct … H)
759 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
763 nlemma neqbit_to_neq21 : ∀t2.eq_bit t14 t2 = false → t14 ≠ t2.
764 #t2; ncases t2; nnormalize; #H;
765 ##[ ##21: napply (bool_destruct … H)
766 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
770 nlemma neqbit_to_neq22 : ∀t2.eq_bit t15 t2 = false → t15 ≠ t2.
771 #t2; ncases t2; nnormalize; #H;
772 ##[ ##22: napply (bool_destruct … H)
773 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
777 nlemma neqbit_to_neq23 : ∀t2.eq_bit t16 t2 = false → t16 ≠ t2.
778 #t2; ncases t2; nnormalize; #H;
779 ##[ ##23: napply (bool_destruct … H)
780 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
784 nlemma neqbit_to_neq24 : ∀t2.eq_bit t17 t2 = false → t17 ≠ t2.
785 #t2; ncases t2; nnormalize; #H;
786 ##[ ##24: napply (bool_destruct … H)
787 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
791 nlemma neqbit_to_neq25 : ∀t2.eq_bit t18 t2 = false → t18 ≠ t2.
792 #t2; ncases t2; nnormalize; #H;
793 ##[ ##25: napply (bool_destruct … H)
794 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
798 nlemma neqbit_to_neq26 : ∀t2.eq_bit t19 t2 = false → t19 ≠ t2.
799 #t2; ncases t2; nnormalize; #H;
800 ##[ ##26: napply (bool_destruct … H)
801 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
805 nlemma neqbit_to_neq27 : ∀t2.eq_bit t1A t2 = false → t1A ≠ t2.
806 #t2; ncases t2; nnormalize; #H;
807 ##[ ##27: napply (bool_destruct … H)
808 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
812 nlemma neqbit_to_neq28 : ∀t2.eq_bit t1B t2 = false → t1B ≠ t2.
813 #t2; ncases t2; nnormalize; #H;
814 ##[ ##28: napply (bool_destruct … H)
815 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
819 nlemma neqbit_to_neq29 : ∀t2.eq_bit t1C t2 = false → t1C ≠ t2.
820 #t2; ncases t2; nnormalize; #H;
821 ##[ ##29: napply (bool_destruct … H)
822 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
826 nlemma neqbit_to_neq30 : ∀t2.eq_bit t1D t2 = false → t1D ≠ t2.
827 #t2; ncases t2; nnormalize; #H;
828 ##[ ##30: napply (bool_destruct … H)
829 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
833 nlemma neqbit_to_neq31 : ∀t2.eq_bit t1E t2 = false → t1E ≠ t2.
834 #t2; ncases t2; nnormalize; #H;
835 ##[ ##31: napply (bool_destruct … H)
836 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
840 nlemma neqbit_to_neq32 : ∀t2.eq_bit t1F t2 = false → t1F ≠ t2.
841 #t2; ncases t2; nnormalize; #H;
842 ##[ ##32: napply (bool_destruct … H)
843 ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
847 nlemma neqbit_to_neq : ∀t1,t2.eq_bit t1 t2 = false → t1 ≠ t2.
849 ##[ ##1: napply neqbit_to_neq1 ##| ##2: napply neqbit_to_neq2
850 ##| ##3: napply neqbit_to_neq3 ##| ##4: napply neqbit_to_neq4
851 ##| ##5: napply neqbit_to_neq5 ##| ##6: napply neqbit_to_neq6
852 ##| ##7: napply neqbit_to_neq7 ##| ##8: napply neqbit_to_neq8
853 ##| ##9: napply neqbit_to_neq9 ##| ##10: napply neqbit_to_neq10
854 ##| ##11: napply neqbit_to_neq11 ##| ##12: napply neqbit_to_neq12
855 ##| ##13: napply neqbit_to_neq13 ##| ##14: napply neqbit_to_neq14
856 ##| ##15: napply neqbit_to_neq15 ##| ##16: napply neqbit_to_neq16
857 ##| ##17: napply neqbit_to_neq17 ##| ##18: napply neqbit_to_neq18
858 ##| ##19: napply neqbit_to_neq19 ##| ##20: napply neqbit_to_neq20
859 ##| ##21: napply neqbit_to_neq21 ##| ##22: napply neqbit_to_neq22
860 ##| ##23: napply neqbit_to_neq23 ##| ##24: napply neqbit_to_neq24
861 ##| ##25: napply neqbit_to_neq25 ##| ##26: napply neqbit_to_neq26
862 ##| ##27: napply neqbit_to_neq27 ##| ##28: napply neqbit_to_neq28
863 ##| ##29: napply neqbit_to_neq29 ##| ##30: napply neqbit_to_neq30
864 ##| ##31: napply neqbit_to_neq31 ##| ##32: napply neqbit_to_neq32
868 nlemma neq_to_neqbit1 : ∀t2.t00 ≠ t2 → eq_bit t00 t2 = false.
869 #t2; ncases t2; nnormalize; #H; ##[ ##1: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
872 nlemma neq_to_neqbit2 : ∀t2.t01 ≠ t2 → eq_bit t01 t2 = false.
873 #t2; ncases t2; nnormalize; #H; ##[ ##2: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
876 nlemma neq_to_neqbit3 : ∀t2.t02 ≠ t2 → eq_bit t02 t2 = false.
877 #t2; ncases t2; nnormalize; #H; ##[ ##3: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
880 nlemma neq_to_neqbit4 : ∀t2.t03 ≠ t2 → eq_bit t03 t2 = false.
881 #t2; ncases t2; nnormalize; #H; ##[ ##4: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
884 nlemma neq_to_neqbit5 : ∀t2.t04 ≠ t2 → eq_bit t04 t2 = false.
885 #t2; ncases t2; nnormalize; #H; ##[ ##5: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
888 nlemma neq_to_neqbit6 : ∀t2.t05 ≠ t2 → eq_bit t05 t2 = false.
889 #t2; ncases t2; nnormalize; #H; ##[ ##6: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
892 nlemma neq_to_neqbit7 : ∀t2.t06 ≠ t2 → eq_bit t06 t2 = false.
893 #t2; ncases t2; nnormalize; #H; ##[ ##7: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
896 nlemma neq_to_neqbit8 : ∀t2.t07 ≠ t2 → eq_bit t07 t2 = false.
897 #t2; ncases t2; nnormalize; #H; ##[ ##8: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
900 nlemma neq_to_neqbit9 : ∀t2.t08 ≠ t2 → eq_bit t08 t2 = false.
901 #t2; ncases t2; nnormalize; #H; ##[ ##9: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
904 nlemma neq_to_neqbit10 : ∀t2.t09 ≠ t2 → eq_bit t09 t2 = false.
905 #t2; ncases t2; nnormalize; #H; ##[ ##10: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
908 nlemma neq_to_neqbit11 : ∀t2.t0A ≠ t2 → eq_bit t0A t2 = false.
909 #t2; ncases t2; nnormalize; #H; ##[ ##11: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
912 nlemma neq_to_neqbit12 : ∀t2.t0B ≠ t2 → eq_bit t0B t2 = false.
913 #t2; ncases t2; nnormalize; #H; ##[ ##12: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
916 nlemma neq_to_neqbit13 : ∀t2.t0C ≠ t2 → eq_bit t0C t2 = false.
917 #t2; ncases t2; nnormalize; #H; ##[ ##13: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
920 nlemma neq_to_neqbit14 : ∀t2.t0D ≠ t2 → eq_bit t0D t2 = false.
921 #t2; ncases t2; nnormalize; #H; ##[ ##14: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
924 nlemma neq_to_neqbit15 : ∀t2.t0E ≠ t2 → eq_bit t0E t2 = false.
925 #t2; ncases t2; nnormalize; #H; ##[ ##15: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
928 nlemma neq_to_neqbit16 : ∀t2.t0F ≠ t2 → eq_bit t0F t2 = false.
929 #t2; ncases t2; nnormalize; #H; ##[ ##16: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
932 nlemma neq_to_neqbit17 : ∀t2.t10 ≠ t2 → eq_bit t10 t2 = false.
933 #t2; ncases t2; nnormalize; #H; ##[ ##17: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
936 nlemma neq_to_neqbit18 : ∀t2.t11 ≠ t2 → eq_bit t11 t2 = false.
937 #t2; ncases t2; nnormalize; #H; ##[ ##18: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
940 nlemma neq_to_neqbit19 : ∀t2.t12 ≠ t2 → eq_bit t12 t2 = false.
941 #t2; ncases t2; nnormalize; #H; ##[ ##19: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
944 nlemma neq_to_neqbit20 : ∀t2.t13 ≠ t2 → eq_bit t13 t2 = false.
945 #t2; ncases t2; nnormalize; #H; ##[ ##20: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
948 nlemma neq_to_neqbit21 : ∀t2.t14 ≠ t2 → eq_bit t14 t2 = false.
949 #t2; ncases t2; nnormalize; #H; ##[ ##21: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
952 nlemma neq_to_neqbit22 : ∀t2.t15 ≠ t2 → eq_bit t15 t2 = false.
953 #t2; ncases t2; nnormalize; #H; ##[ ##22: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
956 nlemma neq_to_neqbit23 : ∀t2.t16 ≠ t2 → eq_bit t16 t2 = false.
957 #t2; ncases t2; nnormalize; #H; ##[ ##23: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
960 nlemma neq_to_neqbit24 : ∀t2.t17 ≠ t2 → eq_bit t17 t2 = false.
961 #t2; ncases t2; nnormalize; #H; ##[ ##24: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
964 nlemma neq_to_neqbit25 : ∀t2.t18 ≠ t2 → eq_bit t18 t2 = false.
965 #t2; ncases t2; nnormalize; #H; ##[ ##25: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
968 nlemma neq_to_neqbit26 : ∀t2.t19 ≠ t2 → eq_bit t19 t2 = false.
969 #t2; ncases t2; nnormalize; #H; ##[ ##26: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
972 nlemma neq_to_neqbit27 : ∀t2.t1A ≠ t2 → eq_bit t1A t2 = false.
973 #t2; ncases t2; nnormalize; #H; ##[ ##27: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
976 nlemma neq_to_neqbit28 : ∀t2.t1B ≠ t2 → eq_bit t1B t2 = false.
977 #t2; ncases t2; nnormalize; #H; ##[ ##28: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
980 nlemma neq_to_neqbit29 : ∀t2.t1C ≠ t2 → eq_bit t1C t2 = false.
981 #t2; ncases t2; nnormalize; #H; ##[ ##29: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
984 nlemma neq_to_neqbit30 : ∀t2.t1D ≠ t2 → eq_bit t1D t2 = false.
985 #t2; ncases t2; nnormalize; #H; ##[ ##30: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
988 nlemma neq_to_neqbit31 : ∀t2.t1E ≠ t2 → eq_bit t1E t2 = false.
989 #t2; ncases t2; nnormalize; #H; ##[ ##31: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
992 nlemma neq_to_neqbit32 : ∀t2.t1F ≠ t2 → eq_bit t1F t2 = false.
993 #t2; ncases t2; nnormalize; #H; ##[ ##32: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
996 nlemma neq_to_neqbit : ∀t1,t2.t1 ≠ t2 → eq_bit t1 t2 = false.
998 ##[ ##1: napply neq_to_neqbit1 ##| ##2: napply neq_to_neqbit2
999 ##| ##3: napply neq_to_neqbit3 ##| ##4: napply neq_to_neqbit4
1000 ##| ##5: napply neq_to_neqbit5 ##| ##6: napply neq_to_neqbit6
1001 ##| ##7: napply neq_to_neqbit7 ##| ##8: napply neq_to_neqbit8
1002 ##| ##9: napply neq_to_neqbit9 ##| ##10: napply neq_to_neqbit10
1003 ##| ##11: napply neq_to_neqbit11 ##| ##12: napply neq_to_neqbit12
1004 ##| ##13: napply neq_to_neqbit13 ##| ##14: napply neq_to_neqbit14
1005 ##| ##15: napply neq_to_neqbit15 ##| ##16: napply neq_to_neqbit16
1006 ##| ##17: napply neq_to_neqbit17 ##| ##18: napply neq_to_neqbit18
1007 ##| ##19: napply neq_to_neqbit19 ##| ##20: napply neq_to_neqbit20
1008 ##| ##21: napply neq_to_neqbit21 ##| ##22: napply neq_to_neqbit22
1009 ##| ##23: napply neq_to_neqbit23 ##| ##24: napply neq_to_neqbit24
1010 ##| ##25: napply neq_to_neqbit25 ##| ##26: napply neq_to_neqbit26
1011 ##| ##27: napply neq_to_neqbit27 ##| ##28: napply neq_to_neqbit28
1012 ##| ##29: napply neq_to_neqbit29 ##| ##30: napply neq_to_neqbit30
1013 ##| ##31: napply neq_to_neqbit31 ##| ##32: napply neq_to_neqbit32