fix to speedup reduction making intermediate conversion problems smaller

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma
index e0c59bab3869df2166db9a80123aaf63353ebf57..addc35386a0fcc96cd361a02775fb5df2d508e7a 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word16.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma
@@ -246,97 +246,97 @@ ninductive rec_word16 : word16 → Type ≝
 ndefinition w16_to_recw16_aux1_1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x1,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? recw
+ w16_S 〈n:〈x0,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? recw
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_2 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x2,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_1 ? recw)
+ w16_S 〈n:〈x1,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_1 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_3 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x3,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_2 ? recw)
+ w16_S 〈n:〈x2,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_2 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_4 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x4,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_3 ? recw)
+ w16_S 〈n:〈x3,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_3 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_5 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x5,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_4 ? recw)
+ w16_S 〈n:〈x4,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_4 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_6 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x6,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_5 ? recw)
+ w16_S 〈n:〈x5,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_5 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_7 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x7,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_6 ? recw)
+ w16_S 〈n:〈x6,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_6 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_8 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x8,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_7 ? recw)
+ w16_S 〈n:〈x7,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_7 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_9 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈x9,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_8 ? recw)
+ w16_S 〈n:〈x8,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_8 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_10 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xA,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_9 ? recw)
+ w16_S 〈n:〈x9,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_9 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_11 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xB,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_10 ? recw)
+ w16_S 〈n:〈xA,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_10 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_12 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xC,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_11 ? recw)
+ w16_S 〈n:〈xB,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_11 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_13 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xD,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_12 ? recw)
+ w16_S 〈n:〈xC,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_12 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_14 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xE,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_13 ? recw)
+ w16_S 〈n:〈xD,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_13 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1_15 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈n:〈xF,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_14 ? recw)
+ w16_S 〈n:〈xE,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_14 ? recw)
  ))))))))))))))).
 
 ndefinition w16_to_recw16_aux1 : Πn.rec_word16 〈n:〈x0,x0〉〉 → rec_word16 〈(succ_b8 n):〈x0,x0〉〉 ≝
 λn.λrecw:rec_word16 〈n:〈x0,x0〉〉.
  w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (
- w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_15 ? recw)
+ w16_S 〈n:〈xF,x7〉〉 (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_S ? (w16_to_recw16_aux1_15 ? recw)
  ))))))))))))))).
 
 (* ... cifra byte superiore *)
@@ -369,10 +369,7 @@ ndefinition w16_to_recw16_aux3 ≝
  ].
 
 nlemma w16_to_recw16_aux4_1 : Πn,e.rec_word16 〈n:〈e,x0〉〉 → rec_word16 〈n:〈e,x1〉〉.
- #n; #e;
- (* non funziona nelim e *)
-  #H;
- nelim e in H:(%) ⊢ %; 
+ #n; #e; nelim e;
  #input; napply (w16_S ? input).
 nqed.