1) \ldots here and there

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/byte8_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/byte8_lemmas.ma
index 33c08f99df2e5c3f5a31ff2a516bbe45325c9f92..f0ca96016b03f7b98c3f4c0023a17b39124221b1 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/byte8_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/byte8_lemmas.ma
@@ -34,7 +34,7 @@ nlemma byte8_destruct_1 :
  nchange with (match mk_byte8 x2 y2 with [ mk_byte8 a _ ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma byte8_destruct_2 :
@@ -44,7 +44,7 @@ nlemma byte8_destruct_2 :
  nchange with (match mk_byte8 x2 y2 with [ mk_byte8 _ b ⇒ y1 = b ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_eqb8 : symmetricT byte8 bool eq_b8.
@@ -55,7 +55,7 @@ nlemma symmetric_eqb8 : symmetricT byte8 bool eq_b8.
  nchange with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = ((eq_ex e1 e3)⊗(eq_ex e2 e4)));
  nrewrite > (symmetric_eqex e1 e3);
  nrewrite > (symmetric_eqex e2 e4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed. 
 
 nlemma symmetric_andb8 : symmetricT byte8 byte8 and_b8.
@@ -66,7 +66,7 @@ nlemma symmetric_andb8 : symmetricT byte8 byte8 and_b8.
  nchange with ((mk_byte8 (and_ex e3 e1) (and_ex e4 e2)) = (mk_byte8 (and_ex e1 e3) (and_ex e2 e4)));
  nrewrite > (symmetric_andex e1 e3);
  nrewrite > (symmetric_andex e2 e4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_andb8 : ∀b1,b2,b3.(and_b8 (and_b8 b1 b2) b3) = (and_b8 b1 (and_b8 b2 b3)).
@@ -81,7 +81,7 @@ nlemma associative_andb8 : ∀b1,b2,b3.(and_b8 (and_b8 b1 b2) b3) = (and_b8 b1 (
   mk_byte8 (and_ex e1 (and_ex e3 e5)) (and_ex e2 (and_ex e4 e6)));
  nrewrite < (associative_andex e1 e3 e5);
  nrewrite < (associative_andex e2 e4 e6);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_orb8 : symmetricT byte8 byte8 or_b8.
@@ -92,7 +92,7 @@ nlemma symmetric_orb8 : symmetricT byte8 byte8 or_b8.
  nchange with ((mk_byte8 (or_ex e3 e1) (or_ex e4 e2)) = (mk_byte8 (or_ex e1 e3) (or_ex e2 e4)));
  nrewrite > (symmetric_orex e1 e3);
  nrewrite > (symmetric_orex e2 e4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_orb8 : ∀b1,b2,b3.(or_b8 (or_b8 b1 b2) b3) = (or_b8 b1 (or_b8 b2 b3)).
@@ -107,7 +107,7 @@ nlemma associative_orb8 : ∀b1,b2,b3.(or_b8 (or_b8 b1 b2) b3) = (or_b8 b1 (or_b
   mk_byte8 (or_ex e1 (or_ex e3 e5)) (or_ex e2 (or_ex e4 e6)));
  nrewrite < (associative_orex e1 e3 e5);
  nrewrite < (associative_orex e2 e4 e6);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_xorb8 : symmetricT byte8 byte8 xor_b8.
@@ -118,7 +118,7 @@ nlemma symmetric_xorb8 : symmetricT byte8 byte8 xor_b8.
  nchange with ((mk_byte8 (xor_ex e3 e1) (xor_ex e4 e2)) = (mk_byte8 (xor_ex e1 e3) (xor_ex e2 e4)));
  nrewrite > (symmetric_xorex e1 e3);
  nrewrite > (symmetric_xorex e2 e4);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma associative_xorb8 : ∀b1,b2,b3.(xor_b8 (xor_b8 b1 b2) b3) = (xor_b8 b1 (xor_b8 b2 b3)).
@@ -133,7 +133,7 @@ nlemma associative_xorb8 : ∀b1,b2,b3.(xor_b8 (xor_b8 b1 b2) b3) = (xor_b8 b1 (
   mk_byte8 (xor_ex e1 (xor_ex e3 e5)) (xor_ex e2 (xor_ex e4 e6)));
  nrewrite < (associative_xorex e1 e3 e5);
  nrewrite < (associative_xorex e2 e4 e6);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusb8_dc_dc : ∀b1,b2,c.plus_b8_dc_dc b1 b2 c = plus_b8_dc_dc b2 b1 c.
@@ -145,20 +145,20 @@ nlemma symmetric_plusb8_dc_dc : ∀b1,b2,c.plus_b8_dc_dc b1 b2 c = plus_b8_dc_dc
  nchange with (
   match plus_ex_dc_dc e2 e4 c with
    [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
-    [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]] =
+    [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
   match plus_ex_dc_dc e4 e2 c with
    [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
-    [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]]);
+    [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
  nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
  ncases (plus_ex_dc_dc e2 e4 c);
  #e5; #c1;
  nchange with (
   match plus_ex_dc_dc e1 e3 c1 with
-   [ pair h c' ⇒ pair ?? 〈h,e5〉 c' ] =
+   [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
   match plus_ex_dc_dc e3 e1 c1 with
-   [ pair h c' ⇒ pair ?? 〈h,e5〉 c' ]);
+   [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
  nrewrite > (symmetric_plusex_dc_dc e1 e3 c1);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusb8_dc_d : ∀b1,b2,c.plus_b8_dc_d b1 b2 c = plus_b8_dc_d b2 b1 c.
@@ -177,7 +177,7 @@ nlemma symmetric_plusb8_dc_d : ∀b1,b2,c.plus_b8_dc_d b1 b2 c = plus_b8_dc_d b2
  #e5; #c1;
  nchange with (〈plus_ex_dc_d e1 e3 c1,e5〉 = 〈plus_ex_dc_d e3 e1 c1,e5〉);
  nrewrite > (symmetric_plusex_dc_d e1 e3 c1);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusb8_dc_c : ∀b1,b2,c.plus_b8_dc_c b1 b2 c = plus_b8_dc_c b2 b1 c.
@@ -191,7 +191,7 @@ nlemma symmetric_plusb8_dc_c : ∀b1,b2,c.plus_b8_dc_c b1 b2 c = plus_b8_dc_c b2
   plus_ex_dc_c e3 e1 (plus_ex_dc_c e4 e2 c));
  nrewrite > (symmetric_plusex_dc_c e4 e2 c);
  nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_dc_c e2 e4 c));
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusb8_d_dc : ∀b1,b2.plus_b8_d_dc b1 b2 = plus_b8_d_dc b2 b1.
@@ -203,20 +203,20 @@ nlemma symmetric_plusb8_d_dc : ∀b1,b2.plus_b8_d_dc b1 b2 = plus_b8_d_dc b2 b1.
  nchange with (
   match plus_ex_d_dc e2 e4 with
    [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
-    [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]] =
+    [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
   match plus_ex_d_dc e4 e2 with
    [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
-    [ pair h c' ⇒ pair ?? 〈h,l〉 c' ]]);
+    [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
  nrewrite > (symmetric_plusex_d_dc e4 e2);
  ncases (plus_ex_d_dc e2 e4);
  #e5; #c;
  nchange with (
   match plus_ex_dc_dc e1 e3 c with
-   [ pair h c' ⇒ pair ?? 〈h,e5〉 c' ] =
+   [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
   match plus_ex_dc_dc e3 e1 c with
-   [ pair h c' ⇒ pair ?? 〈h,e5〉 c' ]);
+   [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
  nrewrite > (symmetric_plusex_dc_dc e1 e3 c);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusb8_d_d : ∀b1,b2.plus_b8_d_d b1 b2 = plus_b8_d_d b2 b1.
@@ -235,7 +235,7 @@ nlemma symmetric_plusb8_d_d : ∀b1,b2.plus_b8_d_d b1 b2 = plus_b8_d_d b2 b1.
  #e5; #c;
  nchange with (〈plus_ex_dc_d e1 e3 c,e5〉 = 〈plus_ex_dc_d e3 e1 c,e5〉);
  nrewrite > (symmetric_plusex_dc_d e1 e3 c);
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_plusb8_d_c : ∀b1,b2.plus_b8_d_c b1 b2 = plus_b8_d_c b2 b1.
@@ -249,7 +249,7 @@ nlemma symmetric_plusb8_d_c : ∀b1,b2.plus_b8_d_c b1 b2 = plus_b8_d_c b2 b1.
   plus_ex_dc_c e3 e1 (plus_ex_d_c e4 e2));
  nrewrite > (symmetric_plusex_d_c e4 e2);
  nrewrite > (symmetric_plusex_dc_c e3 e1 (plus_ex_d_c e2 e4));
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma symmetric_mulex : symmetricT exadecim byte8 mul_ex.
@@ -257,7 +257,7 @@ nlemma symmetric_mulex : symmetricT exadecim byte8 mul_ex.
  nelim e1;
  nelim e2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqb8_to_eq : ∀b1,b2:byte8.(eq_b8 b1 b2 = true) → (b1 = b2).
@@ -267,9 +267,9 @@ nlemma eqb8_to_eq : ∀b1,b2:byte8.(eq_b8 b1 b2 = true) → (b1 = b2).
  #e1; #e2; #e3; #e4;
  nchange in ⊢ (% → ?) with (((eq_ex e3 e1)⊗(eq_ex e4 e2)) = true);
  #H;
- nrewrite < (eqex_to_eq ?? (andb_true_true_l ?? H));
- nrewrite < (eqex_to_eq ?? (andb_true_true_r ?? H));
- napply (refl_eq ??).
+ nrewrite < (eqex_to_eq … (andb_true_true_l … H));
+ nrewrite < (eqex_to_eq … (andb_true_true_r … H));
+ napply refl_eq.
 nqed. 
 
 nlemma eq_to_eqb8 : ∀b1,b2.b1 = b2 → eq_b8 b1 b2 = true.
@@ -278,11 +278,11 @@ nlemma eq_to_eqb8 : ∀b1,b2.b1 = b2 → eq_b8 b1 b2 = true.
  nelim b2;
  #e1; #e2; #e3; #e4;
  #H;
- nrewrite < (byte8_destruct_1 ???? H);
- nrewrite < (byte8_destruct_2 ???? H);
+ nrewrite < (byte8_destruct_1 … H);
+ nrewrite < (byte8_destruct_2 … H);
  nchange with (((eq_ex e3 e3)⊗(eq_ex e4 e4)) = true);
- nrewrite > (eq_to_eqex e3 e3 (refl_eq ??));
- nrewrite > (eq_to_eqex e4 e4 (refl_eq ??)); 
+ nrewrite > (eq_to_eqex e3 e3 (refl_eq …));
+ nrewrite > (eq_to_eqex e4 e4 (refl_eq …)); 
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.