1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / exadecim_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
index e6be57877ae3b5f6d799dbd9b05d9b1367edea0a..7b361a2cbe81d946edb7829d811455d64ccbdfe8 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/exadecim_lemmas.ma
@@ -218,7 +218,7 @@ nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
@@ -226,28 +226,28 @@ nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
  #e1; #e2; #e3;
  nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
+ ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
  ##]
 nqed.
 
@@ -256,28 +256,28 @@ nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
  #e1; #e2; #e3;
  nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
+ ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
  ##]
 nqed.
 
@@ -286,28 +286,28 @@ nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
  #e1; #e2; #e3;
  nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
+ ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
  ##]
 nqed.
 
@@ -317,25 +317,25 @@ nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc
  nelim e2;
  nelim c;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
-nlemma plusex_dc_dc_to_dc_d : ∀e1,e2,c.fst ?? (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_d e1 e2 c.
+nlemma plusex_dc_dc_to_dc_d : ∀e1,e2,c.fst … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_d e1 e2 c.
  #e1; #e2; #c;
  nelim e1;
  nelim e2;
  nelim c;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
-nlemma plusex_dc_dc_to_dc_c : ∀e1,e2,c.snd ?? (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_c e1 e2 c.
+nlemma plusex_dc_dc_to_dc_c : ∀e1,e2,c.snd … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_c e1 e2 c.
  #e1; #e2; #c;
  nelim e1;
  nelim e2;
  nelim c;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
@@ -343,23 +343,23 @@ nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
-nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst ?? (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
+nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
  #e1; #e2;
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
-nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd ?? (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
+nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
  #e1; #e2;
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
@@ -368,7 +368,7 @@ nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2
  nelim e2;
  nelim c;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
@@ -377,7 +377,7 @@ nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2
  nelim e2;
  nelim c;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
@@ -385,23 +385,23 @@ nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
-nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst ?? (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
+nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst … (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
  #e1; #e2;
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
-nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd ?? (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
+nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd … (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
  #e1; #e2;
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
@@ -409,28 +409,28 @@ nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)).
  #e1; #e2; #e3;
  nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
- ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
+ ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
+ ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
  ##]
 nqed.
 
@@ -439,7 +439,7 @@ nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
@@ -447,8 +447,8 @@ nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
  ncases e1;
  ncases e2;
  nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -457,7 +457,7 @@ nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
  ncases m1;
  ncases m2;
  nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (exadecim_destruct ??? H)
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
+ ##| ##*: #H; napply (exadecim_destruct … H)
  ##]
 nqed.