helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/word32.ma".
  24 include "num/word16_lemmas.ma".
  25
  26 (* ***** *)
  27 (* DWORD *)
  28 (* ***** *)
  29
  30 nlemma word32_destruct_1 :
  31 ∀x1,x2,y1,y2.
  32  mk_word32 x1 y1 = mk_word32 x2 y2 → x1 = x2.
  33  #x1; #x2; #y1; #y2; #H;
  34  nchange with (match mk_word32 x2 y2 with [ mk_word32 a _ ⇒ x1 = a ]);
  35  nrewrite < H;
  36  nnormalize;
  37  napply refl_eq.
  38 nqed.
  39
  40 nlemma word32_destruct_2 :
  41 ∀x1,x2,y1,y2.
  42  mk_word32 x1 y1 = mk_word32 x2 y2 → y1 = y2.
  43  #x1; #x2; #y1; #y2; #H;
  44  nchange with (match mk_word32 x2 y2 with [ mk_word32 _ b ⇒ y1 = b ]);
  45  nrewrite < H;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma symmetric_eqw32 : symmetricT word32 bool eq_w32.
  51  #dw1; #dw2;
  52  nelim dw1;
  53  nelim dw2;
  54  #w1; #w2; #w3; #w4;
  55  nchange with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = ((eq_w16 w1 w3)⊗(eq_w16 w2 w4)));
  56  nrewrite > (symmetric_eqw16 w1 w3);
  57  nrewrite > (symmetric_eqw16 w2 w4);
  58  napply refl_eq.
  59 nqed.
  60
  61 nlemma symmetric_andw32 : symmetricT word32 word32 and_w32.
  62  #dw1; #dw2;
  63  nelim dw1;
  64  nelim dw2;
  65  #w1; #w2; #w3; #w4;
  66  nchange with ((mk_word32 (and_w16 w3 w1) (and_w16 w4 w2)) = (mk_word32 (and_w16 w1 w3) (and_w16 w2 w4)));
  67  nrewrite > (symmetric_andw16 w1 w3);
  68  nrewrite > (symmetric_andw16 w2 w4);
  69  napply refl_eq.
  70 nqed.
  71
  72 nlemma associative_andw32 : ∀dw1,dw2,dw3.(and_w32 (and_w32 dw1 dw2) dw3) = (and_w32 dw1 (and_w32 dw2 dw3)).
  73  #dw1; #dw2; #dw3;
  74  nelim dw1;
  75  #w1; #w2;
  76  nelim dw2;
  77  #w3; #w4;
  78  nelim dw3;
  79  #w5; #w6;
  80  nchange with (mk_word32 (and_w16 (and_w16 w1 w3) w5) (and_w16 (and_w16 w2 w4) w6) =
  81   mk_word32 (and_w16 w1 (and_w16 w3 w5)) (and_w16 w2 (and_w16 w4 w6)));
  82  nrewrite < (associative_andw16 w1 w3 w5);
  83  nrewrite < (associative_andw16 w2 w4 w6);
  84  napply refl_eq.
  85 nqed.
  86
  87 nlemma symmetric_orw32 : symmetricT word32 word32 or_w32.
  88  #dw1; #dw2;
  89  nelim dw1;
  90  nelim dw2;
  91  #w1; #w2; #w3; #w4;
  92  nchange with ((mk_word32 (or_w16 w3 w1) (or_w16 w4 w2)) = (mk_word32 (or_w16 w1 w3) (or_w16 w2 w4)));
  93  nrewrite > (symmetric_orw16 w1 w3);
  94  nrewrite > (symmetric_orw16 w2 w4);
  95  napply refl_eq.
  96 nqed.
  97
  98 nlemma associative_orw32 : ∀dw1,dw2,dw3.(or_w32 (or_w32 dw1 dw2) dw3) = (or_w32 dw1 (or_w32 dw2 dw3)).
  99  #dw1; #dw2; #dw3;
 100  nelim dw1;
 101  #w1; #w2;
 102  nelim dw2;
 103  #w3; #w4;
 104  nelim dw3;
 105  #w5; #w6;
 106  nchange with (mk_word32 (or_w16 (or_w16 w1 w3) w5) (or_w16 (or_w16 w2 w4) w6) =
 107   mk_word32 (or_w16 w1 (or_w16 w3 w5)) (or_w16 w2 (or_w16 w4 w6)));
 108  nrewrite < (associative_orw16 w1 w3 w5);
 109  nrewrite < (associative_orw16 w2 w4 w6);
 110  napply refl_eq.
 111 nqed.
 112
 113 nlemma symmetric_xorw32 : symmetricT word32 word32 xor_w32.
 114  #dw1; #dw2;
 115  nelim dw1;
 116  nelim dw2;
 117  #w1; #w2; #w3; #w4;
 118  nchange with ((mk_word32 (xor_w16 w3 w1) (xor_w16 w4 w2)) = (mk_word32 (xor_w16 w1 w3) (xor_w16 w2 w4)));
 119  nrewrite > (symmetric_xorw16 w1 w3);
 120  nrewrite > (symmetric_xorw16 w2 w4);
 121  napply refl_eq.
 122 nqed.
 123
 124 nlemma associative_xorw32 : ∀dw1,dw2,dw3.(xor_w32 (xor_w32 dw1 dw2) dw3) = (xor_w32 dw1 (xor_w32 dw2 dw3)).
 125  #dw1; #dw2; #dw3;
 126  nelim dw1;
 127  #w1; #w2;
 128  nelim dw2;
 129  #w3; #w4;
 130  nelim dw3;
 131  #w5; #w6;
 132  nchange with (mk_word32 (xor_w16 (xor_w16 w1 w3) w5) (xor_w16 (xor_w16 w2 w4) w6) =
 133   mk_word32 (xor_w16 w1 (xor_w16 w3 w5)) (xor_w16 w2 (xor_w16 w4 w6)));
 134  nrewrite < (associative_xorw16 w1 w3 w5);
 135  nrewrite < (associative_xorw16 w2 w4 w6);
 136  napply refl_eq.
 137 nqed.
 138
 139 nlemma symmetric_plusw32_dc_dc : ∀dw1,dw2,c.plus_w32_dc_dc dw1 dw2 c = plus_w32_dc_dc dw2 dw1 c.
 140  #dw1; #dw2; #c;
 141  nelim dw1;
 142  #w1; #w2;
 143  nelim dw2;
 144  #w3; #w4;
 145  nchange with (
 146   match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
 147   match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
 148  nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
 149  ncases (plus_w16_dc_dc w2 w4 c);
 150  #w5; #c1;
 151  nchange with (
 152   match plus_w16_dc_dc w1 w3 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
 153   match plus_w16_dc_dc w3 w1 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
 154  nrewrite > (symmetric_plusw16_dc_dc w1 w3 c1);
 155  napply refl_eq.
 156 nqed.
 157
 158 nlemma symmetric_plusw32_dc_d : ∀dw1,dw2,c.plus_w32_dc_d dw1 dw2 c = plus_w32_dc_d dw2 dw1 c.
 159  #dw1; #dw2; #c;
 160  nelim dw1;
 161  #w1; #w2;
 162  nelim dw2;
 163  #w3; #w4;
 164  nchange with (
 165   match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
 166   match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
 167  nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
 168  ncases (plus_w16_dc_dc w2 w4 c);
 169  #w5; #c1;
 170  nchange with (〈plus_w16_dc_d w1 w3 c1.w5〉 = 〈plus_w16_dc_d w3 w1 c1.w5〉);
 171  nrewrite > (symmetric_plusw16_dc_d w1 w3 c1);
 172  napply refl_eq.
 173 nqed.
 174
 175 nlemma symmetric_plusw32_dc_c : ∀dw1,dw2,c.plus_w32_dc_c dw1 dw2 c = plus_w32_dc_c dw2 dw1 c.
 176  #dw1; #dw2; #c;
 177  nelim dw1;
 178  #w1; #w2;
 179  nelim dw2;
 180  #w3; #w4;
 181  nchange with (
 182   plus_w16_dc_c w1 w3 (plus_w16_dc_c w2 w4 c) =
 183   plus_w16_dc_c w3 w1 (plus_w16_dc_c w4 w2 c));
 184  nrewrite > (symmetric_plusw16_dc_c w4 w2 c);
 185  nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_dc_c w2 w4 c));
 186  napply refl_eq.
 187 nqed.
 188
 189 nlemma symmetric_plusw32_d_dc : ∀dw1,dw2.plus_w32_d_dc dw1 dw2 = plus_w32_d_dc dw2 dw1.
 190  #dw1; #dw2;
 191  nelim dw1;
 192  #w1; #w2;
 193  nelim dw2;
 194  #w3; #w4;
 195  nchange with (
 196   match plus_w16_d_dc w2 w4 with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
 197   match plus_w16_d_dc w4 w2 with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
 198  nrewrite > (symmetric_plusw16_d_dc w4 w2);
 199  ncases (plus_w16_d_dc w2 w4);
 200  #w5; #c;
 201  nchange with (
 202   match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
 203   match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
 204  nrewrite > (symmetric_plusw16_dc_dc w1 w3 c);
 205  napply refl_eq.
 206 nqed.
 207
 208 nlemma symmetric_plusw32_d_d : ∀dw1,dw2.plus_w32_d_d dw1 dw2 = plus_w32_d_d dw2 dw1.
 209  #dw1; #dw2;
 210  nelim dw1;
 211  #w1; #w2;
 212  nelim dw2;
 213  #w3; #w4;
 214  nchange with (
 215   match plus_w16_d_dc w2 w4 with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
 216   match plus_w16_d_dc w4 w2 with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
 217  nrewrite > (symmetric_plusw16_d_dc w4 w2);
 218  ncases (plus_w16_d_dc w2 w4);
 219  #w5; #c;
 220  nchange with (〈plus_w16_dc_d w1 w3 c.w5〉 = 〈plus_w16_dc_d w3 w1 c.w5〉);
 221  nrewrite > (symmetric_plusw16_dc_d w1 w3 c);
 222  napply refl_eq.
 223 nqed.
 224
 225 nlemma symmetric_plusw32_d_c : ∀dw1,dw2.plus_w32_d_c dw1 dw2 = plus_w32_d_c dw2 dw1.
 226  #dw1; #dw2;
 227  nelim dw1;
 228  #w1; #w2;
 229  nelim dw2;
 230  #w3; #w4;
 231  nchange with (
 232   plus_w16_dc_c w1 w3 (plus_w16_d_c w2 w4) =
 233   plus_w16_dc_c w3 w1 (plus_w16_d_c w4 w2));
 234  nrewrite > (symmetric_plusw16_d_c w4 w2);
 235  nrewrite > (symmetric_plusw16_dc_c w3 w1 (plus_w16_d_c w2 w4));
 236  napply refl_eq.
 237 nqed.
 238
 239 nlemma symmetric_mulw16 : symmetricT word16 word32 mul_w16.
 240  #w1; #w2;
 241  nelim w1;
 242  #b1; #b2;
 243  nelim w2;
 244  #b3; #b4;
 245  nchange with (match mul_b8 b2 b4 with
 246  [ mk_word16 t1_h t1_l ⇒ match mul_b8 b1 b4 with
 247  [ mk_word16 t2_h t2_l ⇒ match mul_b8 b3 b2 with
 248  [ mk_word16 t3_h t3_l ⇒ match mul_b8 b1 b3 with
 249  [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
 250  ]]]] = match mul_b8 b4 b2 with
 251  [ mk_word16 t1_h t1_l ⇒ match mul_b8 b3 b2 with
 252  [ mk_word16 t2_h t2_l ⇒ match mul_b8 b1 b4 with
 253  [ mk_word16 t3_h t3_l ⇒ match mul_b8 b3 b1 with
 254  [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈t1_h:t1_l〉〉
 255  ]]]]);
 256  nrewrite < (symmetric_mulb8 b2 b4);
 257  ncases (mul_b8 b2 b4);
 258  #b5; #b6;
 259  nchange with (match mul_b8 b1 b4 with
 260  [ mk_word16 t2_h t2_l ⇒ match mul_b8 b3 b2 with
 261  [ mk_word16 t3_h t3_l ⇒ match mul_b8 b1 b3 with
 262  [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
 263  ]]] = match mul_b8 b3 b2 with
 264  [ mk_word16 t2_h t2_l ⇒ match mul_b8 b1 b4 with
 265  [ mk_word16 t3_h t3_l ⇒ match mul_b8 b3 b1 with
 266  [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:t3_h〉.〈t3_l:〈x0,x0〉〉〉 〈〈〈x0,x0〉:t2_h〉.〈t2_l:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
 267  ]]]);
 268  ncases (mul_b8 b3 b2);
 269  #b7; #b8;
 270  ncases (mul_b8 b1 b4);
 271  #b9; #b10;
 272  nchange with (match mul_b8 b1 b3 with
 273  [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
 274  ] = match mul_b8 b3 b1 with
 275  [ mk_word16 t4_h t4_l ⇒ plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉) 〈〈t4_h:t4_l〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉
 276  ]);
 277  nrewrite < (symmetric_mulb8 b1 b3);
 278  ncases (mul_b8 b1 b3);
 279  #b11; #b12;
 280  nchange with ((plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉) =
 281   (plus_w32_d_d (plus_w32_d_d (plus_w32_d_d 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉) 〈〈b11:b12〉.〈〈x0,x0〉:〈x0,x0〉〉〉)〈〈〈x0,x0〉:〈x0,x0〉〉.〈b5:b6〉〉));
 282  nrewrite > (symmetric_plusw32_d_d 〈〈〈x0,x0〉:b7〉.〈b8:〈x0,x0〉〉〉 〈〈〈x0,x0〉:b9〉.〈b10:〈x0,x0〉〉〉);
 283  napply refl_eq.
 284 nqed.
 285
 286 nlemma eqw32_to_eq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = true) → (dw1 = dw2).
 287  #dw1; #dw2;
 288  nelim dw1;
 289  nelim dw2;
 290  #w1; #w2; #w3; #w4;
 291  nchange in ⊢ (% → ?) with (((eq_w16 w3 w1)⊗(eq_w16 w4 w2)) = true);
 292  #H;
 293  nrewrite < (eqw16_to_eq … (andb_true_true_l … H));
 294  nrewrite < (eqw16_to_eq … (andb_true_true_r … H));
 295  napply refl_eq.
 296 nqed.
 297
 298 nlemma eq_to_eqw32 : ∀dw1,dw2.dw1 = dw2 → eq_w32 dw1 dw2 = true.
 299  #dw1; #dw2;
 300  nelim dw1;
 301  nelim dw2;
 302  #w1; #w2; #w3; #w4;
 303  #H;
 304  nrewrite < (word32_destruct_1 … H);
 305  nrewrite < (word32_destruct_2 … H);
 306  nchange with (((eq_w16 w3 w3)⊗(eq_w16 w4 w4)) = true);
 307  nrewrite > (eq_to_eqw16 w3 w3 (refl_eq …));
 308  nrewrite > (eq_to_eqw16 w4 w4 (refl_eq …));
 309  nnormalize;
 310  napply refl_eq.
 311 nqed.
 312
 313 nlemma decidable_w32_aux1 : ∀w1,w2,w3,w4.w1 ≠ w3 → 〈w1.w2〉 ≠ 〈w3.w4〉.
 314  #w1; #w2; #w3; #w4;
 315  nnormalize; #H; #H1;
 316  napply (H (word32_destruct_1 … H1)).
 317 nqed.
 318
 319 nlemma decidable_w32_aux2 : ∀w1,w2,w3,w4.w2 ≠ w4 → 〈w1.w2〉 ≠ 〈w3.w4〉.
 320  #w1; #w2; #w3; #w4;
 321  nnormalize; #H; #H1;
 322  napply (H (word32_destruct_2 … H1)).
 323 nqed.
 324
 325 nlemma decidable_w32 : ∀x,y:word32.decidable (x = y).
 326  #x; nelim x; #w1; #w2;
 327  #y; nelim y; #w3; #w4;
 328  nnormalize;
 329  napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
 330  ##[ ##2: #H; napply (or2_intro2 … (decidable_w32_aux1 w1 w2 w3 w4 H))
 331  ##| ##1: #H; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
 332           ##[ ##2: #H1; napply (or2_intro2 … (decidable_w32_aux2 w1 w2 w3 w4 H1))
 333           ##| ##1: #H1; nrewrite > H; nrewrite > H1;
 334                         napply (or2_intro1 … (refl_eq ? 〈w3.w4〉))
 335           ##]
 336  ##]
 337 nqed.
 338
 339 nlemma neqw32_to_neq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = false) → (dw1 ≠ dw2).
 340  #dw1; #dw2;
 341  nelim dw1;
 342  nelim dw2;
 343  #w1; #w2; #w3; #w4;
 344  nchange with ((((eq_w16 w3 w1) ⊗ (eq_w16 w4 w2)) = false) → ?);
 345  #H;
 346  napply (or2_elim ((eq_w16 w3 w1) = false) ((eq_w16 w4 w2) = false) ? (andb_false2 … H) …);
 347  ##[ ##1: #H1; napply (decidable_w32_aux1 … (neqw16_to_neq … H1))
 348  ##| ##2: #H1; napply (decidable_w32_aux2 … (neqw16_to_neq … H1))
 349  ##]
 350 nqed.
 351
 352 nlemma word32_destruct : ∀w1,w2,w3,w4.〈w1.w2〉 ≠ 〈w3.w4〉 → w1 ≠ w3 ∨ w2 ≠ w4.
 353  #w1; #w2; #w3; #w4;
 354  nnormalize; #H;
 355  napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
 356  ##[ ##2: #H1; napply (or2_intro1 … H1)
 357  ##| ##1: #H1; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
 358           ##[ ##2: #H2; napply (or2_intro2 … H2)
 359           ##| ##1: #H2; nrewrite > H1 in H:(%);
 360                    nrewrite > H2;
 361                    #H; nelim (H (refl_eq …))
 362           ##]
 363  ##]
 364 nqed.
 365
 366 nlemma neq_to_neqw32 : ∀dw1,dw2.dw1 ≠ dw2 → eq_w32 dw1 dw2 = false.
 367  #dw1; #dw2;
 368  nelim dw1; #w1; #w2;
 369  nelim dw2; #w3; #w4;
 370  #H; nchange with (((eq_w16 w1 w3) ⊗ (eq_w16 w2 w4)) = false);
 371  napply (or2_elim (w1 ≠ w3) (w2 ≠ w4) ? (word32_destruct … H) …);
 372  ##[ ##1: #H1; nrewrite > (neq_to_neqw16 … H1); nnormalize; napply refl_eq
 373  ##| ##2: #H1; nrewrite > (neq_to_neqw16 … H1);
 374           nrewrite > (symmetric_andbool (eq_w16 w1 w3) false);
 375           nnormalize; napply refl_eq
 376  ##]
 377 nqed.