--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: *)
+(* Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* *)
+(* Questo materiale fa parte della tesi: *)
+(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *)
+(* *)
+(* data ultima modifica 15/11/2007 *)
+(* ********************************************************************** *)
+
+include "freescale/bool_lemmas.ma".
+include "freescale/aux_bases.ma".
+
+(* ****** *)
+(* OTTALI *)
+(* ****** *)
+
+ndefinition oct_destruct :
+ Πn1,n2:oct.ΠP:Prop.n1 = n2 →
+ match n1 with
+ [ o0 ⇒ match n2 with [ o0 ⇒ P → P | _ ⇒ P ]
+ | o1 ⇒ match n2 with [ o1 ⇒ P → P | _ ⇒ P ]
+ | o2 ⇒ match n2 with [ o2 ⇒ P → P | _ ⇒ P ]
+ | o3 ⇒ match n2 with [ o3 ⇒ P → P | _ ⇒ P ]
+ | o4 ⇒ match n2 with [ o4 ⇒ P → P | _ ⇒ P ]
+ | o5 ⇒ match n2 with [ o5 ⇒ P → P | _ ⇒ P ]
+ | o6 ⇒ match n2 with [ o6 ⇒ P → P | _ ⇒ P ]
+ | o7 ⇒ match n2 with [ o7 ⇒ P → P | _ ⇒ P ]
+ ].
+ #n1; #n2; #P;
+ nelim n1;
+ ##[ ##1: nelim n2; nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o0 with [ o0 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##2: nelim n2; nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o1 with [ o1 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##3: nelim n2; nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o2 with [ o2 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##4: nelim n2; nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o3 with [ o3 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##5: nelim n2; nnormalize; #H;
+ ##[ ##5: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o4 with [ o4 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##6: nelim n2; nnormalize; #H;
+ ##[ ##6: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o5 with [ o5 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##7: nelim n2; nnormalize; #H;
+ ##[ ##7: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o6 with [ o6 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##8: nelim n2; nnormalize; #H;
+ ##[ ##8: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match o7 with [ o7 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##]
+nqed.
+
+nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
+ #n1; #n2;
+ nelim n1;
+ nelim n2;
+ nnormalize;
+ napply (refl_eq ??).
+nqed.
+
+nlemma eqoct_to_eq : ∀o1,o2.eq_oct o1 o2 = true → o1 = o2.
+ #n1; #n2; #H;
+ nletin K ≝ (bool_destruct ?? (n1 = n2) H);
+ nelim n1 in K:(%) ⊢ %;
+ nelim n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply H
+ ##]
+nqed.
+
+nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
+ #n1; #n2; #H;
+ nletin K ≝ (oct_destruct ?? (eq_oct n1 n2 = true) H);
+ nelim n1 in K:(%) ⊢ %;
+ nelim n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
+ ##| ##*: #H; napply H
+ ##]
+nqed.
+
+(* ************* *)
+(* BITRIGESIMALI *)
+(* ************* *)
+
+ndefinition bitrigesim_destruct :
+ Πt1,t2:bitrigesim.ΠP:Prop.t1 = t2 →
+ match t1 with
+ [ t00 ⇒ match t2 with [ t00 ⇒ P → P | _ ⇒ P ]
+ | t01 ⇒ match t2 with [ t01 ⇒ P → P | _ ⇒ P ]
+ | t02 ⇒ match t2 with [ t02 ⇒ P → P | _ ⇒ P ]
+ | t03 ⇒ match t2 with [ t03 ⇒ P → P | _ ⇒ P ]
+ | t04 ⇒ match t2 with [ t04 ⇒ P → P | _ ⇒ P ]
+ | t05 ⇒ match t2 with [ t05 ⇒ P → P | _ ⇒ P ]
+ | t06 ⇒ match t2 with [ t06 ⇒ P → P | _ ⇒ P ]
+ | t07 ⇒ match t2 with [ t07 ⇒ P → P | _ ⇒ P ]
+ | t08 ⇒ match t2 with [ t08 ⇒ P → P | _ ⇒ P ]
+ | t09 ⇒ match t2 with [ t09 ⇒ P → P | _ ⇒ P ]
+ | t0A ⇒ match t2 with [ t0A ⇒ P → P | _ ⇒ P ]
+ | t0B ⇒ match t2 with [ t0B ⇒ P → P | _ ⇒ P ]
+ | t0C ⇒ match t2 with [ t0C ⇒ P → P | _ ⇒ P ]
+ | t0D ⇒ match t2 with [ t0D ⇒ P → P | _ ⇒ P ]
+ | t0E ⇒ match t2 with [ t0E ⇒ P → P | _ ⇒ P ]
+ | t0F ⇒ match t2 with [ t0F ⇒ P → P | _ ⇒ P ]
+ | t10 ⇒ match t2 with [ t10 ⇒ P → P | _ ⇒ P ]
+ | t11 ⇒ match t2 with [ t11 ⇒ P → P | _ ⇒ P ]
+ | t12 ⇒ match t2 with [ t12 ⇒ P → P | _ ⇒ P ]
+ | t13 ⇒ match t2 with [ t13 ⇒ P → P | _ ⇒ P ]
+ | t14 ⇒ match t2 with [ t14 ⇒ P → P | _ ⇒ P ]
+ | t15 ⇒ match t2 with [ t15 ⇒ P → P | _ ⇒ P ]
+ | t16 ⇒ match t2 with [ t16 ⇒ P → P | _ ⇒ P ]
+ | t17 ⇒ match t2 with [ t17 ⇒ P → P | _ ⇒ P ]
+ | t18 ⇒ match t2 with [ t18 ⇒ P → P | _ ⇒ P ]
+ | t19 ⇒ match t2 with [ t19 ⇒ P → P | _ ⇒ P ]
+ | t1A ⇒ match t2 with [ t1A ⇒ P → P | _ ⇒ P ]
+ | t1B ⇒ match t2 with [ t1B ⇒ P → P | _ ⇒ P ]
+ | t1C ⇒ match t2 with [ t1C ⇒ P → P | _ ⇒ P ]
+ | t1D ⇒ match t2 with [ t1D ⇒ P → P | _ ⇒ P ]
+ | t1E ⇒ match t2 with [ t1E ⇒ P → P | _ ⇒ P ]
+ | t1F ⇒ match t2 with [ t1F ⇒ P → P | _ ⇒ P ]
+ ].
+ #t1; #t2; #P;
+ nelim t1;
+ ##[ ##1: nelim t2; nnormalize; #H;
+ ##[ ##1: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t00 with [ t00 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##2: nelim t2; nnormalize; #H;
+ ##[ ##2: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t01 with [ t01 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##3: nelim t2; nnormalize; #H;
+ ##[ ##3: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t02 with [ t02 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##4: nelim t2; nnormalize; #H;
+ ##[ ##4: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t03 with [ t03 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##5: nelim t2; nnormalize; #H;
+ ##[ ##5: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t04 with [ t04 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##6: nelim t2; nnormalize; #H;
+ ##[ ##6: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t05 with [ t05 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##7: nelim t2; nnormalize; #H;
+ ##[ ##7: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t06 with [ t06 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##8: nelim t2; nnormalize; #H;
+ ##[ ##8: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t07 with [ t07 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##9: nelim t2; nnormalize; #H;
+ ##[ ##9: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t08 with [ t08 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##10: nelim t2; nnormalize; #H;
+ ##[ ##10: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t09 with [ t09 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##11: nelim t2; nnormalize; #H;
+ ##[ ##11: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0A with [ t0A ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##12: nelim t2; nnormalize; #H;
+ ##[ ##12: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0B with [ t0B ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##13: nelim t2; nnormalize; #H;
+ ##[ ##13: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0C with [ t0C ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##14: nelim t2; nnormalize; #H;
+ ##[ ##14: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0D with [ t0D ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##15: nelim t2; nnormalize; #H;
+ ##[ ##15: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0E with [ t0E ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##16: nelim t2; nnormalize; #H;
+ ##[ ##16: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t0F with [ t0F ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##17: nelim t2; nnormalize; #H;
+ ##[ ##17: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t10 with [ t10 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##18: nelim t2; nnormalize; #H;
+ ##[ ##18: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t11 with [ t11 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##19: nelim t2; nnormalize; #H;
+ ##[ ##19: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t12 with [ t12 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##20: nelim t2; nnormalize; #H;
+ ##[ ##20: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t13 with [ t13 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##21: nelim t2; nnormalize; #H;
+ ##[ ##21: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t14 with [ t14 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##22: nelim t2; nnormalize; #H;
+ ##[ ##22: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t15 with [ t15 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##23: nelim t2; nnormalize; #H;
+ ##[ ##23: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t16 with [ t16 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##24: nelim t2; nnormalize; #H;
+ ##[ ##24: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t17 with [ t17 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##25: nelim t2; nnormalize; #H;
+ ##[ ##25: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t18 with [ t18 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##26: nelim t2; nnormalize; #H;
+ ##[ ##26: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t19 with [ t19 ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##27: nelim t2; nnormalize; #H;
+ ##[ ##27: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1A with [ t1A ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##28: nelim t2; nnormalize; #H;
+ ##[ ##28: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1B with [ t1B ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##29: nelim t2; nnormalize; #H;
+ ##[ ##29: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1C with [ t1C ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##30: nelim t2; nnormalize; #H;
+ ##[ ##30: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1D with [ t1D ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##31: nelim t2; nnormalize; #H;
+ ##[ ##31: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1E with [ t1E ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##| ##32: nelim t2; nnormalize; #H;
+ ##[ ##32: napply (λx:P.x)
+ ##| ##*: napply (False_ind ??);
+ nchange with (match t1F with [ t1F ⇒ False | _ ⇒ True ]);
+ nrewrite > H; nnormalize; napply I
+ ##]
+ ##]
+nqed.
+
+nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
+ #t1;
+ nelim t1;
+ ##[ ##1: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##2: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##3: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##4: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##5: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##6: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##7: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##8: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##9: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##10: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##11: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##12: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##13: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##14: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##15: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##16: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##17: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##18: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##19: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##20: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##21: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##22: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##23: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##24: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##25: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##26: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##27: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##28: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##29: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##30: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##31: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##| ##32: #t2; nelim t2; nnormalize; napply (refl_eq ??)
+ ##]
+nqed.
+
+nlemma eqbitrig_to_eq : ∀t1,t2.eq_bitrig t1 t2 = true → t1 = t2.
+ #t1; #t2; #H;
+ nletin K ≝ (bool_destruct ?? (t1 = t2) H);
+ nelim t1 in K:(%) ⊢ %;
+ ##[ ##1: nelim t2; nnormalize; #H;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##2: nelim t2; nnormalize; #H;
+ ##[ ##2: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##3: nelim t2; nnormalize; #H;
+ ##[ ##3: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##4: nelim t2; nnormalize; #H;
+ ##[ ##4: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##5: nelim t2; nnormalize; #H;
+ ##[ ##5: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##6: nelim t2; nnormalize; #H;
+ ##[ ##6: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##7: nelim t2; nnormalize; #H;
+ ##[ ##7: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##8: nelim t2; nnormalize; #H;
+ ##[ ##8: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##9: nelim t2; nnormalize; #H;
+ ##[ ##9: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##10: nelim t2; nnormalize; #H;
+ ##[ ##10: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##11: nelim t2; nnormalize; #H;
+ ##[ ##11: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##12: nelim t2; nnormalize; #H;
+ ##[ ##12: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##13: nelim t2; nnormalize; #H;
+ ##[ ##13: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##14: nelim t2; nnormalize; #H;
+ ##[ ##14: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##15: nelim t2; nnormalize; #H;
+ ##[ ##15: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##16: nelim t2; nnormalize; #H;
+ ##[ ##16: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##17: nelim t2; nnormalize; #H;
+ ##[ ##17: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##18: nelim t2; nnormalize; #H;
+ ##[ ##18: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##19: nelim t2; nnormalize; #H;
+ ##[ ##19: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##20: nelim t2; nnormalize; #H;
+ ##[ ##20: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##21: nelim t2; nnormalize; #H;
+ ##[ ##21: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##22: nelim t2; nnormalize; #H;
+ ##[ ##22: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##23: nelim t2; nnormalize; #H;
+ ##[ ##23: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##24: nelim t2; nnormalize; #H;
+ ##[ ##24: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##25: nelim t2; nnormalize; #H;
+ ##[ ##25: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##26: nelim t2; nnormalize; #H;
+ ##[ ##26: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##27: nelim t2; nnormalize; #H;
+ ##[ ##27: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##28: nelim t2; nnormalize; #H;
+ ##[ ##28: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##29: nelim t2; nnormalize; #H;
+ ##[ ##29: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##30: nelim t2; nnormalize; #H;
+ ##[ ##30: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##31: nelim t2; nnormalize; #H;
+ ##[ ##31: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##32: nelim t2; nnormalize; #H;
+ ##[ ##32: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##]
+nqed.
+
+nlemma eq_to_eqbitrig : ∀t1,t2.t1 = t2 → eq_bitrig t1 t2 = true.
+ #t1; #t2; #H;
+ nletin K ≝ (bitrigesim_destruct ?? (eq_bitrig t1 t2 = true) H);
+ nelim t1 in K:(%) ⊢ %;
+ ##[ ##1: nelim t2; nnormalize; #H;
+ ##[ ##1: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##2: nelim t2; nnormalize; #H;
+ ##[ ##2: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##3: nelim t2; nnormalize; #H;
+ ##[ ##3: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##4: nelim t2; nnormalize; #H;
+ ##[ ##4: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##5: nelim t2; nnormalize; #H;
+ ##[ ##5: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##6: nelim t2; nnormalize; #H;
+ ##[ ##6: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##7: nelim t2; nnormalize; #H;
+ ##[ ##7: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##8: nelim t2; nnormalize; #H;
+ ##[ ##8: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##9: nelim t2; nnormalize; #H;
+ ##[ ##9: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##10: nelim t2; nnormalize; #H;
+ ##[ ##10: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##11: nelim t2; nnormalize; #H;
+ ##[ ##11: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##12: nelim t2; nnormalize; #H;
+ ##[ ##12: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##13: nelim t2; nnormalize; #H;
+ ##[ ##13: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##14: nelim t2; nnormalize; #H;
+ ##[ ##14: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##15: nelim t2; nnormalize; #H;
+ ##[ ##15: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##16: nelim t2; nnormalize; #H;
+ ##[ ##16: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##17: nelim t2; nnormalize; #H;
+ ##[ ##17: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##18: nelim t2; nnormalize; #H;
+ ##[ ##18: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##19: nelim t2; nnormalize; #H;
+ ##[ ##19: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##20: nelim t2; nnormalize; #H;
+ ##[ ##20: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##21: nelim t2; nnormalize; #H;
+ ##[ ##21: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##22: nelim t2; nnormalize; #H;
+ ##[ ##22: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##23: nelim t2; nnormalize; #H;
+ ##[ ##23: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##24: nelim t2; nnormalize; #H;
+ ##[ ##24: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##25: nelim t2; nnormalize; #H;
+ ##[ ##25: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##26: nelim t2; nnormalize; #H;
+ ##[ ##26: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##27: nelim t2; nnormalize; #H;
+ ##[ ##27: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##28: nelim t2; nnormalize; #H;
+ ##[ ##28: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##29: nelim t2; nnormalize; #H;
+ ##[ ##29: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##30: nelim t2; nnormalize; #H;
+ ##[ ##30: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##31: nelim t2; nnormalize; #H;
+ ##[ ##31: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##| ##32: nelim t2; nnormalize; #H;
+ ##[ ##32: napply (refl_eq ??)
+ ##| ##*: napply H
+ ##]
+ ##]
+nqed.
projects / helm.git / blobdiff