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 *)
19 (* Cosimo Oliboni, oliboni@cs.unibo.it *)
21 (* Questo materiale fa parte della tesi: *)
22 (* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
24 (* data ultima modifica 15/11/2007 *)
25 (* ********************************************************************** *)
27 include "freescale/bool_lemmas.ma".
28 include "freescale/aux_bases.ma".
34 ndefinition oct_destruct_aux ≝
35 Πn1,n2:oct.ΠP:Prop.n1 = n2 →
37 [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
38 | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
39 | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ]
40 | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
41 | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ]
42 | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
43 | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
44 | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
47 ndefinition oct_destruct : oct_destruct_aux.
50 ##[ ##1: nelim n2; nnormalize; #H;
51 ##[ ##1: napply (λx:P.x)
52 ##| ##*: napply (False_ind ??);
53 nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
54 nrewrite > H; nnormalize; napply I
56 ##| ##2: nelim n2; nnormalize; #H;
57 ##[ ##2: napply (λx:P.x)
58 ##| ##*: napply (False_ind ??);
59 nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
60 nrewrite > H; nnormalize; napply I
62 ##| ##3: nelim n2; nnormalize; #H;
63 ##[ ##3: napply (λx:P.x)
64 ##| ##*: napply (False_ind ??);
65 nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
66 nrewrite > H; nnormalize; napply I
68 ##| ##4: nelim n2; nnormalize; #H;
69 ##[ ##4: napply (λx:P.x)
70 ##| ##*: napply (False_ind ??);
71 nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
72 nrewrite > H; nnormalize; napply I
74 ##| ##5: nelim n2; nnormalize; #H;
75 ##[ ##5: napply (λx:P.x)
76 ##| ##*: napply (False_ind ??);
77 nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
78 nrewrite > H; nnormalize; napply I
80 ##| ##6: nelim n2; nnormalize; #H;
81 ##[ ##6: napply (λx:P.x)
82 ##| ##*: napply (False_ind ??);
83 nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
84 nrewrite > H; nnormalize; napply I
86 ##| ##7: nelim n2; nnormalize; #H;
87 ##[ ##7: napply (λx:P.x)
88 ##| ##*: napply (False_ind ??);
89 nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
90 nrewrite > H; nnormalize; napply I
92 ##| ##8: nelim n2; nnormalize; #H;
93 ##[ ##8: napply (λx:P.x)
94 ##| ##*: napply (False_ind ??);
95 nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
96 nrewrite > H; nnormalize; napply I
101 nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
109 nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
114 ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
115 ##| ##*: #H; napply (bool_destruct ??? H)
119 nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
124 ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
125 ##| ##*: #H; napply (oct_destruct ??? H)
133 ndefinition bitrigesim_destruct1 :
134 Πt2:bitrigesim.ΠP:Prop.t00 = t2 → match t2 with [ t00 ⇒ P → P | _ ⇒ P ].
138 ##[ ##1: napply (λx:P.x)
139 ##| ##*: napply (False_ind ??);
140 nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
141 nrewrite > H; nnormalize; napply I
145 ndefinition bitrigesim_destruct2 :
146 Πt2:bitrigesim.ΠP:Prop.t01 = t2 → match t2 with [ t01 ⇒ P → P | _ ⇒ P ].
150 ##[ ##2: napply (λx:P.x)
151 ##| ##*: napply (False_ind ??);
152 nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
153 nrewrite > H; nnormalize; napply I
157 ndefinition bitrigesim_destruct3 :
158 Πt2:bitrigesim.ΠP:Prop.t02 = t2 → match t2 with [ t02 ⇒ P → P | _ ⇒ P ].
162 ##[ ##3: napply (λx:P.x)
163 ##| ##*: napply (False_ind ??);
164 nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
165 nrewrite > H; nnormalize; napply I
169 ndefinition bitrigesim_destruct4 :
170 Πt2:bitrigesim.ΠP:Prop.t03 = t2 → match t2 with [ t03 ⇒ P → P | _ ⇒ P ].
174 ##[ ##4: napply (λx:P.x)
175 ##| ##*: napply (False_ind ??);
176 nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
177 nrewrite > H; nnormalize; napply I
181 ndefinition bitrigesim_destruct5 :
182 Πt2:bitrigesim.ΠP:Prop.t04 = t2 → match t2 with [ t04 ⇒ P → P | _ ⇒ P ].
186 ##[ ##5: napply (λx:P.x)
187 ##| ##*: napply (False_ind ??);
188 nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
189 nrewrite > H; nnormalize; napply I
193 ndefinition bitrigesim_destruct6 :
194 Πt2:bitrigesim.ΠP:Prop.t05 = t2 → match t2 with [ t05 ⇒ P → P | _ ⇒ P ].
198 ##[ ##6: napply (λx:P.x)
199 ##| ##*: napply (False_ind ??);
200 nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
201 nrewrite > H; nnormalize; napply I
205 ndefinition bitrigesim_destruct7 :
206 Πt2:bitrigesim.ΠP:Prop.t06 = t2 → match t2 with [ t06 ⇒ P → P | _ ⇒ P ].
210 ##[ ##7: napply (λx:P.x)
211 ##| ##*: napply (False_ind ??);
212 nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
213 nrewrite > H; nnormalize; napply I
217 ndefinition bitrigesim_destruct8 :
218 Πt2:bitrigesim.ΠP:Prop.t07 = t2 → match t2 with [ t07 ⇒ P → P | _ ⇒ P ].
222 ##[ ##8: napply (λx:P.x)
223 ##| ##*: napply (False_ind ??);
224 nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
225 nrewrite > H; nnormalize; napply I
229 ndefinition bitrigesim_destruct9 :
230 Πt2:bitrigesim.ΠP:Prop.t08 = t2 → match t2 with [ t08 ⇒ P → P | _ ⇒ P ].
234 ##[ ##9: napply (λx:P.x)
235 ##| ##*: napply (False_ind ??);
236 nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
237 nrewrite > H; nnormalize; napply I
241 ndefinition bitrigesim_destruct10 :
242 Πt2:bitrigesim.ΠP:Prop.t09 = t2 → match t2 with [ t09 ⇒ P → P | _ ⇒ P ].
246 ##[ ##10: napply (λx:P.x)
247 ##| ##*: napply (False_ind ??);
248 nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
249 nrewrite > H; nnormalize; napply I
253 ndefinition bitrigesim_destruct11 :
254 Πt2:bitrigesim.ΠP:Prop.t0A = t2 → match t2 with [ t0A ⇒ P → P | _ ⇒ P ].
258 ##[ ##11: napply (λx:P.x)
259 ##| ##*: napply (False_ind ??);
260 nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
261 nrewrite > H; nnormalize; napply I
265 ndefinition bitrigesim_destruct12 :
266 Πt2:bitrigesim.ΠP:Prop.t0B = t2 → match t2 with [ t0B ⇒ P → P | _ ⇒ P ].
270 ##[ ##12: napply (λx:P.x)
271 ##| ##*: napply (False_ind ??);
272 nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
273 nrewrite > H; nnormalize; napply I
277 ndefinition bitrigesim_destruct13 :
278 Πt2:bitrigesim.ΠP:Prop.t0C = t2 → match t2 with [ t0C ⇒ P → P | _ ⇒ P ].
282 ##[ ##13: napply (λx:P.x)
283 ##| ##*: napply (False_ind ??);
284 nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
285 nrewrite > H; nnormalize; napply I
289 ndefinition bitrigesim_destruct14 :
290 Πt2:bitrigesim.ΠP:Prop.t0D = t2 → match t2 with [ t0D ⇒ P → P | _ ⇒ P ].
294 ##[ ##14: napply (λx:P.x)
295 ##| ##*: napply (False_ind ??);
296 nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
297 nrewrite > H; nnormalize; napply I
301 ndefinition bitrigesim_destruct15 :
302 Πt2:bitrigesim.ΠP:Prop.t0E = t2 → match t2 with [ t0E ⇒ P → P | _ ⇒ P ].
306 ##[ ##15: napply (λx:P.x)
307 ##| ##*: napply (False_ind ??);
308 nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
309 nrewrite > H; nnormalize; napply I
313 ndefinition bitrigesim_destruct16 :
314 Πt2:bitrigesim.ΠP:Prop.t0F = t2 → match t2 with [ t0F ⇒ P → P | _ ⇒ P ].
318 ##[ ##16: napply (λx:P.x)
319 ##| ##*: napply (False_ind ??);
320 nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
321 nrewrite > H; nnormalize; napply I
325 ndefinition bitrigesim_destruct17 :
326 Πt2:bitrigesim.ΠP:Prop.t10 = t2 → match t2 with [ t10 ⇒ P → P | _ ⇒ P ].
330 ##[ ##17: napply (λx:P.x)
331 ##| ##*: napply (False_ind ??);
332 nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
333 nrewrite > H; nnormalize; napply I
337 ndefinition bitrigesim_destruct18 :
338 Πt2:bitrigesim.ΠP:Prop.t11 = t2 → match t2 with [ t11 ⇒ P → P | _ ⇒ P ].
342 ##[ ##18: napply (λx:P.x)
343 ##| ##*: napply (False_ind ??);
344 nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
345 nrewrite > H; nnormalize; napply I
349 ndefinition bitrigesim_destruct19 :
350 Πt2:bitrigesim.ΠP:Prop.t12 = t2 → match t2 with [ t12 ⇒ P → P | _ ⇒ P ].
354 ##[ ##19: napply (λx:P.x)
355 ##| ##*: napply (False_ind ??);
356 nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
357 nrewrite > H; nnormalize; napply I
361 ndefinition bitrigesim_destruct20 :
362 Πt2:bitrigesim.ΠP:Prop.t13 = t2 → match t2 with [ t13 ⇒ P → P | _ ⇒ P ].
366 ##[ ##20: napply (λx:P.x)
367 ##| ##*: napply (False_ind ??);
368 nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
369 nrewrite > H; nnormalize; napply I
373 ndefinition bitrigesim_destruct21 :
374 Πt2:bitrigesim.ΠP:Prop.t14 = t2 → match t2 with [ t14 ⇒ P → P | _ ⇒ P ].
378 ##[ ##21: napply (λx:P.x)
379 ##| ##*: napply (False_ind ??);
380 nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
381 nrewrite > H; nnormalize; napply I
385 ndefinition bitrigesim_destruct22 :
386 Πt2:bitrigesim.ΠP:Prop.t15 = t2 → match t2 with [ t15 ⇒ P → P | _ ⇒ P ].
390 ##[ ##22: napply (λx:P.x)
391 ##| ##*: napply (False_ind ??);
392 nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
393 nrewrite > H; nnormalize; napply I
397 ndefinition bitrigesim_destruct23 :
398 Πt2:bitrigesim.ΠP:Prop.t16 = t2 → match t2 with [ t16 ⇒ P → P | _ ⇒ P ].
402 ##[ ##23: napply (λx:P.x)
403 ##| ##*: napply (False_ind ??);
404 nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
405 nrewrite > H; nnormalize; napply I
409 ndefinition bitrigesim_destruct24 :
410 Πt2:bitrigesim.ΠP:Prop.t17 = t2 → match t2 with [ t17 ⇒ P → P | _ ⇒ P ].
414 ##[ ##24: napply (λx:P.x)
415 ##| ##*: napply (False_ind ??);
416 nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
417 nrewrite > H; nnormalize; napply I
421 ndefinition bitrigesim_destruct25 :
422 Πt2:bitrigesim.ΠP:Prop.t18 = t2 → match t2 with [ t18 ⇒ P → P | _ ⇒ P ].
426 ##[ ##25: napply (λx:P.x)
427 ##| ##*: napply (False_ind ??);
428 nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
429 nrewrite > H; nnormalize; napply I
433 ndefinition bitrigesim_destruct26 :
434 Πt2:bitrigesim.ΠP:Prop.t19 = t2 → match t2 with [ t19 ⇒ P → P | _ ⇒ P ].
438 ##[ ##26: napply (λx:P.x)
439 ##| ##*: napply (False_ind ??);
440 nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
441 nrewrite > H; nnormalize; napply I
445 ndefinition bitrigesim_destruct27 :
446 Πt2:bitrigesim.ΠP:Prop.t1A = t2 → match t2 with [ t1A ⇒ P → P | _ ⇒ P ].
450 ##[ ##27: napply (λx:P.x)
451 ##| ##*: napply (False_ind ??);
452 nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
453 nrewrite > H; nnormalize; napply I
457 ndefinition bitrigesim_destruct28 :
458 Πt2:bitrigesim.ΠP:Prop.t1B = t2 → match t2 with [ t1B ⇒ P → P | _ ⇒ P ].
462 ##[ ##28: napply (λx:P.x)
463 ##| ##*: napply (False_ind ??);
464 nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
465 nrewrite > H; nnormalize; napply I
469 ndefinition bitrigesim_destruct29 :
470 Πt2:bitrigesim.ΠP:Prop.t1C = t2 → match t2 with [ t1C ⇒ P → P | _ ⇒ P ].
474 ##[ ##29: napply (λx:P.x)
475 ##| ##*: napply (False_ind ??);
476 nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
477 nrewrite > H; nnormalize; napply I
481 ndefinition bitrigesim_destruct30 :
482 Πt2:bitrigesim.ΠP:Prop.t1D = t2 → match t2 with [ t1D ⇒ P → P | _ ⇒ P ].
486 ##[ ##30: napply (λx:P.x)
487 ##| ##*: napply (False_ind ??);
488 nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
489 nrewrite > H; nnormalize; napply I
493 ndefinition bitrigesim_destruct31 :
494 Πt2:bitrigesim.ΠP:Prop.t1E = t2 → match t2 with [ t1E ⇒ P → P | _ ⇒ P ].
498 ##[ ##31: napply (λx:P.x)
499 ##| ##*: napply (False_ind ??);
500 nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
501 nrewrite > H; nnormalize; napply I
505 ndefinition bitrigesim_destruct32 :
506 Πt2:bitrigesim.ΠP:Prop.t1F = t2 → match t2 with [ t1F ⇒ P → P | _ ⇒ P ].
510 ##[ ##32: napply (λx:P.x)
511 ##| ##*: napply (False_ind ??);
512 nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
513 nrewrite > H; nnormalize; napply I
517 ndefinition bitrigesim_destruct_aux ≝
518 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
520 [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
521 | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
522 | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
523 | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
524 | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
525 | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
526 | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
527 | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
528 | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
529 | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
530 | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
531 | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
532 | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
533 | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
534 | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
535 | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
536 | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
537 | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
538 | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
539 | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
540 | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
541 | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
542 | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
543 | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
544 | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
545 | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
546 | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
547 | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
548 | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
549 | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
550 | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
551 | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
554 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
557 ##[ ##1: napply bitrigesim_destruct1
558 ##| ##2: napply bitrigesim_destruct2
559 ##| ##3: napply bitrigesim_destruct3
560 ##| ##4: napply bitrigesim_destruct4
561 ##| ##5: napply bitrigesim_destruct5
562 ##| ##6: napply bitrigesim_destruct6
563 ##| ##7: napply bitrigesim_destruct7
564 ##| ##8: napply bitrigesim_destruct8
565 ##| ##9: napply bitrigesim_destruct9
566 ##| ##10: napply bitrigesim_destruct10
567 ##| ##11: napply bitrigesim_destruct11
568 ##| ##12: napply bitrigesim_destruct12
569 ##| ##13: napply bitrigesim_destruct13
570 ##| ##14: napply bitrigesim_destruct14
571 ##| ##15: napply bitrigesim_destruct15
572 ##| ##16: napply bitrigesim_destruct16
573 ##| ##17: napply bitrigesim_destruct17
574 ##| ##18: napply bitrigesim_destruct18
575 ##| ##19: napply bitrigesim_destruct19
576 ##| ##20: napply bitrigesim_destruct20
577 ##| ##21: napply bitrigesim_destruct21
578 ##| ##22: napply bitrigesim_destruct22
579 ##| ##23: napply bitrigesim_destruct23
580 ##| ##24: napply bitrigesim_destruct24
581 ##| ##25: napply bitrigesim_destruct25
582 ##| ##26: napply bitrigesim_destruct26
583 ##| ##27: napply bitrigesim_destruct27
584 ##| ##28: napply bitrigesim_destruct28
585 ##| ##29: napply bitrigesim_destruct29
586 ##| ##30: napply bitrigesim_destruct30
587 ##| ##31: napply bitrigesim_destruct31
588 ##| ##32: napply bitrigesim_destruct32
592 nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
595 ##[ ##1: #t2; nelim t2; nnormalize; napply (refl_eq ??)
596 ##| ##2: #t2; nelim t2; nnormalize; napply (refl_eq ??)
597 ##| ##3: #t2; nelim t2; nnormalize; napply (refl_eq ??)
598 ##| ##4: #t2; nelim t2; nnormalize; napply (refl_eq ??)
599 ##| ##5: #t2; nelim t2; nnormalize; napply (refl_eq ??)
600 ##| ##6: #t2; nelim t2; nnormalize; napply (refl_eq ??)
601 ##| ##7: #t2; nelim t2; nnormalize; napply (refl_eq ??)
602 ##| ##8: #t2; nelim t2; nnormalize; napply (refl_eq ??)
603 ##| ##9: #t2; nelim t2; nnormalize; napply (refl_eq ??)
604 ##| ##10: #t2; nelim t2; nnormalize; napply (refl_eq ??)
605 ##| ##11: #t2; nelim t2; nnormalize; napply (refl_eq ??)
606 ##| ##12: #t2; nelim t2; nnormalize; napply (refl_eq ??)
607 ##| ##13: #t2; nelim t2; nnormalize; napply (refl_eq ??)
608 ##| ##14: #t2; nelim t2; nnormalize; napply (refl_eq ??)
609 ##| ##15: #t2; nelim t2; nnormalize; napply (refl_eq ??)
610 ##| ##16: #t2; nelim t2; nnormalize; napply (refl_eq ??)
611 ##| ##17: #t2; nelim t2; nnormalize; napply (refl_eq ??)
612 ##| ##18: #t2; nelim t2; nnormalize; napply (refl_eq ??)
613 ##| ##19: #t2; nelim t2; nnormalize; napply (refl_eq ??)
614 ##| ##20: #t2; nelim t2; nnormalize; napply (refl_eq ??)
615 ##| ##21: #t2; nelim t2; nnormalize; napply (refl_eq ??)
616 ##| ##22: #t2; nelim t2; nnormalize; napply (refl_eq ??)
617 ##| ##23: #t2; nelim t2; nnormalize; napply (refl_eq ??)
618 ##| ##24: #t2; nelim t2; nnormalize; napply (refl_eq ??)
619 ##| ##25: #t2; nelim t2; nnormalize; napply (refl_eq ??)
620 ##| ##26: #t2; nelim t2; nnormalize; napply (refl_eq ??)
621 ##| ##27: #t2; nelim t2; nnormalize; napply (refl_eq ??)
622 ##| ##28: #t2; nelim t2; nnormalize; napply (refl_eq ??)
623 ##| ##29: #t2; nelim t2; nnormalize; napply (refl_eq ??)
624 ##| ##30: #t2; nelim t2; nnormalize; napply (refl_eq ??)
625 ##| ##31: #t2; nelim t2; nnormalize; napply (refl_eq ??)
626 ##| ##32: #t2; nelim t2; nnormalize; napply (refl_eq ??)
630 nlemma eqbitrig_to_eq1 : ∀t2.eq_bitrig t00 t2 = true → t00 = t2.
631 #t2; ncases t2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
634 nlemma eqbitrig_to_eq2 : ∀t2.eq_bitrig t01 t2 = true → t01 = t2.
635 #t2; ncases t2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
638 nlemma eqbitrig_to_eq3 : ∀t2.eq_bitrig t02 t2 = true → t02 = t2.
639 #t2; ncases t2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
642 nlemma eqbitrig_to_eq4 : ∀t2.eq_bitrig t03 t2 = true → t03 = t2.
643 #t2; ncases t2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
646 nlemma eqbitrig_to_eq5 : ∀t2.eq_bitrig t04 t2 = true → t04 = t2.
647 #t2; ncases t2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
650 nlemma eqbitrig_to_eq6 : ∀t2.eq_bitrig t05 t2 = true → t05 = t2.
651 #t2; ncases t2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
654 nlemma eqbitrig_to_eq7 : ∀t2.eq_bitrig t06 t2 = true → t06 = t2.
655 #t2; ncases t2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
658 nlemma eqbitrig_to_eq8 : ∀t2.eq_bitrig t07 t2 = true → t07 = t2.
659 #t2; ncases t2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
662 nlemma eqbitrig_to_eq9 : ∀t2.eq_bitrig t08 t2 = true → t08 = t2.
663 #t2; ncases t2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
666 nlemma eqbitrig_to_eq10 : ∀t2.eq_bitrig t09 t2 = true → t09 = t2.
667 #t2; ncases t2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
670 nlemma eqbitrig_to_eq11 : ∀t2.eq_bitrig t0A t2 = true → t0A = t2.
671 #t2; ncases t2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
674 nlemma eqbitrig_to_eq12 : ∀t2.eq_bitrig t0B t2 = true → t0B = t2.
675 #t2; ncases t2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
678 nlemma eqbitrig_to_eq13 : ∀t2.eq_bitrig t0C t2 = true → t0C = t2.
679 #t2; ncases t2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
682 nlemma eqbitrig_to_eq14 : ∀t2.eq_bitrig t0D t2 = true → t0D = t2.
683 #t2; ncases t2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
686 nlemma eqbitrig_to_eq15 : ∀t2.eq_bitrig t0E t2 = true → t0E = t2.
687 #t2; ncases t2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
690 nlemma eqbitrig_to_eq16 : ∀t2.eq_bitrig t0F t2 = true → t0F = t2.
691 #t2; ncases t2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
694 nlemma eqbitrig_to_eq17 : ∀t2.eq_bitrig t10 t2 = true → t10 = t2.
695 #t2; ncases t2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
698 nlemma eqbitrig_to_eq18 : ∀t2.eq_bitrig t11 t2 = true → t11 = t2.
699 #t2; ncases t2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
702 nlemma eqbitrig_to_eq19 : ∀t2.eq_bitrig t12 t2 = true → t12 = t2.
703 #t2; ncases t2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
706 nlemma eqbitrig_to_eq20 : ∀t2.eq_bitrig t13 t2 = true → t13 = t2.
707 #t2; ncases t2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
710 nlemma eqbitrig_to_eq21 : ∀t2.eq_bitrig t14 t2 = true → t14 = t2.
711 #t2; ncases t2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
714 nlemma eqbitrig_to_eq22 : ∀t2.eq_bitrig t15 t2 = true → t15 = t2.
715 #t2; ncases t2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
718 nlemma eqbitrig_to_eq23 : ∀t2.eq_bitrig t16 t2 = true → t16 = t2.
719 #t2; ncases t2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
722 nlemma eqbitrig_to_eq24 : ∀t2.eq_bitrig t17 t2 = true → t17 = t2.
723 #t2; ncases t2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
726 nlemma eqbitrig_to_eq25 : ∀t2.eq_bitrig t18 t2 = true → t18 = t2.
727 #t2; ncases t2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
730 nlemma eqbitrig_to_eq26 : ∀t2.eq_bitrig t19 t2 = true → t19 = t2.
731 #t2; ncases t2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
734 nlemma eqbitrig_to_eq27 : ∀t2.eq_bitrig t1A t2 = true → t1A = t2.
735 #t2; ncases t2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
738 nlemma eqbitrig_to_eq28 : ∀t2.eq_bitrig t1B t2 = true → t1B = t2.
739 #t2; ncases t2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
742 nlemma eqbitrig_to_eq29 : ∀t2.eq_bitrig t1C t2 = true → t1C = t2.
743 #t2; ncases t2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
746 nlemma eqbitrig_to_eq30 : ∀t2.eq_bitrig t1D t2 = true → t1D = t2.
747 #t2; ncases t2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
750 nlemma eqbitrig_to_eq31 : ∀t2.eq_bitrig t1E t2 = true → t1E = t2.
751 #t2; ncases t2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
754 nlemma eqbitrig_to_eq32 : ∀t2.eq_bitrig t1F t2 = true → t1F = t2.
755 #t2; ncases t2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (bool_destruct ??? H) ##]
758 nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
761 ##[ ##1: napply eqbitrig_to_eq1
762 ##| ##2: napply eqbitrig_to_eq2
763 ##| ##3: napply eqbitrig_to_eq3
764 ##| ##4: napply eqbitrig_to_eq4
765 ##| ##5: napply eqbitrig_to_eq5
766 ##| ##6: napply eqbitrig_to_eq6
767 ##| ##7: napply eqbitrig_to_eq7
768 ##| ##8: napply eqbitrig_to_eq8
769 ##| ##9: napply eqbitrig_to_eq9
770 ##| ##10: napply eqbitrig_to_eq10
771 ##| ##11: napply eqbitrig_to_eq11
772 ##| ##12: napply eqbitrig_to_eq12
773 ##| ##13: napply eqbitrig_to_eq13
774 ##| ##14: napply eqbitrig_to_eq14
775 ##| ##15: napply eqbitrig_to_eq15
776 ##| ##16: napply eqbitrig_to_eq16
777 ##| ##17: napply eqbitrig_to_eq17
778 ##| ##18: napply eqbitrig_to_eq18
779 ##| ##19: napply eqbitrig_to_eq19
780 ##| ##20: napply eqbitrig_to_eq20
781 ##| ##21: napply eqbitrig_to_eq21
782 ##| ##22: napply eqbitrig_to_eq22
783 ##| ##23: napply eqbitrig_to_eq23
784 ##| ##24: napply eqbitrig_to_eq24
785 ##| ##25: napply eqbitrig_to_eq25
786 ##| ##26: napply eqbitrig_to_eq26
787 ##| ##27: napply eqbitrig_to_eq27
788 ##| ##28: napply eqbitrig_to_eq28
789 ##| ##29: napply eqbitrig_to_eq29
790 ##| ##30: napply eqbitrig_to_eq30
791 ##| ##31: napply eqbitrig_to_eq31
792 ##| ##32: napply eqbitrig_to_eq32
796 nlemma eq_to_eqbitrig1 : ∀t2.t00 = t2 → eq_bitrig t00 t2 = true.
797 #t2; ncases t2; nnormalize; #H; ##[ ##1: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
800 nlemma eq_to_eqbitrig2 : ∀t2.t01 = t2 → eq_bitrig t01 t2 = true.
801 #t2; ncases t2; nnormalize; #H; ##[ ##2: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
804 nlemma eq_to_eqbitrig3 : ∀t2.t02 = t2 → eq_bitrig t02 t2 = true.
805 #t2; ncases t2; nnormalize; #H; ##[ ##3: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
808 nlemma eq_to_eqbitrig4 : ∀t2.t03 = t2 → eq_bitrig t03 t2 = true.
809 #t2; ncases t2; nnormalize; #H; ##[ ##4: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
812 nlemma eq_to_eqbitrig5 : ∀t2.t04 = t2 → eq_bitrig t04 t2 = true.
813 #t2; ncases t2; nnormalize; #H; ##[ ##5: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
816 nlemma eq_to_eqbitrig6 : ∀t2.t05 = t2 → eq_bitrig t05 t2 = true.
817 #t2; ncases t2; nnormalize; #H; ##[ ##6: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
820 nlemma eq_to_eqbitrig7 : ∀t2.t06 = t2 → eq_bitrig t06 t2 = true.
821 #t2; ncases t2; nnormalize; #H; ##[ ##7: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
824 nlemma eq_to_eqbitrig8 : ∀t2.t07 = t2 → eq_bitrig t07 t2 = true.
825 #t2; ncases t2; nnormalize; #H; ##[ ##8: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
828 nlemma eq_to_eqbitrig9 : ∀t2.t08 = t2 → eq_bitrig t08 t2 = true.
829 #t2; ncases t2; nnormalize; #H; ##[ ##9: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
832 nlemma eq_to_eqbitrig10 : ∀t2.t09 = t2 → eq_bitrig t09 t2 = true.
833 #t2; ncases t2; nnormalize; #H; ##[ ##10: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
836 nlemma eq_to_eqbitrig11 : ∀t2.t0A = t2 → eq_bitrig t0A t2 = true.
837 #t2; ncases t2; nnormalize; #H; ##[ ##11: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
840 nlemma eq_to_eqbitrig12 : ∀t2.t0B = t2 → eq_bitrig t0B t2 = true.
841 #t2; ncases t2; nnormalize; #H; ##[ ##12: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
844 nlemma eq_to_eqbitrig13 : ∀t2.t0C = t2 → eq_bitrig t0C t2 = true.
845 #t2; ncases t2; nnormalize; #H; ##[ ##13: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
848 nlemma eq_to_eqbitrig14 : ∀t2.t0D = t2 → eq_bitrig t0D t2 = true.
849 #t2; ncases t2; nnormalize; #H; ##[ ##14: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
852 nlemma eq_to_eqbitrig15 : ∀t2.t0E = t2 → eq_bitrig t0E t2 = true.
853 #t2; ncases t2; nnormalize; #H; ##[ ##15: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
856 nlemma eq_to_eqbitrig16 : ∀t2.t0F = t2 → eq_bitrig t0F t2 = true.
857 #t2; ncases t2; nnormalize; #H; ##[ ##16: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
860 nlemma eq_to_eqbitrig17 : ∀t2.t10 = t2 → eq_bitrig t10 t2 = true.
861 #t2; ncases t2; nnormalize; #H; ##[ ##17: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
864 nlemma eq_to_eqbitrig18 : ∀t2.t11 = t2 → eq_bitrig t11 t2 = true.
865 #t2; ncases t2; nnormalize; #H; ##[ ##18: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
868 nlemma eq_to_eqbitrig19 : ∀t2.t12 = t2 → eq_bitrig t12 t2 = true.
869 #t2; ncases t2; nnormalize; #H; ##[ ##19: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
872 nlemma eq_to_eqbitrig20 : ∀t2.t13 = t2 → eq_bitrig t13 t2 = true.
873 #t2; ncases t2; nnormalize; #H; ##[ ##20: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
876 nlemma eq_to_eqbitrig21 : ∀t2.t14 = t2 → eq_bitrig t14 t2 = true.
877 #t2; ncases t2; nnormalize; #H; ##[ ##21: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
879 nlemma eq_to_eqbitrig22 : ∀t2.t15 = t2 → eq_bitrig t15 t2 = true.
880 #t2; ncases t2; nnormalize; #H; ##[ ##22: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
883 nlemma eq_to_eqbitrig23 : ∀t2.t16 = t2 → eq_bitrig t16 t2 = true.
884 #t2; ncases t2; nnormalize; #H; ##[ ##23: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
887 nlemma eq_to_eqbitrig24 : ∀t2.t17 = t2 → eq_bitrig t17 t2 = true.
888 #t2; ncases t2; nnormalize; #H; ##[ ##24: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
891 nlemma eq_to_eqbitrig25 : ∀t2.t18 = t2 → eq_bitrig t18 t2 = true.
892 #t2; ncases t2; nnormalize; #H; ##[ ##25: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
895 nlemma eq_to_eqbitrig26 : ∀t2.t19 = t2 → eq_bitrig t19 t2 = true.
896 #t2; ncases t2; nnormalize; #H; ##[ ##26: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
899 nlemma eq_to_eqbitrig27 : ∀t2.t1A = t2 → eq_bitrig t1A t2 = true.
900 #t2; ncases t2; nnormalize; #H; ##[ ##27: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
903 nlemma eq_to_eqbitrig28 : ∀t2.t1B = t2 → eq_bitrig t1B t2 = true.
904 #t2; ncases t2; nnormalize; #H; ##[ ##28: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
907 nlemma eq_to_eqbitrig29 : ∀t2.t1C = t2 → eq_bitrig t1C t2 = true.
908 #t2; ncases t2; nnormalize; #H; ##[ ##29: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
911 nlemma eq_to_eqbitrig30 : ∀t2.t1D = t2 → eq_bitrig t1D t2 = true.
912 #t2; ncases t2; nnormalize; #H; ##[ ##30: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
915 nlemma eq_to_eqbitrig31 : ∀t2.t1E = t2 → eq_bitrig t1E t2 = true.
916 #t2; ncases t2; nnormalize; #H; ##[ ##31: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
919 nlemma eq_to_eqbitrig32 : ∀t2.t1F = t2 → eq_bitrig t1F t2 = true.
920 #t2; ncases t2; nnormalize; #H; ##[ ##32: napply (refl_eq ??) ##| ##*: napply (bitrigesim_destruct ??? H) ##]
923 nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
926 ##[ ##1: napply eq_to_eqbitrig1
927 ##| ##2: napply eq_to_eqbitrig2
928 ##| ##3: napply eq_to_eqbitrig3
929 ##| ##4: napply eq_to_eqbitrig4
930 ##| ##5: napply eq_to_eqbitrig5
931 ##| ##6: napply eq_to_eqbitrig6
932 ##| ##7: napply eq_to_eqbitrig7
933 ##| ##8: napply eq_to_eqbitrig8
934 ##| ##9: napply eq_to_eqbitrig9
935 ##| ##10: napply eq_to_eqbitrig10
936 ##| ##11: napply eq_to_eqbitrig11
937 ##| ##12: napply eq_to_eqbitrig12
938 ##| ##13: napply eq_to_eqbitrig13
939 ##| ##14: napply eq_to_eqbitrig14
940 ##| ##15: napply eq_to_eqbitrig15
941 ##| ##16: napply eq_to_eqbitrig16
942 ##| ##17: napply eq_to_eqbitrig17
943 ##| ##18: napply eq_to_eqbitrig18
944 ##| ##19: napply eq_to_eqbitrig19
945 ##| ##20: napply eq_to_eqbitrig20
946 ##| ##21: napply eq_to_eqbitrig21
947 ##| ##22: napply eq_to_eqbitrig22
948 ##| ##23: napply eq_to_eqbitrig23
949 ##| ##24: napply eq_to_eqbitrig24
950 ##| ##25: napply eq_to_eqbitrig25
951 ##| ##26: napply eq_to_eqbitrig26
952 ##| ##27: napply eq_to_eqbitrig27
953 ##| ##28: napply eq_to_eqbitrig28
954 ##| ##29: napply eq_to_eqbitrig29
955 ##| ##30: napply eq_to_eqbitrig30
956 ##| ##31: napply eq_to_eqbitrig31
957 ##| ##32: napply eq_to_eqbitrig32