X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Faux_bases_lemmas.ma;h=55ef3df2367d79e1a56441ff9899ea087eec39be;hb=c3fc204cc02f1031b5d17fb0f2be1fc01e5c452f;hp=c85df6e61b4d27528e74dae147e4b6532044a418;hpb=3e5c359c75874748cfed8a9046031b62396e0e6d;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
index c85df6e61..55ef3df23 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/aux_bases_lemmas.ma
@@ -104,25 +104,23 @@ nlemma symmetric_eqoct : symmetricT oct bool eq_oct.
  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;
+nlemma eqoct_to_eq : ∀n1,n2.eq_oct n1 n2 = true → n1 = n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
  nnormalize;
  ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (bool_destruct ??? 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;
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
  nnormalize;
  ##[ ##1,10,19,28,37,46,55,64: #H; napply (refl_eq ??)
- ##| ##*: #H; napply H
+ ##| ##*: #H; napply (oct_destruct ??? H)
  ##]
 nqed.
 
@@ -402,271 +400,269 @@ nlemma symmetric_eqbitrig : symmetricT bitrigesim bool eq_bitrig.
 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;
+ #t1; #t2;
+ ncases t1;
+ ##[ ##1: ncases t2; nnormalize; #H;
           ##[ ##1: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##2: nelim t2; nnormalize; #H;
+ ##| ##2: ncases t2; nnormalize; #H;
           ##[ ##2: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]          
- ##| ##3: nelim t2; nnormalize; #H;
+ ##| ##3: ncases t2; nnormalize; #H;
           ##[ ##3: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##4: nelim t2; nnormalize; #H;
+ ##| ##4: ncases t2; nnormalize; #H;
           ##[ ##4: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##5: nelim t2; nnormalize; #H;
+ ##| ##5: ncases t2; nnormalize; #H;
           ##[ ##5: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##6: nelim t2; nnormalize; #H;
+ ##| ##6: ncases t2; nnormalize; #H;
           ##[ ##6: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*:napply (bool_destruct ??? H)
           ##]
- ##| ##7: nelim t2; nnormalize; #H;
+ ##| ##7: ncases t2; nnormalize; #H;
           ##[ ##7: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##8: nelim t2; nnormalize; #H;
+ ##| ##8: ncases t2; nnormalize; #H;
           ##[ ##8: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##9: nelim t2; nnormalize; #H;
+ ##| ##9: ncases t2; nnormalize; #H;
           ##[ ##9: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##10: nelim t2; nnormalize; #H;
+ ##| ##10: ncases t2; nnormalize; #H;
           ##[ ##10: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##11: nelim t2; nnormalize; #H;
+ ##| ##11: ncases t2; nnormalize; #H;
           ##[ ##11: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]            
- ##| ##12: nelim t2; nnormalize; #H;
+ ##| ##12: ncases t2; nnormalize; #H;
           ##[ ##12: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##13: nelim t2; nnormalize; #H;
+ ##| ##13: ncases t2; nnormalize; #H;
           ##[ ##13: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##14: nelim t2; nnormalize; #H;
+ ##| ##14: ncases t2; nnormalize; #H;
           ##[ ##14: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##15: nelim t2; nnormalize; #H;
+ ##| ##15: ncases t2; nnormalize; #H;
           ##[ ##15: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]            
- ##| ##16: nelim t2; nnormalize; #H;
+ ##| ##16: ncases t2; nnormalize; #H;
           ##[ ##16: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##17: nelim t2; nnormalize; #H;
+ ##| ##17: ncases t2; nnormalize; #H;
           ##[ ##17: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##18: nelim t2; nnormalize; #H;
+ ##| ##18: ncases t2; nnormalize; #H;
           ##[ ##18: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##19: nelim t2; nnormalize; #H;
+ ##| ##19: ncases t2; nnormalize; #H;
           ##[ ##19: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]            
- ##| ##20: nelim t2; nnormalize; #H;
+ ##| ##20: ncases t2; nnormalize; #H;
           ##[ ##20: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##21: nelim t2; nnormalize; #H;
+ ##| ##21: ncases t2; nnormalize; #H;
           ##[ ##21: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##22: nelim t2; nnormalize; #H;
+ ##| ##22: ncases t2; nnormalize; #H;
           ##[ ##22: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##23: nelim t2; nnormalize; #H;
+ ##| ##23: ncases t2; nnormalize; #H;
           ##[ ##23: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##24: nelim t2; nnormalize; #H;
+ ##| ##24: ncases t2; nnormalize; #H;
           ##[ ##24: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##25: nelim t2; nnormalize; #H;
+ ##| ##25: ncases t2; nnormalize; #H;
           ##[ ##25: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##26: nelim t2; nnormalize; #H;
+ ##| ##26: ncases t2; nnormalize; #H;
           ##[ ##26: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##27: nelim t2; nnormalize; #H;
+ ##| ##27: ncases t2; nnormalize; #H;
           ##[ ##27: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##28: nelim t2; nnormalize; #H;
+ ##| ##28: ncases t2; nnormalize; #H;
           ##[ ##28: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##29: nelim t2; nnormalize; #H;
+ ##| ##29: ncases t2; nnormalize; #H;
           ##[ ##29: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##30: nelim t2; nnormalize; #H;
+ ##| ##30: ncases t2; nnormalize; #H;
           ##[ ##30: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##31: nelim t2; nnormalize; #H;
+ ##| ##31: ncases t2; nnormalize; #H;
           ##[ ##31: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? H)
           ##]
- ##| ##32: nelim t2; nnormalize; #H;
+ ##| ##32: ncases t2; nnormalize; #H;
           ##[ ##32: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bool_destruct ??? 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;
+ #t1; #t2;
+ ncases t1;
+ ##[ ##1: ncases t2; nnormalize; #H;
           ##[ ##1: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##2: nelim t2; nnormalize; #H;
+ ##| ##2: ncases t2; nnormalize; #H;
           ##[ ##2: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]          
- ##| ##3: nelim t2; nnormalize; #H;
+ ##| ##3: ncases t2; nnormalize; #H;
           ##[ ##3: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##4: nelim t2; nnormalize; #H;
+ ##| ##4: ncases t2; nnormalize; #H;
           ##[ ##4: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##5: nelim t2; nnormalize; #H;
+ ##| ##5: ncases t2; nnormalize; #H;
           ##[ ##5: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##6: nelim t2; nnormalize; #H;
+ ##| ##6: ncases t2; nnormalize; #H;
           ##[ ##6: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##7: nelim t2; nnormalize; #H;
+ ##| ##7: ncases t2; nnormalize; #H;
           ##[ ##7: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##8: nelim t2; nnormalize; #H;
+ ##| ##8: ncases t2; nnormalize; #H;
           ##[ ##8: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##9: nelim t2; nnormalize; #H;
+ ##| ##9: ncases t2; nnormalize; #H;
           ##[ ##9: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##10: nelim t2; nnormalize; #H;
+ ##| ##10: ncases t2; nnormalize; #H;
           ##[ ##10: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##11: nelim t2; nnormalize; #H;
+ ##| ##11: ncases t2; nnormalize; #H;
           ##[ ##11: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]            
- ##| ##12: nelim t2; nnormalize; #H;
+ ##| ##12: ncases t2; nnormalize; #H;
           ##[ ##12: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##13: nelim t2; nnormalize; #H;
+ ##| ##13: ncases t2; nnormalize; #H;
           ##[ ##13: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##14: nelim t2; nnormalize; #H;
+ ##| ##14: ncases t2; nnormalize; #H;
           ##[ ##14: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##15: nelim t2; nnormalize; #H;
+ ##| ##15: ncases t2; nnormalize; #H;
           ##[ ##15: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]            
- ##| ##16: nelim t2; nnormalize; #H;
+ ##| ##16: ncases t2; nnormalize; #H;
           ##[ ##16: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##17: nelim t2; nnormalize; #H;
+ ##| ##17: ncases t2; nnormalize; #H;
           ##[ ##17: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##18: nelim t2; nnormalize; #H;
+ ##| ##18: ncases t2; nnormalize; #H;
           ##[ ##18: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##19: nelim t2; nnormalize; #H;
+ ##| ##19: ncases t2; nnormalize; #H;
           ##[ ##19: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]            
- ##| ##20: nelim t2; nnormalize; #H;
+ ##| ##20: ncases t2; nnormalize; #H;
           ##[ ##20: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##21: nelim t2; nnormalize; #H;
+ ##| ##21: ncases t2; nnormalize; #H;
           ##[ ##21: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##22: nelim t2; nnormalize; #H;
+ ##| ##22: ncases t2; nnormalize; #H;
           ##[ ##22: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##23: nelim t2; nnormalize; #H;
+ ##| ##23: ncases t2; nnormalize; #H;
           ##[ ##23: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##24: nelim t2; nnormalize; #H;
+ ##| ##24: ncases t2; nnormalize; #H;
           ##[ ##24: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##25: nelim t2; nnormalize; #H;
+ ##| ##25: ncases t2; nnormalize; #H;
           ##[ ##25: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##26: nelim t2; nnormalize; #H;
+ ##| ##26: ncases t2; nnormalize; #H;
           ##[ ##26: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##27: nelim t2; nnormalize; #H;
+ ##| ##27: ncases t2; nnormalize; #H;
           ##[ ##27: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##28: nelim t2; nnormalize; #H;
+ ##| ##28: ncases t2; nnormalize; #H;
           ##[ ##28: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##29: nelim t2; nnormalize; #H;
+ ##| ##29: ncases t2; nnormalize; #H;
           ##[ ##29: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##30: nelim t2; nnormalize; #H;
+ ##| ##30: ncases t2; nnormalize; #H;
           ##[ ##30: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##31: nelim t2; nnormalize; #H;
+ ##| ##31: ncases t2; nnormalize; #H;
           ##[ ##31: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
- ##| ##32: nelim t2; nnormalize; #H;
+ ##| ##32: ncases t2; nnormalize; #H;
           ##[ ##32: napply (refl_eq ??)
-          ##| ##*: napply H
+          ##| ##*: napply (bitrigesim_destruct ??? H)
           ##]
  ##]
 nqed.