X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fword16_lemmas.ma;h=56a54ae999455fc1e429df0d168d354aaf1e704e;hb=f9b16ad62794042c2b31c6e3433b3c4035f8a0d5;hp=06030fffb9ed0c5dae9f29052265261602722315;hpb=29cfb9e2961e62c836cb50217905c0594a074e81;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
index 06030fffb..56a54ae99 100755
--- a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
@@ -143,20 +143,14 @@ nlemma symmetric_plusw16_dc_dc : ∀w1,w2,c.plus_w16_dc_dc w1 w2 c = plus_w16_dc
  nelim w2;
  #b3; #b4;
  nchange with (
-  match plus_b8_dc_dc b2 b4 c with
-   [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
-    [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
-  match plus_b8_dc_dc b4 b2 c with
-   [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
-    [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+  match plus_b8_dc_dc b2 b4 c with [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+  match plus_b8_dc_dc b4 b2 c with [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
  nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
  ncases (plus_b8_dc_dc b2 b4 c);
  #b5; #c1;
  nchange with (
-  match plus_b8_dc_dc b1 b3 c1 with
-   [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
-  match plus_b8_dc_dc b3 b1 c1 with
-   [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+  match plus_b8_dc_dc b1 b3 c1 with [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+  match plus_b8_dc_dc b3 b1 c1 with [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
  nrewrite > (symmetric_plusb8_dc_dc b1 b3 c1);
  napply refl_eq.
 nqed.
@@ -168,10 +162,8 @@ nlemma symmetric_plusw16_dc_d : ∀w1,w2,c.plus_w16_dc_d w1 w2 c = plus_w16_dc_d
  nelim w2;
  #b3; #b4;
  nchange with (
-  match plus_b8_dc_dc b2 b4 c with
-   [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
-  match plus_b8_dc_dc b4 b2 c with
-   [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+  match plus_b8_dc_dc b2 b4 c with [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+  match plus_b8_dc_dc b4 b2 c with [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
  nrewrite > (symmetric_plusb8_dc_dc b4 b2 c);
  ncases (plus_b8_dc_dc b2 b4 c);
  #b5; #c1;
@@ -201,20 +193,14 @@ nlemma symmetric_plusw16_d_dc : ∀w1,w2.plus_w16_d_dc w1 w2 = plus_w16_d_dc w2
  nelim w2;
  #b3; #b4;
  nchange with (
-  match plus_b8_d_dc b2 b4 with
-   [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with
-    [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
-  match plus_b8_d_dc b4 b2 with
-   [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with
-    [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
+  match plus_b8_d_dc b2 b4 with [ pair l c ⇒ match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]] =
+  match plus_b8_d_dc b4 b2 with [ pair l c ⇒ match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:l〉 c' ]]);
  nrewrite > (symmetric_plusb8_d_dc b4 b2);
  ncases (plus_b8_d_dc b2 b4);
  #b5; #c;
  nchange with (
-  match plus_b8_dc_dc b1 b3 c with
-   [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
-  match plus_b8_dc_dc b3 b1 c with
-   [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
+  match plus_b8_dc_dc b1 b3 c with [ pair h c' ⇒ pair … 〈h:b5〉 c' ] =
+  match plus_b8_dc_dc b3 b1 c with [ pair h c' ⇒ pair … 〈h:b5〉 c' ]);
  nrewrite > (symmetric_plusb8_dc_dc b1 b3 c);
  napply refl_eq.
 nqed.
@@ -226,10 +212,8 @@ nlemma symmetric_plusw16_d_d : ∀w1,w2.plus_w16_d_d w1 w2 = plus_w16_d_d w2 w1.
  nelim w2;
  #b3; #b4;
  nchange with (
-  match plus_b8_d_dc b2 b4 with
-   [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
-  match plus_b8_d_dc b4 b2 with
-   [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
+  match plus_b8_d_dc b2 b4 with [ pair l c ⇒ 〈plus_b8_dc_d b1 b3 c:l〉 ] =
+  match plus_b8_d_dc b4 b2 with [ pair l c ⇒ 〈plus_b8_dc_d b3 b1 c:l〉 ]);
  nrewrite > (symmetric_plusb8_d_dc b4 b2);
  ncases (plus_b8_d_dc b2 b4);
  #b5; #c;
@@ -359,7 +343,7 @@ nlemma neqw16_to_neq : ∀w1,w2:word16.(eq_w16 w1 w2 = false) → (w1 ≠ w2).
  #b1; #b2; #b3; #b4;
  nchange with ((((eq_b8 b3 b1) ⊗ (eq_b8 b4 b2)) = false) → ?);
  #H;
- napply (or2_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false … H) …);
+ napply (or2_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false2 … H) …);
  ##[ ##1: #H1; napply (decidable_w16_aux1 … (neqb8_to_neq … H1))
  ##| ##2: #H1; napply (decidable_w16_aux2 … (neqb8_to_neq … H1))
  ##]