]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/ng_assembly/freescale/bitrigesim_lemmas.ma
freescale porting, work in progress
[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / bitrigesim_lemmas.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "freescale/bool_lemmas.ma".
24 include "freescale/bitrigesim.ma".
25
26 (* ************* *)
27 (* BITRIGESIMALI *)
28 (* ************* *)
29
30 ndefinition bitrigesim_destruct1 :
31 Πt2:bitrigesim.ΠP:Prop.t00 = t2 → match t2 with [ t00 ⇒ P → P | _ ⇒ P ].
32  #t2; #P;
33  ncases t2;
34  nnormalize; #H;
35  ##[ ##1: napply (λx:P.x)
36  ##| ##*: napply False_ind;
37           nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
38           nrewrite > H; nnormalize; napply I
39  ##]
40 nqed.
41
42 ndefinition bitrigesim_destruct2 :
43 Πt2:bitrigesim.ΠP:Prop.t01 = t2 → match t2 with [ t01 ⇒ P → P | _ ⇒ P ].
44  #t2; #P;
45  ncases t2;
46  nnormalize; #H;
47  ##[ ##2: napply (λx:P.x)
48  ##| ##*: napply False_ind;
49           nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
50           nrewrite > H; nnormalize; napply I
51  ##]
52 nqed.
53
54 ndefinition bitrigesim_destruct3 :
55 Πt2:bitrigesim.ΠP:Prop.t02 = t2 → match t2 with [ t02 ⇒ P → P | _ ⇒ P ].
56  #t2; #P;
57  ncases t2;
58  nnormalize; #H;
59  ##[ ##3: napply (λx:P.x)
60  ##| ##*: napply False_ind;
61           nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
62           nrewrite > H; nnormalize; napply I
63  ##]
64 nqed.
65
66 ndefinition bitrigesim_destruct4 :
67 Πt2:bitrigesim.ΠP:Prop.t03 = t2 → match t2 with [ t03 ⇒ P → P | _ ⇒ P ].
68  #t2; #P;
69  ncases t2;
70  nnormalize; #H;
71  ##[ ##4: napply (λx:P.x)
72  ##| ##*: napply False_ind;
73           nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
74           nrewrite > H; nnormalize; napply I
75  ##]
76 nqed.
77
78 ndefinition bitrigesim_destruct5 :
79 Πt2:bitrigesim.ΠP:Prop.t04 = t2 → match t2 with [ t04 ⇒ P → P | _ ⇒ P ].
80  #t2; #P;
81  ncases t2;
82  nnormalize; #H;
83  ##[ ##5: napply (λx:P.x)
84  ##| ##*: napply False_ind;
85           nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
86           nrewrite > H; nnormalize; napply I
87  ##]
88 nqed.
89
90 ndefinition bitrigesim_destruct6 :
91 Πt2:bitrigesim.ΠP:Prop.t05 = t2 → match t2 with [ t05 ⇒ P → P | _ ⇒ P ].
92  #t2; #P;
93  ncases t2;
94  nnormalize; #H;
95  ##[ ##6: napply (λx:P.x)
96  ##| ##*: napply False_ind;
97           nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
98           nrewrite > H; nnormalize; napply I
99  ##]
100 nqed.
101
102 ndefinition bitrigesim_destruct7 :
103 Πt2:bitrigesim.ΠP:Prop.t06 = t2 → match t2 with [ t06 ⇒ P → P | _ ⇒ P ].
104  #t2; #P;
105  ncases t2;
106  nnormalize; #H;
107  ##[ ##7: napply (λx:P.x)
108  ##| ##*: napply False_ind;
109           nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
110           nrewrite > H; nnormalize; napply I
111  ##]
112 nqed.
113
114 ndefinition bitrigesim_destruct8 :
115 Πt2:bitrigesim.ΠP:Prop.t07 = t2 → match t2 with [ t07 ⇒ P → P | _ ⇒ P ].
116  #t2; #P;
117  ncases t2;
118  nnormalize; #H;
119  ##[ ##8: napply (λx:P.x)
120  ##| ##*: napply False_ind;
121           nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
122           nrewrite > H; nnormalize; napply I
123  ##]
124 nqed.
125
126 ndefinition bitrigesim_destruct9 :
127 Πt2:bitrigesim.ΠP:Prop.t08 = t2 → match t2 with [ t08 ⇒ P → P | _ ⇒ P ].
128  #t2; #P;
129  ncases t2;
130  nnormalize; #H;
131  ##[ ##9: napply (λx:P.x)
132  ##| ##*: napply False_ind;
133           nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
134           nrewrite > H; nnormalize; napply I
135  ##]
136 nqed.
137
138 ndefinition bitrigesim_destruct10 :
139 Πt2:bitrigesim.ΠP:Prop.t09 = t2 → match t2 with [ t09 ⇒ P → P | _ ⇒ P ].
140  #t2; #P;
141  ncases t2;
142  nnormalize; #H;
143  ##[ ##10: napply (λx:P.x)
144  ##| ##*: napply False_ind;
145           nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
146           nrewrite > H; nnormalize; napply I
147  ##]
148 nqed.
149
150 ndefinition bitrigesim_destruct11 :
151 Πt2:bitrigesim.ΠP:Prop.t0A = t2 → match t2 with [ t0A ⇒ P → P | _ ⇒ P ].
152  #t2; #P;
153  ncases t2;
154  nnormalize; #H;
155  ##[ ##11: napply (λx:P.x)
156  ##| ##*: napply False_ind;
157           nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
158           nrewrite > H; nnormalize; napply I
159  ##]
160 nqed.
161
162 ndefinition bitrigesim_destruct12 :
163 Πt2:bitrigesim.ΠP:Prop.t0B = t2 → match t2 with [ t0B ⇒ P → P | _ ⇒ P ].
164  #t2; #P;
165  ncases t2;
166  nnormalize; #H;
167  ##[ ##12: napply (λx:P.x)
168  ##| ##*: napply False_ind;
169           nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
170           nrewrite > H; nnormalize; napply I
171  ##]
172 nqed.
173
174 ndefinition bitrigesim_destruct13 :
175 Πt2:bitrigesim.ΠP:Prop.t0C = t2 → match t2 with [ t0C ⇒ P → P | _ ⇒ P ].
176  #t2; #P;
177  ncases t2;
178  nnormalize; #H;
179  ##[ ##13: napply (λx:P.x)
180  ##| ##*: napply False_ind;
181           nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
182           nrewrite > H; nnormalize; napply I
183  ##]
184 nqed.
185
186 ndefinition bitrigesim_destruct14 :
187 Πt2:bitrigesim.ΠP:Prop.t0D = t2 → match t2 with [ t0D ⇒ P → P | _ ⇒ P ].
188  #t2; #P;
189  ncases t2;
190  nnormalize; #H;
191  ##[ ##14: napply (λx:P.x)
192  ##| ##*: napply False_ind;
193           nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
194           nrewrite > H; nnormalize; napply I
195  ##]
196 nqed.
197
198 ndefinition bitrigesim_destruct15 :
199 Πt2:bitrigesim.ΠP:Prop.t0E = t2 → match t2 with [ t0E ⇒ P → P | _ ⇒ P ].
200  #t2; #P;
201  ncases t2;
202  nnormalize; #H;
203  ##[ ##15: napply (λx:P.x)
204  ##| ##*: napply False_ind;
205           nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
206           nrewrite > H; nnormalize; napply I
207  ##]
208 nqed.
209
210 ndefinition bitrigesim_destruct16 :
211 Πt2:bitrigesim.ΠP:Prop.t0F = t2 → match t2 with [ t0F ⇒ P → P | _ ⇒ P ].
212  #t2; #P;
213  ncases t2;
214  nnormalize; #H;
215  ##[ ##16: napply (λx:P.x)
216  ##| ##*: napply False_ind;
217           nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
218           nrewrite > H; nnormalize; napply I
219  ##]
220 nqed.
221
222 ndefinition bitrigesim_destruct17 :
223 Πt2:bitrigesim.ΠP:Prop.t10 = t2 → match t2 with [ t10 ⇒ P → P | _ ⇒ P ].
224  #t2; #P;
225  ncases t2;
226  nnormalize; #H;
227  ##[ ##17: napply (λx:P.x)
228  ##| ##*: napply False_ind;
229           nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
230           nrewrite > H; nnormalize; napply I
231  ##]
232 nqed.
233
234 ndefinition bitrigesim_destruct18 :
235 Πt2:bitrigesim.ΠP:Prop.t11 = t2 → match t2 with [ t11 ⇒ P → P | _ ⇒ P ].
236  #t2; #P;
237  ncases t2;
238  nnormalize; #H;
239  ##[ ##18: napply (λx:P.x)
240  ##| ##*: napply False_ind;
241           nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
242           nrewrite > H; nnormalize; napply I
243  ##]
244 nqed.
245
246 ndefinition bitrigesim_destruct19 :
247 Πt2:bitrigesim.ΠP:Prop.t12 = t2 → match t2 with [ t12 ⇒ P → P | _ ⇒ P ].
248  #t2; #P;
249  ncases t2;
250  nnormalize; #H;
251  ##[ ##19: napply (λx:P.x)
252  ##| ##*: napply False_ind;
253           nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
254           nrewrite > H; nnormalize; napply I
255  ##]
256 nqed.
257
258 ndefinition bitrigesim_destruct20 :
259 Πt2:bitrigesim.ΠP:Prop.t13 = t2 → match t2 with [ t13 ⇒ P → P | _ ⇒ P ].
260  #t2; #P;
261  ncases t2;
262  nnormalize; #H;
263  ##[ ##20: napply (λx:P.x)
264  ##| ##*: napply False_ind;
265           nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
266           nrewrite > H; nnormalize; napply I
267  ##]
268 nqed.
269
270 ndefinition bitrigesim_destruct21 :
271 Πt2:bitrigesim.ΠP:Prop.t14 = t2 → match t2 with [ t14 ⇒ P → P | _ ⇒ P ].
272  #t2; #P;
273  ncases t2;
274  nnormalize; #H;
275  ##[ ##21: napply (λx:P.x)
276  ##| ##*: napply False_ind;
277           nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
278           nrewrite > H; nnormalize; napply I
279  ##]
280 nqed.
281
282 ndefinition bitrigesim_destruct22 :
283 Πt2:bitrigesim.ΠP:Prop.t15 = t2 → match t2 with [ t15 ⇒ P → P | _ ⇒ P ].
284  #t2; #P;
285  ncases t2;
286  nnormalize; #H;
287  ##[ ##22: napply (λx:P.x)
288  ##| ##*: napply False_ind;
289           nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
290           nrewrite > H; nnormalize; napply I
291  ##]
292 nqed.
293
294 ndefinition bitrigesim_destruct23 :
295 Πt2:bitrigesim.ΠP:Prop.t16 = t2 → match t2 with [ t16 ⇒ P → P | _ ⇒ P ].
296  #t2; #P;
297  ncases t2;
298  nnormalize; #H;
299  ##[ ##23: napply (λx:P.x)
300  ##| ##*: napply False_ind;
301           nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
302           nrewrite > H; nnormalize; napply I
303  ##]
304 nqed.
305
306 ndefinition bitrigesim_destruct24 :
307 Πt2:bitrigesim.ΠP:Prop.t17 = t2 → match t2 with [ t17 ⇒ P → P | _ ⇒ P ].
308  #t2; #P;
309  ncases t2;
310  nnormalize; #H;
311  ##[ ##24: napply (λx:P.x)
312  ##| ##*: napply False_ind;
313           nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
314           nrewrite > H; nnormalize; napply I
315  ##]
316 nqed.
317
318 ndefinition bitrigesim_destruct25 :
319 Πt2:bitrigesim.ΠP:Prop.t18 = t2 → match t2 with [ t18 ⇒ P → P | _ ⇒ P ].
320  #t2; #P;
321  ncases t2;
322  nnormalize; #H;
323  ##[ ##25: napply (λx:P.x)
324  ##| ##*: napply False_ind;
325           nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
326           nrewrite > H; nnormalize; napply I
327  ##]
328 nqed.
329
330 ndefinition bitrigesim_destruct26 :
331 Πt2:bitrigesim.ΠP:Prop.t19 = t2 → match t2 with [ t19 ⇒ P → P | _ ⇒ P ].
332  #t2; #P;
333  ncases t2;
334  nnormalize; #H;
335  ##[ ##26: napply (λx:P.x)
336  ##| ##*: napply False_ind;
337           nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
338           nrewrite > H; nnormalize; napply I
339  ##]
340 nqed.
341
342 ndefinition bitrigesim_destruct27 :
343 Πt2:bitrigesim.ΠP:Prop.t1A = t2 → match t2 with [ t1A ⇒ P → P | _ ⇒ P ].
344  #t2; #P;
345  ncases t2;
346  nnormalize; #H;
347  ##[ ##27: napply (λx:P.x)
348  ##| ##*: napply False_ind;
349           nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
350           nrewrite > H; nnormalize; napply I
351  ##]
352 nqed.
353
354 ndefinition bitrigesim_destruct28 :
355 Πt2:bitrigesim.ΠP:Prop.t1B = t2 → match t2 with [ t1B ⇒ P → P | _ ⇒ P ].
356  #t2; #P;
357  ncases t2;
358  nnormalize; #H;
359  ##[ ##28: napply (λx:P.x)
360  ##| ##*: napply False_ind;
361           nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
362           nrewrite > H; nnormalize; napply I
363  ##]
364 nqed.
365
366 ndefinition bitrigesim_destruct29 :
367 Πt2:bitrigesim.ΠP:Prop.t1C = t2 → match t2 with [ t1C ⇒ P → P | _ ⇒ P ].
368  #t2; #P;
369  ncases t2;
370  nnormalize; #H;
371  ##[ ##29: napply (λx:P.x)
372  ##| ##*: napply False_ind;
373           nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
374           nrewrite > H; nnormalize; napply I
375  ##]
376 nqed.
377
378 ndefinition bitrigesim_destruct30 :
379 Πt2:bitrigesim.ΠP:Prop.t1D = t2 → match t2 with [ t1D ⇒ P → P | _ ⇒ P ].
380  #t2; #P;
381  ncases t2;
382  nnormalize; #H;
383  ##[ ##30: napply (λx:P.x)
384  ##| ##*: napply False_ind;
385           nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
386           nrewrite > H; nnormalize; napply I
387  ##]
388 nqed.
389
390 ndefinition bitrigesim_destruct31 :
391 Πt2:bitrigesim.ΠP:Prop.t1E = t2 → match t2 with [ t1E ⇒ P → P | _ ⇒ P ].
392  #t2; #P;
393  ncases t2;
394  nnormalize; #H;
395  ##[ ##31: napply (λx:P.x)
396  ##| ##*: napply False_ind;
397           nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
398           nrewrite > H; nnormalize; napply I
399  ##]
400 nqed.
401
402 ndefinition bitrigesim_destruct32 :
403 Πt2:bitrigesim.ΠP:Prop.t1F = t2 → match t2 with [ t1F ⇒ P → P | _ ⇒ P ].
404  #t2; #P;
405  ncases t2;
406  nnormalize; #H;
407  ##[ ##32: napply (λx:P.x)
408  ##| ##*: napply False_ind;
409           nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
410           nrewrite > H; nnormalize; napply I
411  ##]
412 nqed.
413
414 ndefinition bitrigesim_destruct_aux ≝
415 Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
416  match t1 with
417   [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
418   | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
419   | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
420   | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
421   | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
422   | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
423   | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
424   | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
425   | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
426   | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
427   | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
428   | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
429   | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
430   | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
431   | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
432   | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
433   | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
434   | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
435   | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
436   | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
437   | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
438   | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
439   | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
440   | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
441   | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
442   | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
443   | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
444   | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
445   | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
446   | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
447   | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
448   | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
449   ].
450
451 ndefinition bitrigesim_destruct : bitrigesim_destruct_aux.
452  #t1;
453  ncases t1;
454  ##[ ##1: napply bitrigesim_destruct1
455  ##| ##2: napply bitrigesim_destruct2
456  ##| ##3: napply bitrigesim_destruct3
457  ##| ##4: napply bitrigesim_destruct4
458  ##| ##5: napply bitrigesim_destruct5
459  ##| ##6: napply bitrigesim_destruct6
460  ##| ##7: napply bitrigesim_destruct7
461  ##| ##8: napply bitrigesim_destruct8
462  ##| ##9: napply bitrigesim_destruct9
463  ##| ##10: napply bitrigesim_destruct10
464  ##| ##11: napply bitrigesim_destruct11
465  ##| ##12: napply bitrigesim_destruct12
466  ##| ##13: napply bitrigesim_destruct13
467  ##| ##14: napply bitrigesim_destruct14
468  ##| ##15: napply bitrigesim_destruct15
469  ##| ##16: napply bitrigesim_destruct16
470  ##| ##17: napply bitrigesim_destruct17
471  ##| ##18: napply bitrigesim_destruct18
472  ##| ##19: napply bitrigesim_destruct19
473  ##| ##20: napply bitrigesim_destruct20
474  ##| ##21: napply bitrigesim_destruct21
475  ##| ##22: napply bitrigesim_destruct22
476  ##| ##23: napply bitrigesim_destruct23
477  ##| ##24: napply bitrigesim_destruct24
478  ##| ##25: napply bitrigesim_destruct25
479  ##| ##26: napply bitrigesim_destruct26
480  ##| ##27: napply bitrigesim_destruct27
481  ##| ##28: napply bitrigesim_destruct28
482  ##| ##29: napply bitrigesim_destruct29
483  ##| ##30: napply bitrigesim_destruct30
484  ##| ##31: napply bitrigesim_destruct31
485  ##| ##32: napply bitrigesim_destruct32
486  ##]
487 nqed.
488
489 nlemma symmetric_eqbit : symmetricT bitrigesim bool eq_bit.
490  #t1;
491  nelim t1;
492  ##[ ##1: #t2; nelim t2; nnormalize; napply refl_eq
493  ##| ##2: #t2; nelim t2; nnormalize; napply refl_eq
494  ##| ##3: #t2; nelim t2; nnormalize; napply refl_eq
495  ##| ##4: #t2; nelim t2; nnormalize; napply refl_eq
496  ##| ##5: #t2; nelim t2; nnormalize; napply refl_eq
497  ##| ##6: #t2; nelim t2; nnormalize; napply refl_eq
498  ##| ##7: #t2; nelim t2; nnormalize; napply refl_eq
499  ##| ##8: #t2; nelim t2; nnormalize; napply refl_eq
500  ##| ##9: #t2; nelim t2; nnormalize; napply refl_eq
501  ##| ##10: #t2; nelim t2; nnormalize; napply refl_eq
502  ##| ##11: #t2; nelim t2; nnormalize; napply refl_eq
503  ##| ##12: #t2; nelim t2; nnormalize; napply refl_eq
504  ##| ##13: #t2; nelim t2; nnormalize; napply refl_eq
505  ##| ##14: #t2; nelim t2; nnormalize; napply refl_eq
506  ##| ##15: #t2; nelim t2; nnormalize; napply refl_eq
507  ##| ##16: #t2; nelim t2; nnormalize; napply refl_eq
508  ##| ##17: #t2; nelim t2; nnormalize; napply refl_eq
509  ##| ##18: #t2; nelim t2; nnormalize; napply refl_eq
510  ##| ##19: #t2; nelim t2; nnormalize; napply refl_eq
511  ##| ##20: #t2; nelim t2; nnormalize; napply refl_eq
512  ##| ##21: #t2; nelim t2; nnormalize; napply refl_eq
513  ##| ##22: #t2; nelim t2; nnormalize; napply refl_eq
514  ##| ##23: #t2; nelim t2; nnormalize; napply refl_eq
515  ##| ##24: #t2; nelim t2; nnormalize; napply refl_eq
516  ##| ##25: #t2; nelim t2; nnormalize; napply refl_eq
517  ##| ##26: #t2; nelim t2; nnormalize; napply refl_eq
518  ##| ##27: #t2; nelim t2; nnormalize; napply refl_eq
519  ##| ##28: #t2; nelim t2; nnormalize; napply refl_eq
520  ##| ##29: #t2; nelim t2; nnormalize; napply refl_eq
521  ##| ##30: #t2; nelim t2; nnormalize; napply refl_eq
522  ##| ##31: #t2; nelim t2; nnormalize; napply refl_eq
523  ##| ##32: #t2; nelim t2; nnormalize; napply refl_eq
524  ##]
525 nqed.
526
527 nlemma eqbit_to_eq1 : ∀t2.eq_bit t00 t2 = true → t00 = t2.
528  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
529 nqed.
530
531 nlemma eqbit_to_eq2 : ∀t2.eq_bit t01 t2 = true → t01 = t2.
532  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
533 nqed.
534
535 nlemma eqbit_to_eq3 : ∀t2.eq_bit t02 t2 = true → t02 = t2.
536  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
537 nqed.
538
539 nlemma eqbit_to_eq4 : ∀t2.eq_bit t03 t2 = true → t03 = t2.
540  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
541 nqed.
542
543 nlemma eqbit_to_eq5 : ∀t2.eq_bit t04 t2 = true → t04 = t2.
544  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
545 nqed.
546
547 nlemma eqbit_to_eq6 : ∀t2.eq_bit t05 t2 = true → t05 = t2.
548  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
549 nqed.
550
551 nlemma eqbit_to_eq7 : ∀t2.eq_bit t06 t2 = true → t06 = t2.
552  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
553 nqed.
554
555 nlemma eqbit_to_eq8 : ∀t2.eq_bit t07 t2 = true → t07 = t2.
556  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
557 nqed.
558
559 nlemma eqbit_to_eq9 : ∀t2.eq_bit t08 t2 = true → t08 = t2.
560  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
561 nqed.
562
563 nlemma eqbit_to_eq10 : ∀t2.eq_bit t09 t2 = true → t09 = t2.
564  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
565 nqed.
566
567 nlemma eqbit_to_eq11 : ∀t2.eq_bit t0A t2 = true → t0A = t2.
568  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
569 nqed.
570
571 nlemma eqbit_to_eq12 : ∀t2.eq_bit t0B t2 = true → t0B = t2.
572  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
573 nqed.
574
575 nlemma eqbit_to_eq13 : ∀t2.eq_bit t0C t2 = true → t0C = t2.
576  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
577 nqed.
578
579 nlemma eqbit_to_eq14 : ∀t2.eq_bit t0D t2 = true → t0D = t2.
580  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
581 nqed.
582
583 nlemma eqbit_to_eq15 : ∀t2.eq_bit t0E t2 = true → t0E = t2.
584  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
585 nqed.
586
587 nlemma eqbit_to_eq16 : ∀t2.eq_bit t0F t2 = true → t0F = t2.
588  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
589 nqed.
590
591 nlemma eqbit_to_eq17 : ∀t2.eq_bit t10 t2 = true → t10 = t2.
592  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
593 nqed.
594
595 nlemma eqbit_to_eq18 : ∀t2.eq_bit t11 t2 = true → t11 = t2.
596  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
597 nqed.
598
599 nlemma eqbit_to_eq19 : ∀t2.eq_bit t12 t2 = true → t12 = t2.
600  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
601 nqed.
602
603 nlemma eqbit_to_eq20 : ∀t2.eq_bit t13 t2 = true → t13 = t2.
604  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
605 nqed.
606
607 nlemma eqbit_to_eq21 : ∀t2.eq_bit t14 t2 = true → t14 = t2.
608  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
609 nqed.
610
611 nlemma eqbit_to_eq22 : ∀t2.eq_bit t15 t2 = true → t15 = t2.
612  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
613 nqed.
614
615 nlemma eqbit_to_eq23 : ∀t2.eq_bit t16 t2 = true → t16 = t2.
616  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
617 nqed.
618
619 nlemma eqbit_to_eq24 : ∀t2.eq_bit t17 t2 = true → t17 = t2.
620  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
621 nqed.
622
623 nlemma eqbit_to_eq25 : ∀t2.eq_bit t18 t2 = true → t18 = t2.
624  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
625 nqed.
626
627 nlemma eqbit_to_eq26 : ∀t2.eq_bit t19 t2 = true → t19 = t2.
628  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
629 nqed.
630
631 nlemma eqbit_to_eq27 : ∀t2.eq_bit t1A t2 = true → t1A = t2.
632  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
633 nqed.
634
635 nlemma eqbit_to_eq28 : ∀t2.eq_bit t1B t2 = true → t1B = t2.
636  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
637 nqed.
638
639 nlemma eqbit_to_eq29 : ∀t2.eq_bit t1C t2 = true → t1C = t2.
640  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
641 nqed.
642
643 nlemma eqbit_to_eq30 : ∀t2.eq_bit t1D t2 = true → t1D = t2.
644  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
645 nqed.
646
647 nlemma eqbit_to_eq31 : ∀t2.eq_bit t1E t2 = true → t1E = t2.
648  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
649 nqed.
650
651 nlemma eqbit_to_eq32 : ∀t2.eq_bit t1F t2 = true → t1F = t2.
652  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bool_destruct … H) ##]
653 nqed.
654
655 nlemma eqbit_to_eq : ∀t1,t2.eq_bit t1 t2 = true → t1 = t2.
656  #t1;
657  ncases t1;
658  ##[ ##1: napply eqbit_to_eq1
659  ##| ##2: napply eqbit_to_eq2
660  ##| ##3: napply eqbit_to_eq3
661  ##| ##4: napply eqbit_to_eq4
662  ##| ##5: napply eqbit_to_eq5
663  ##| ##6: napply eqbit_to_eq6
664  ##| ##7: napply eqbit_to_eq7
665  ##| ##8: napply eqbit_to_eq8
666  ##| ##9: napply eqbit_to_eq9
667  ##| ##10: napply eqbit_to_eq10
668  ##| ##11: napply eqbit_to_eq11
669  ##| ##12: napply eqbit_to_eq12
670  ##| ##13: napply eqbit_to_eq13
671  ##| ##14: napply eqbit_to_eq14
672  ##| ##15: napply eqbit_to_eq15
673  ##| ##16: napply eqbit_to_eq16
674  ##| ##17: napply eqbit_to_eq17
675  ##| ##18: napply eqbit_to_eq18
676  ##| ##19: napply eqbit_to_eq19
677  ##| ##20: napply eqbit_to_eq20
678  ##| ##21: napply eqbit_to_eq21
679  ##| ##22: napply eqbit_to_eq22
680  ##| ##23: napply eqbit_to_eq23
681  ##| ##24: napply eqbit_to_eq24
682  ##| ##25: napply eqbit_to_eq25
683  ##| ##26: napply eqbit_to_eq26
684  ##| ##27: napply eqbit_to_eq27
685  ##| ##28: napply eqbit_to_eq28
686  ##| ##29: napply eqbit_to_eq29
687  ##| ##30: napply eqbit_to_eq30
688  ##| ##31: napply eqbit_to_eq31
689  ##| ##32: napply eqbit_to_eq32
690  ##]
691 nqed.
692
693 nlemma eq_to_eqbit1 : ∀t2.t00 = t2 → eq_bit t00 t2 = true.
694  #t2; ncases t2; nnormalize; #H; ##[ ##1: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
695 nqed.
696
697 nlemma eq_to_eqbit2 : ∀t2.t01 = t2 → eq_bit t01 t2 = true.
698  #t2; ncases t2; nnormalize; #H; ##[ ##2: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
699 nqed.
700
701 nlemma eq_to_eqbit3 : ∀t2.t02 = t2 → eq_bit t02 t2 = true.
702  #t2; ncases t2; nnormalize; #H; ##[ ##3: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
703 nqed.
704
705 nlemma eq_to_eqbit4 : ∀t2.t03 = t2 → eq_bit t03 t2 = true.
706  #t2; ncases t2; nnormalize; #H; ##[ ##4: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
707 nqed.
708
709 nlemma eq_to_eqbit5 : ∀t2.t04 = t2 → eq_bit t04 t2 = true.
710  #t2; ncases t2; nnormalize; #H; ##[ ##5: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
711 nqed.
712
713 nlemma eq_to_eqbit6 : ∀t2.t05 = t2 → eq_bit t05 t2 = true.
714  #t2; ncases t2; nnormalize; #H; ##[ ##6: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
715 nqed.
716
717 nlemma eq_to_eqbit7 : ∀t2.t06 = t2 → eq_bit t06 t2 = true.
718  #t2; ncases t2; nnormalize; #H; ##[ ##7: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
719 nqed.
720
721 nlemma eq_to_eqbit8 : ∀t2.t07 = t2 → eq_bit t07 t2 = true.
722  #t2; ncases t2; nnormalize; #H; ##[ ##8: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
723 nqed.
724
725 nlemma eq_to_eqbit9 : ∀t2.t08 = t2 → eq_bit t08 t2 = true.
726  #t2; ncases t2; nnormalize; #H; ##[ ##9: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
727 nqed.
728
729 nlemma eq_to_eqbit10 : ∀t2.t09 = t2 → eq_bit t09 t2 = true.
730  #t2; ncases t2; nnormalize; #H; ##[ ##10: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
731 nqed.
732
733 nlemma eq_to_eqbit11 : ∀t2.t0A = t2 → eq_bit t0A t2 = true.
734  #t2; ncases t2; nnormalize; #H; ##[ ##11: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
735 nqed.
736
737 nlemma eq_to_eqbit12 : ∀t2.t0B = t2 → eq_bit t0B t2 = true.
738  #t2; ncases t2; nnormalize; #H; ##[ ##12: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
739 nqed.
740
741 nlemma eq_to_eqbit13 : ∀t2.t0C = t2 → eq_bit t0C t2 = true.
742  #t2; ncases t2; nnormalize; #H; ##[ ##13: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
743 nqed.
744
745 nlemma eq_to_eqbit14 : ∀t2.t0D = t2 → eq_bit t0D t2 = true.
746  #t2; ncases t2; nnormalize; #H; ##[ ##14: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
747 nqed.
748
749 nlemma eq_to_eqbit15 : ∀t2.t0E = t2 → eq_bit t0E t2 = true.
750  #t2; ncases t2; nnormalize; #H; ##[ ##15: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
751 nqed.
752
753 nlemma eq_to_eqbit16 : ∀t2.t0F = t2 → eq_bit t0F t2 = true.
754  #t2; ncases t2; nnormalize; #H; ##[ ##16: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
755 nqed.
756
757 nlemma eq_to_eqbit17 : ∀t2.t10 = t2 → eq_bit t10 t2 = true.
758  #t2; ncases t2; nnormalize; #H; ##[ ##17: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
759 nqed.
760
761 nlemma eq_to_eqbit18 : ∀t2.t11 = t2 → eq_bit t11 t2 = true.
762  #t2; ncases t2; nnormalize; #H; ##[ ##18: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
763 nqed.
764
765 nlemma eq_to_eqbit19 : ∀t2.t12 = t2 → eq_bit t12 t2 = true.
766  #t2; ncases t2; nnormalize; #H; ##[ ##19: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
767 nqed.
768
769 nlemma eq_to_eqbit20 : ∀t2.t13 = t2 → eq_bit t13 t2 = true.
770  #t2; ncases t2; nnormalize; #H; ##[ ##20: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
771 nqed.
772
773 nlemma eq_to_eqbit21 : ∀t2.t14 = t2 → eq_bit t14 t2 = true.
774  #t2; ncases t2; nnormalize; #H; ##[ ##21: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
775 nqed.
776
777 nlemma eq_to_eqbit22 : ∀t2.t15 = t2 → eq_bit t15 t2 = true.
778  #t2; ncases t2; nnormalize; #H; ##[ ##22: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
779 nqed.
780
781 nlemma eq_to_eqbit23 : ∀t2.t16 = t2 → eq_bit t16 t2 = true.
782  #t2; ncases t2; nnormalize; #H; ##[ ##23: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
783 nqed.
784
785 nlemma eq_to_eqbit24 : ∀t2.t17 = t2 → eq_bit t17 t2 = true.
786  #t2; ncases t2; nnormalize; #H; ##[ ##24: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
787 nqed.
788
789 nlemma eq_to_eqbit25 : ∀t2.t18 = t2 → eq_bit t18 t2 = true.
790  #t2; ncases t2; nnormalize; #H; ##[ ##25: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
791 nqed.
792
793 nlemma eq_to_eqbit26 : ∀t2.t19 = t2 → eq_bit t19 t2 = true.
794  #t2; ncases t2; nnormalize; #H; ##[ ##26: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
795 nqed.
796
797 nlemma eq_to_eqbit27 : ∀t2.t1A = t2 → eq_bit t1A t2 = true.
798  #t2; ncases t2; nnormalize; #H; ##[ ##27: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
799 nqed.
800
801 nlemma eq_to_eqbit28 : ∀t2.t1B = t2 → eq_bit t1B t2 = true.
802  #t2; ncases t2; nnormalize; #H; ##[ ##28: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
803 nqed.
804
805 nlemma eq_to_eqbit29 : ∀t2.t1C = t2 → eq_bit t1C t2 = true.
806  #t2; ncases t2; nnormalize; #H; ##[ ##29: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
807 nqed.
808
809 nlemma eq_to_eqbit30 : ∀t2.t1D = t2 → eq_bit t1D t2 = true.
810  #t2; ncases t2; nnormalize; #H; ##[ ##30: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
811 nqed.
812
813 nlemma eq_to_eqbit31 : ∀t2.t1E = t2 → eq_bit t1E t2 = true.
814  #t2; ncases t2; nnormalize; #H; ##[ ##31: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
815 nqed.
816
817 nlemma eq_to_eqbit32 : ∀t2.t1F = t2 → eq_bit t1F t2 = true.
818  #t2; ncases t2; nnormalize; #H; ##[ ##32: napply refl_eq ##| ##*: napply (bitrigesim_destruct … H) ##]
819 nqed.
820
821 nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
822  #t1;
823  ncases t1;
824  ##[ ##1: napply eq_to_eqbit1
825  ##| ##2: napply eq_to_eqbit2
826  ##| ##3: napply eq_to_eqbit3
827  ##| ##4: napply eq_to_eqbit4
828  ##| ##5: napply eq_to_eqbit5
829  ##| ##6: napply eq_to_eqbit6
830  ##| ##7: napply eq_to_eqbit7
831  ##| ##8: napply eq_to_eqbit8
832  ##| ##9: napply eq_to_eqbit9
833  ##| ##10: napply eq_to_eqbit10
834  ##| ##11: napply eq_to_eqbit11
835  ##| ##12: napply eq_to_eqbit12
836  ##| ##13: napply eq_to_eqbit13
837  ##| ##14: napply eq_to_eqbit14
838  ##| ##15: napply eq_to_eqbit15
839  ##| ##16: napply eq_to_eqbit16
840  ##| ##17: napply eq_to_eqbit17
841  ##| ##18: napply eq_to_eqbit18
842  ##| ##19: napply eq_to_eqbit19
843  ##| ##20: napply eq_to_eqbit20
844  ##| ##21: napply eq_to_eqbit21
845  ##| ##22: napply eq_to_eqbit22
846  ##| ##23: napply eq_to_eqbit23
847  ##| ##24: napply eq_to_eqbit24
848  ##| ##25: napply eq_to_eqbit25
849  ##| ##26: napply eq_to_eqbit26
850  ##| ##27: napply eq_to_eqbit27
851  ##| ##28: napply eq_to_eqbit28
852  ##| ##29: napply eq_to_eqbit29
853  ##| ##30: napply eq_to_eqbit30
854  ##| ##31: napply eq_to_eqbit31
855  ##| ##32: napply eq_to_eqbit32
856  ##]
857 nqed.