1) \ldots here and there

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma
index 8d8f526b7e7f08e4d04a2f582dd436bb4cf16c59..ad383d2ab72567b38e03afbee6e8b7d285bbaff0 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas_instrmode1.ma
@@ -543,7 +543,7 @@ nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 →
  nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 ndefinition instr_mode_destruct31 :
@@ -571,7 +571,7 @@ ndefinition instr_mode_destruct31 :
      ncases n2;
      nnormalize;
      ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
-     ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn ?? H))
+     ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn … H))
      ##]
 nqed.
 
@@ -580,7 +580,7 @@ nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 =
  nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 ndefinition instr_mode_destruct32 :
@@ -608,7 +608,7 @@ ndefinition instr_mode_destruct32 :
      ncases n2;
      nnormalize;
      ##[ ##1,10,19,28,37,46,55,64: #H; napply (λx:P.x)
-     ##| ##*: #H; napply (oct_destruct ??? (instr_mode_destruct_MODE_DIRn_and_IMM1 ?? H))
+     ##| ##*: #H; napply (oct_destruct … (instr_mode_destruct_MODE_DIRn_and_IMM1 … H))
      ##]
 nqed.
 
@@ -617,7 +617,7 @@ nlemma instr_mode_destruct_MODE_TNY : ∀n1,n2.MODE_TNY n1 = MODE_TNY n2 → n1
  nchange with (match MODE_TNY n2 with [ MODE_TNY a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 ndefinition instr_mode_destruct33 :
@@ -649,7 +649,7 @@ ndefinition instr_mode_destruct33 :
      ncases n2;
      nnormalize;
      ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (λx:P.x)
-     ##| ##*: #H; napply (exadecim_destruct ??? (instr_mode_destruct_MODE_TNY ?? H))
+     ##| ##*: #H; napply (exadecim_destruct … (instr_mode_destruct_MODE_TNY … H))
      ##]
 nqed.
 
@@ -658,7 +658,7 @@ nlemma instr_mode_destruct_MODE_SRT : ∀n1,n2.MODE_SRT n1 = MODE_SRT n2 → n1
  nchange with (match MODE_SRT n2 with [ MODE_SRT a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 ndefinition instr_mode_destruct34 :
@@ -697,131 +697,131 @@ ndefinition instr_mode_destruct34 :
      ncases n1;
      ##[ ##1: ncases n2; nnormalize;
               ##[ ##1: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##2: ncases n2; nnormalize;
               ##[ ##2: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##3: ncases n2; nnormalize;
               ##[ ##3: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##4: ncases n2; nnormalize;
               ##[ ##4: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##5: ncases n2; nnormalize;
               ##[ ##5: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##6: ncases n2; nnormalize;
               ##[ ##6: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##7: ncases n2; nnormalize;
               ##[ ##7: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##8: ncases n2; nnormalize;
               ##[ ##8: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##9: ncases n2; nnormalize;
               ##[ ##9: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##10: ncases n2; nnormalize;
               ##[ ##10: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##11: ncases n2; nnormalize;
               ##[ ##11: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##12: ncases n2; nnormalize;
               ##[ ##12: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##13: ncases n2; nnormalize;
               ##[ ##13: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##14: ncases n2; nnormalize;
               ##[ ##14: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##15: ncases n2; nnormalize;
               ##[ ##15: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##16: ncases n2; nnormalize;
               ##[ ##16: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##17: ncases n2; nnormalize;
               ##[ ##17: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##18: ncases n2; nnormalize;
               ##[ ##18: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##19: ncases n2; nnormalize;
               ##[ ##19: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##20: ncases n2; nnormalize;
               ##[ ##20: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##21: ncases n2; nnormalize;
               ##[ ##21: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##22: ncases n2; nnormalize;
               ##[ ##22: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##23: ncases n2; nnormalize;
               ##[ ##23: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##24: ncases n2; nnormalize;
               ##[ ##24: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##25: ncases n2; nnormalize;
               ##[ ##25: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##26: ncases n2; nnormalize;
               ##[ ##26: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##27: ncases n2; nnormalize;
               ##[ ##27: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##28: ncases n2; nnormalize;
               ##[ ##28: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##29: ncases n2; nnormalize;
               ##[ ##29: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##30: ncases n2; nnormalize;
               ##[ ##30: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##31: ncases n2; nnormalize;
               ##[ ##31: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##| ##32: ncases n2; nnormalize;
               ##[ ##32: #H; napply (λx:P.x)
-              ##| ##*: #H; napply (bitrigesim_destruct ??? (instr_mode_destruct_MODE_SRT ?? H))
+              ##| ##*: #H; napply (bitrigesim_destruct … (instr_mode_destruct_MODE_SRT … H))
               ##]
      ##]
  ##]