helm/software/matita/contribs/ng_assembly/freescale/status_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/word16_lemmas.ma".
  24 include "freescale/opcode_base_lemmas1.ma".
  25 include "freescale/status.ma".
  26 include "common/option_lemmas.ma".
  27 include "common/prod_lemmas.ma".
  28
  29 (* *********************************** *)
  30 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  31 (* *********************************** *)
  32
  33 nlemma aluHC05_destruct_1 :
  34 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
  35  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
  36  x1 = y1.
  37  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  38  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  39  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  40                 with [ mk_alu_HC05 a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  41  nrewrite < H;
  42  nnormalize;
  43  napply refl_eq.
  44 nqed.
  45
  46 nlemma aluHC05_destruct_2 :
  47 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
  48  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
  49  x2 = y2.
  50  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  51  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  52  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  53                 with [ mk_alu_HC05 _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  54  nrewrite < H;
  55  nnormalize;
  56  napply refl_eq.
  57 nqed.
  58
  59 nlemma aluHC05_destruct_3 :
  60 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
  61  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
  62  x3 = y3.
  63  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  64  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  65  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  66                 with [ mk_alu_HC05 _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  67  nrewrite < H;
  68  nnormalize;
  69  napply refl_eq.
  70 nqed.
  71
  72 nlemma aluHC05_destruct_4 :
  73 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
  74  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
  75  x4 = y4.
  76  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  77  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  78  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  79                 with [ mk_alu_HC05 _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  80  nrewrite < H;
  81  nnormalize;
  82  napply refl_eq.
  83 nqed.
  84
  85 nlemma aluHC05_destruct_5 :
  86 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
  87  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
  88  x5 = y5.
  89  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  90  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  91  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  92                 with [ mk_alu_HC05 _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
  93  nrewrite < H;
  94  nnormalize;
  95  napply refl_eq.
  96 nqed.
  97
  98 nlemma aluHC05_destruct_6 :
  99 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 100  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
 101  x6 = y6.
 102  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 103  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 104  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 105                 with [ mk_alu_HC05 _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x6 = a ]);
 106  nrewrite < H;
 107  nnormalize;
 108  napply refl_eq.
 109 nqed.
 110
 111 nlemma aluHC05_destruct_7 :
 112 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 113  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
 114  x7 = y7.
 115  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 116  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 117  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 118                 with [ mk_alu_HC05 _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x7 = a ]);
 119  nrewrite < H;
 120  nnormalize;
 121  napply refl_eq.
 122 nqed.
 123
 124 nlemma aluHC05_destruct_8 :
 125 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 126  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
 127  x8 = y8.
 128  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 129  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 130  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 131                 with [ mk_alu_HC05 _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x8 = a ]);
 132  nrewrite < H;
 133  nnormalize;
 134  napply refl_eq.
 135 nqed.
 136
 137 nlemma aluHC05_destruct_9 :
 138 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 139  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
 140  x9 = y9.
 141  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 142  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 143  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 144                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x9 = a ]);
 145  nrewrite < H;
 146  nnormalize;
 147  napply refl_eq.
 148 nqed.
 149
 150 nlemma aluHC05_destruct_10 :
 151 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 152  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
 153  x10 = y10.
 154  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 155  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 156  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 157                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x10 = a ]);
 158  nrewrite < H;
 159  nnormalize;
 160  napply refl_eq.
 161 nqed.
 162
 163 nlemma aluHC05_destruct_11 :
 164 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 165  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
 166  x11 = y11.
 167  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 168  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 169  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 170                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x11 = a ]);
 171  nrewrite < H;
 172  nnormalize;
 173  napply refl_eq.
 174 nqed.
 175
 176 nlemma aluHC05_destruct_12 :
 177 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 178  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
 179  x12 = y12.
 180  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 181  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 182  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 183                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x12 = a ]);
 184  nrewrite < H;
 185  nnormalize;
 186  napply refl_eq.
 187 nqed.
 188
 189 nlemma aluHC05_destruct_13 :
 190 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 191  mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 = mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 →
 192  x13 = y13.
 193  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 194  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 195  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 196                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x13 = a ]);
 197  nrewrite < H;
 198  nnormalize;
 199  napply refl_eq.
 200 nqed.
 201
 202 nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_aluHC05.
 203  #alu1; #alu2;
 204  ncases alu1;
 205  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 206  ncases alu2;
 207  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 208  nchange with (
 209   ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 210   (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗  (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
 211   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗  (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
 212   (eq_bool x13 y13)) = ((eq_b8 y1 x1) ⊗  (eq_b8 y2 x2) ⊗ (eq_w16 y3 x3) ⊗
 213   (eq_w16 y4 x4) ⊗ (eq_w16 y5 x5) ⊗  (eq_w16 y6 x6) ⊗ (eq_w16 y7 x7) ⊗
 214   (eq_bool y8 x8) ⊗ (eq_bool y9 x9) ⊗  (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗
 215   (eq_bool y12 x12) ⊗ (eq_bool y13 x13)));
 216  nrewrite > (symmetric_eqb8 x1 y1);
 217  nrewrite > (symmetric_eqb8 x2 y2);
 218  nrewrite > (symmetric_eqw16 x3 y3);
 219  nrewrite > (symmetric_eqw16 x4 y4);
 220  nrewrite > (symmetric_eqw16 x5 y5);
 221  nrewrite > (symmetric_eqw16 x6 y6);
 222  nrewrite > (symmetric_eqw16 x7 y7);
 223  nrewrite > (symmetric_eqbool x8 y8);
 224  nrewrite > (symmetric_eqbool x9 y9);
 225  nrewrite > (symmetric_eqbool x10 y10);
 226  nrewrite > (symmetric_eqbool x11 y11);
 227  nrewrite > (symmetric_eqbool x12 y12);
 228  nrewrite > (symmetric_eqbool x13 y13);
 229  napply refl_eq.
 230 nqed.
 231
 232 nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_aluHC05 alu1 alu2 = true → alu1 = alu2.
 233  #alu1; #alu2;
 234  ncases alu1;
 235  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 236  ncases alu2;
 237  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 238  nchange in H:(%) with (
 239  ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗
 240   (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 241   (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗
 242   (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
 243   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗
 244   (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
 245   (eq_bool x13 y13)) = true);
 246  nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
 247  nletin H1 ≝ (andb_true_true_l … H);
 248  nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r … (andb_true_true_l … H)));
 249  nletin H2 ≝ (andb_true_true_l … H1);
 250  nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
 251  nletin H3 ≝ (andb_true_true_l … H2);
 252  nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
 253  nletin H4 ≝ (andb_true_true_l … H3);
 254  nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
 255  nletin H5 ≝ (andb_true_true_l … H4);
 256  nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
 257  nletin H6 ≝ (andb_true_true_l … H5);
 258  nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
 259  nletin H7 ≝ (andb_true_true_l … H6);
 260  nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
 261  nletin H8 ≝ (andb_true_true_l … H7);
 262  nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
 263  nletin H9 ≝ (andb_true_true_l … H8);
 264  nrewrite > (eqw16_to_eq … (andb_true_true_r … H9));
 265  nletin H10 ≝ (andb_true_true_l … H9);
 266  nrewrite > (eqw16_to_eq … (andb_true_true_r … H10));
 267  nletin H11 ≝ (andb_true_true_l … H10);
 268  nrewrite > (eqb8_to_eq … (andb_true_true_r … H11));
 269  nrewrite > (eqb8_to_eq … (andb_true_true_l … H11));
 270  napply refl_eq.
 271 nqed.
 272
 273 nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_aluHC05 alu1 alu2 = true.
 274  #alu1; #alu2;
 275  ncases alu1;
 276  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 277  ncases alu2;
 278  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 279  nrewrite > (aluHC05_destruct_1 … H);
 280  nrewrite > (aluHC05_destruct_2 … H);
 281  nrewrite > (aluHC05_destruct_3 … H);
 282  nrewrite > (aluHC05_destruct_4 … H);
 283  nrewrite > (aluHC05_destruct_5 … H);
 284  nrewrite > (aluHC05_destruct_6 … H);
 285  nrewrite > (aluHC05_destruct_7 … H);
 286  nrewrite > (aluHC05_destruct_8 … H);
 287  nrewrite > (aluHC05_destruct_9 … H);
 288  nrewrite > (aluHC05_destruct_10 … H);
 289  nrewrite > (aluHC05_destruct_11 … H);
 290  nrewrite > (aluHC05_destruct_12 … H);
 291  nrewrite > (aluHC05_destruct_13 … H);
 292  nchange with (
 293  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗
 294   (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 295   (eq_w16 y5 y5) ⊗ (eq_w16 y6 y6) ⊗
 296   (eq_w16 y7 y7) ⊗ (eq_bool y8 y8) ⊗
 297   (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗
 298   (eq_bool y11 y11) ⊗ (eq_bool y12 y12) ⊗
 299   (eq_bool y13 y13)) = true);
 300  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
 301  nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
 302  nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
 303  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
 304  nrewrite > (eq_to_eqw16 y5 y5 (refl_eq …));
 305  nrewrite > (eq_to_eqw16 y6 y6 (refl_eq …));
 306  nrewrite > (eq_to_eqw16 y7 y7 (refl_eq …));
 307  nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
 308  nrewrite > (eq_to_eqbool y9 y9 (refl_eq …));
 309  nrewrite > (eq_to_eqbool y10 y10 (refl_eq …));
 310  nrewrite > (eq_to_eqbool y11 y11 (refl_eq …));
 311  nrewrite > (eq_to_eqbool y12 y12 (refl_eq …));
 312  nrewrite > (eq_to_eqbool y13 y13 (refl_eq …));
 313  napply refl_eq.
 314 nqed.
 315
 316 nlemma decidable_aluHC05_aux1
 317  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 318  (x1 ≠ y1) →
 319  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 320  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 321  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 322  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 323  nnormalize; #H; #H1;
 324  napply (H (aluHC05_destruct_1 … H1)).
 325 nqed.
 326
 327 nlemma decidable_aluHC05_aux2
 328  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 329  (x2 ≠ y2) →
 330  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 331  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 332  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 333  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 334  nnormalize; #H; #H1;
 335  napply (H (aluHC05_destruct_2 … H1)).
 336 nqed.
 337
 338 nlemma decidable_aluHC05_aux3
 339  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 340  (x3 ≠ y3) →
 341  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 342  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 343  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 344  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 345  nnormalize; #H; #H1;
 346  napply (H (aluHC05_destruct_3 … H1)).
 347 nqed.
 348
 349 nlemma decidable_aluHC05_aux4
 350  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 351  (x4 ≠ y4) →
 352  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 353  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 354  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 355  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 356  nnormalize; #H; #H1;
 357  napply (H (aluHC05_destruct_4 … H1)).
 358 nqed.
 359
 360 nlemma decidable_aluHC05_aux5
 361  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 362  (x5 ≠ y5) →
 363  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 364  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 365  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 366  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 367  nnormalize; #H; #H1;
 368  napply (H (aluHC05_destruct_5 … H1)).
 369 nqed.
 370
 371 nlemma decidable_aluHC05_aux6
 372  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 373  (x6 ≠ y6) →
 374  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 375  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 376  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 377  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 378  nnormalize; #H; #H1;
 379  napply (H (aluHC05_destruct_6 … H1)).
 380 nqed.
 381
 382 nlemma decidable_aluHC05_aux7
 383  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 384  (x7 ≠ y7) →
 385  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 386  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 387  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 388  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 389  nnormalize; #H; #H1;
 390  napply (H (aluHC05_destruct_7 … H1)).
 391 nqed.
 392
 393 nlemma decidable_aluHC05_aux8
 394  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 395  (x8 ≠ y8) →
 396  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 397  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 398  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 399  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 400  nnormalize; #H; #H1;
 401  napply (H (aluHC05_destruct_8 … H1)).
 402 nqed.
 403
 404 nlemma decidable_aluHC05_aux9
 405  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 406  (x9 ≠ y9) →
 407  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 408  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 409  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 410  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 411  nnormalize; #H; #H1;
 412  napply (H (aluHC05_destruct_9 … H1)).
 413 nqed.
 414
 415 nlemma decidable_aluHC05_aux10
 416  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 417  (x10 ≠ y10) →
 418  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 419  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 420  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 421  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 422  nnormalize; #H; #H1;
 423  napply (H (aluHC05_destruct_10 … H1)).
 424 nqed.
 425
 426 nlemma decidable_aluHC05_aux11
 427  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 428  (x11 ≠ y11) →
 429  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 430  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 431  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 432  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 433  nnormalize; #H; #H1;
 434  napply (H (aluHC05_destruct_11 … H1)).
 435 nqed.
 436
 437 nlemma decidable_aluHC05_aux12
 438  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 439  (x12 ≠ y12) →
 440  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 441  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 442  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 443  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 444  nnormalize; #H; #H1;
 445  napply (H (aluHC05_destruct_12 … H1)).
 446 nqed.
 447
 448 nlemma decidable_aluHC05_aux13
 449  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13.
 450  (x13 ≠ y13) →
 451  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 452  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 453  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 454  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 455  nnormalize; #H; #H1;
 456  napply (H (aluHC05_destruct_13 … H1)).
 457 nqed.
 458
 459 nlemma decidable_aluHC05 : ∀x,y:alu_HC05.decidable (x = y).
 460  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 461  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 462  nnormalize;
 463  napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
 464  ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC05_aux1 … H))
 465  ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
 466   ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC05_aux2 … H1))
 467   ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
 468    ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC05_aux3 … H2))
 469    ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
 470     ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC05_aux4 … H3))
 471     ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …);
 472      ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC05_aux5 … H4))
 473      ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x6 y6) …);
 474       ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC05_aux6 … H5))
 475       ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x7 y7) …);
 476        ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC05_aux7 … H6))
 477        ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
 478         ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC05_aux8 … H7))
 479         ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …);
 480          ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC05_aux9 … H8))
 481          ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …);
 482           ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC05_aux10 … H9))
 483           ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …);
 484            ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC05_aux11 … H10))
 485            ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …);
 486             ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC05_aux12 … H11))
 487             ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x13 y13) …);
 488              ##[ ##2: #H12; napply (or2_intro2 … (decidable_aluHC05_aux13 … H12))
 489              ##| ##1: #H12; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
 490                       nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
 491                       nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
 492                       nrewrite > H12; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 493              ##]
 494             ##]
 495            ##]
 496           ##]
 497          ##]
 498         ##]
 499        ##]
 500       ##]
 501      ##]
 502     ##]
 503    ##]
 504   ##]
 505  ##]
 506 nqed.
 507
 508 nlemma aluHC08_destruct_1 :
 509 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 510  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 511  x1 = y1.
 512  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 513  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 514  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 515                 with [ mk_alu_HC08 a _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
 516  nrewrite < H;
 517  nnormalize;
 518  napply refl_eq.
 519 nqed.
 520
 521 nlemma aluHC08_destruct_2 :
 522 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 523  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 524  x2 = y2.
 525  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 526  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 527  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 528                 with [ mk_alu_HC08 _ a _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
 529  nrewrite < H;
 530  nnormalize;
 531  napply refl_eq.
 532 nqed.
 533
 534 nlemma aluHC08_destruct_3 :
 535 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 536  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 537  x3 = y3.
 538  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 539  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 540  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 541                 with [ mk_alu_HC08 _ _ a _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
 542  nrewrite < H;
 543  nnormalize;
 544  napply refl_eq.
 545 nqed.
 546
 547 nlemma aluHC08_destruct_4 :
 548 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 549  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 550  x4 = y4.
 551  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 552  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 553  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 554                 with [ mk_alu_HC08 _ _ _ a _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
 555  nrewrite < H;
 556  nnormalize;
 557  napply refl_eq.
 558 nqed.
 559
 560 nlemma aluHC08_destruct_5 :
 561 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 562  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 563  x5 = y5.
 564  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 565  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 566  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 567                 with [ mk_alu_HC08 _ _ _ _ a _ _ _ _ _ _ _ ⇒ x5 = a ]);
 568  nrewrite < H;
 569  nnormalize;
 570  napply refl_eq.
 571 nqed.
 572
 573 nlemma aluHC08_destruct_6 :
 574 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 575  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 576  x6 = y6.
 577  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 578  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 579  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 580                 with [ mk_alu_HC08 _ _ _ _ _ a _ _ _ _ _ _ ⇒ x6 = a ]);
 581  nrewrite < H;
 582  nnormalize;
 583  napply refl_eq.
 584 nqed.
 585
 586 nlemma aluHC08_destruct_7 :
 587 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 588  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 589  x7 = y7.
 590  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 591  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 592  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 593                 with [ mk_alu_HC08 _ _ _ _ _ _ a _ _ _ _ _ ⇒ x7 = a ]);
 594  nrewrite < H;
 595  nnormalize;
 596  napply refl_eq.
 597 nqed.
 598
 599 nlemma aluHC08_destruct_8 :
 600 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 601  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 602  x8 = y8.
 603  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 604  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 605  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 606                 with [ mk_alu_HC08 _ _ _ _ _ _ _ a _ _ _ _ ⇒ x8 = a ]);
 607  nrewrite < H;
 608  nnormalize;
 609  napply refl_eq.
 610 nqed.
 611
 612 nlemma aluHC08_destruct_9 :
 613 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 614  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 615  x9 = y9.
 616  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 617  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 618  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 619                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ a _ _ _ ⇒ x9 = a ]);
 620  nrewrite < H;
 621  nnormalize;
 622  napply refl_eq.
 623 nqed.
 624
 625 nlemma aluHC08_destruct_10 :
 626 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 627  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 628  x10 = y10.
 629  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 630  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 631  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 632                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ a _ _ ⇒ x10 = a ]);
 633  nrewrite < H;
 634  nnormalize;
 635  napply refl_eq.
 636 nqed.
 637
 638 nlemma aluHC08_destruct_11 :
 639 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 640  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 641  x11 = y11.
 642  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 643  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 644  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 645                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ a _ ⇒ x11 = a ]);
 646  nrewrite < H;
 647  nnormalize;
 648  napply refl_eq.
 649 nqed.
 650
 651 nlemma aluHC08_destruct_12 :
 652 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 653  mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 = mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 →
 654  x12 = y12.
 655  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 656  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 657  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 658                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ a ⇒ x12 = a ]);
 659  nrewrite < H;
 660  nnormalize;
 661  napply refl_eq.
 662 nqed.
 663
 664 nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_aluHC08.
 665  #alu1; #alu2;
 666  ncases alu1;
 667  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 668  ncases alu2;
 669  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 670  nchange with (
 671   ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 672    (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
 673    (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) =
 674    ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_b8 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
 675    (eq_w16 y5 x5) ⊗ (eq_bool y6 x6) ⊗ (eq_bool y7 x7) ⊗ (eq_bool y8 x8) ⊗
 676    (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗ (eq_bool y12 x12)));
 677  nrewrite > (symmetric_eqb8 x1 y1);
 678  nrewrite > (symmetric_eqb8 x2 y2);
 679  nrewrite > (symmetric_eqb8 x3 y3);
 680  nrewrite > (symmetric_eqw16 x4 y4);
 681  nrewrite > (symmetric_eqw16 x5 y5);
 682  nrewrite > (symmetric_eqbool x6 y6);
 683  nrewrite > (symmetric_eqbool x7 y7);
 684  nrewrite > (symmetric_eqbool x8 y8);
 685  nrewrite > (symmetric_eqbool x9 y9);
 686  nrewrite > (symmetric_eqbool x10 y10);
 687  nrewrite > (symmetric_eqbool x11 y11);
 688  nrewrite > (symmetric_eqbool x12 y12);
 689  napply refl_eq.
 690 nqed.
 691
 692 nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_aluHC08 alu1 alu2 = true → alu1 = alu2.
 693  #alu1; #alu2;
 694  ncases alu1;
 695  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 696  ncases alu2;
 697  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 698  nchange in H:(%) with (
 699  ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 700   (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
 701   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) = true);
 702  nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
 703  nletin H1 ≝ (andb_true_true_l … H);
 704  nrewrite > (eqbool_to_eq … (andb_true_true_r … H1));
 705  nletin H2 ≝ (andb_true_true_l … H1);
 706  nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
 707  nletin H3 ≝ (andb_true_true_l … H2);
 708  nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
 709  nletin H4 ≝ (andb_true_true_l … H3);
 710  nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
 711  nletin H5 ≝ (andb_true_true_l … H4);
 712  nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
 713  nletin H6 ≝ (andb_true_true_l … H5);
 714  nrewrite > (eqbool_to_eq … (andb_true_true_r … H6));
 715  nletin H7 ≝ (andb_true_true_l … H6);
 716  nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
 717  nletin H8 ≝ (andb_true_true_l … H7);
 718  nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
 719  nletin H9 ≝ (andb_true_true_l … H8);
 720  nrewrite > (eqb8_to_eq … (andb_true_true_r … H9));
 721  nletin H10 ≝ (andb_true_true_l … H9);
 722  nrewrite > (eqb8_to_eq … (andb_true_true_r … H10));
 723  nrewrite > (eqb8_to_eq … (andb_true_true_l … H10));
 724  napply refl_eq.
 725 nqed.
 726
 727 nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_aluHC08 alu1 alu2 = true.
 728  #alu1; #alu2;
 729  ncases alu1;
 730  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 731  ncases alu2;
 732  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 733  nrewrite > (aluHC08_destruct_1 … H);
 734  nrewrite > (aluHC08_destruct_2 … H);
 735  nrewrite > (aluHC08_destruct_3 … H);
 736  nrewrite > (aluHC08_destruct_4 … H);
 737  nrewrite > (aluHC08_destruct_5 … H);
 738  nrewrite > (aluHC08_destruct_6 … H);
 739  nrewrite > (aluHC08_destruct_7 … H);
 740  nrewrite > (aluHC08_destruct_8 … H);
 741  nrewrite > (aluHC08_destruct_9 … H);
 742  nrewrite > (aluHC08_destruct_10 … H);
 743  nrewrite > (aluHC08_destruct_11 … H);
 744  nrewrite > (aluHC08_destruct_12 … H);
 745  nchange with (
 746  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 747   (eq_w16 y5 y5) ⊗ (eq_bool y6 y6) ⊗ (eq_bool y7 y7) ⊗ (eq_bool y8 y8) ⊗
 748   (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗ (eq_bool y11 y11) ⊗ (eq_bool y12 y12)) = true);
 749  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
 750  nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
 751  nrewrite > (eq_to_eqb8 y3 y3 (refl_eq …));
 752  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
 753  nrewrite > (eq_to_eqw16 y5 y5 (refl_eq …));
 754  nrewrite > (eq_to_eqbool y6 y6 (refl_eq …));
 755  nrewrite > (eq_to_eqbool y7 y7 (refl_eq …));
 756  nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
 757  nrewrite > (eq_to_eqbool y9 y9 (refl_eq …));
 758  nrewrite > (eq_to_eqbool y10 y10 (refl_eq …));
 759  nrewrite > (eq_to_eqbool y11 y11 (refl_eq …));
 760  nrewrite > (eq_to_eqbool y12 y12 (refl_eq …));
 761  napply refl_eq.
 762 nqed.
 763
 764 nlemma decidable_aluHC08_aux1
 765  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 766  (x1 ≠ y1) →
 767  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 768  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 769  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 770  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 771  nnormalize; #H; #H1;
 772  napply (H (aluHC08_destruct_1 … H1)).
 773 nqed.
 774
 775 nlemma decidable_aluHC08_aux2
 776  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 777  (x2 ≠ y2) →
 778  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 779  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 780  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 781  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 782  nnormalize; #H; #H1;
 783  napply (H (aluHC08_destruct_2 … H1)).
 784 nqed.
 785
 786 nlemma decidable_aluHC08_aux3
 787  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 788  (x3 ≠ y3) →
 789  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 790  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 791  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 792  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 793  nnormalize; #H; #H1;
 794  napply (H (aluHC08_destruct_3 … H1)).
 795 nqed.
 796
 797 nlemma decidable_aluHC08_aux4
 798  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 799  (x4 ≠ y4) →
 800  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 801  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 802  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 803  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 804  nnormalize; #H; #H1;
 805  napply (H (aluHC08_destruct_4 … H1)).
 806 nqed.
 807
 808 nlemma decidable_aluHC08_aux5
 809  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 810  (x5 ≠ y5) →
 811  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 812  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 813  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 814  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 815  nnormalize; #H; #H1;
 816  napply (H (aluHC08_destruct_5 … H1)).
 817 nqed.
 818
 819 nlemma decidable_aluHC08_aux6
 820  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 821  (x6 ≠ y6) →
 822  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 823  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 824  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 825  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 826  nnormalize; #H; #H1;
 827  napply (H (aluHC08_destruct_6 … H1)).
 828 nqed.
 829
 830 nlemma decidable_aluHC08_aux7
 831  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 832  (x7 ≠ y7) →
 833  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 834  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 835  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 836  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 837  nnormalize; #H; #H1;
 838  napply (H (aluHC08_destruct_7 … H1)).
 839 nqed.
 840
 841 nlemma decidable_aluHC08_aux8
 842  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 843  (x8 ≠ y8) →
 844  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 845  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 846  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 847  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 848  nnormalize; #H; #H1;
 849  napply (H (aluHC08_destruct_8 … H1)).
 850 nqed.
 851
 852 nlemma decidable_aluHC08_aux9
 853  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 854  (x9 ≠ y9) →
 855  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 856  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 857  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 858  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 859  nnormalize; #H; #H1;
 860  napply (H (aluHC08_destruct_9 … H1)).
 861 nqed.
 862
 863 nlemma decidable_aluHC08_aux10
 864  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 865  (x10 ≠ y10) →
 866  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 867  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 868  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 869  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 870  nnormalize; #H; #H1;
 871  napply (H (aluHC08_destruct_10 … H1)).
 872 nqed.
 873
 874 nlemma decidable_aluHC08_aux11
 875  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 876  (x11 ≠ y11) →
 877  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 878  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 879  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 880  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 881  nnormalize; #H; #H1;
 882  napply (H (aluHC08_destruct_11 … H1)).
 883 nqed.
 884
 885 nlemma decidable_aluHC08_aux12
 886  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 887  (x12 ≠ y12) →
 888  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 889  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 890  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 891  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 892  nnormalize; #H; #H1;
 893  napply (H (aluHC08_destruct_12 … H1)).
 894 nqed.
 895
 896 nlemma decidable_aluHC08 : ∀x,y:alu_HC08.decidable (x = y).
 897  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 898  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 899  nnormalize;
 900  napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
 901  ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC08_aux1 … H))
 902  ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
 903   ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC08_aux2 … H1))
 904   ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x3 y3) …);
 905    ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC08_aux3 … H2))
 906    ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
 907     ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC08_aux4 … H3))
 908     ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …);
 909      ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC08_aux5 … H4))
 910      ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x6 y6) …);
 911       ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC08_aux6 … H5))
 912       ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …);
 913        ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC08_aux7 … H6))
 914        ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
 915         ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC08_aux8 … H7))
 916         ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …);
 917          ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC08_aux9 … H8))
 918          ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …);
 919           ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC08_aux10 … H9))
 920           ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …);
 921            ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC08_aux11 … H10))
 922            ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …);
 923             ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC08_aux12 … H11))
 924             ##| ##1: #H11; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
 925                       nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
 926                       nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
 927                       napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 928             ##]
 929            ##]
 930           ##]
 931          ##]
 932         ##]
 933        ##]
 934       ##]
 935      ##]
 936     ##]
 937    ##]
 938   ##]
 939  ##]
 940 nqed.
 941
 942 nlemma aluRS08_destruct_1 :
 943 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 944  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 945  x1 = y1.
 946  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 947  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 948  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 949                 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
 950  nrewrite < H;
 951  nnormalize;
 952  napply refl_eq.
 953 nqed.
 954
 955 nlemma aluRS08_destruct_2 :
 956 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 957  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 958  x2 = y2.
 959  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 960  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 961  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 962                 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
 963  nrewrite < H;
 964  nnormalize;
 965  napply refl_eq.
 966 nqed.
 967
 968 nlemma aluRS08_destruct_3 :
 969 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 970  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 971  x3 = y3.
 972  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 973  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 974  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 975                 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
 976  nrewrite < H;
 977  nnormalize;
 978  napply refl_eq.
 979 nqed.
 980
 981 nlemma aluRS08_destruct_4 :
 982 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 983  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 984  x4 = y4.
 985  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 986  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 987  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 988                 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
 989  nrewrite < H;
 990  nnormalize;
 991  napply refl_eq.
 992 nqed.
 993
 994 nlemma aluRS08_destruct_5 :
 995 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 996  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 997  x5 = y5.
 998  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 999  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1000  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
1001                 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
1002  nrewrite < H;
1003  nnormalize;
1004  napply refl_eq.
1005 nqed.
1006
1007 nlemma aluRS08_destruct_6 :
1008 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1009  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
1010  x6 = y6.
1011  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1012  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1013  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
1014                 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
1015  nrewrite < H;
1016  nnormalize;
1017  napply refl_eq.
1018 nqed.
1019
1020 nlemma aluRS08_destruct_7 :
1021 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1022  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
1023  x7 = y7.
1024  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1025  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1026  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
1027                 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
1028  nrewrite < H;
1029  nnormalize;
1030  napply refl_eq.
1031 nqed.
1032
1033 nlemma aluRS08_destruct_8 :
1034 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1035  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
1036  x8 = y8.
1037  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1038  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1039  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
1040                 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
1041  nrewrite < H;
1042  nnormalize;
1043  napply refl_eq.
1044 nqed.
1045
1046 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_aluRS08.
1047  #alu1; #alu2;
1048  ncases alu1;
1049  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1050  ncases alu2;
1051  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1052  nchange with (
1053   ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
1054    (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
1055    (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
1056    (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) =
1057   ((eq_b8 y1 x1) ⊗ (eq_w16 y2 x2) ⊗
1058    (eq_w16 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
1059    (eq_b8 y5 x5) ⊗ (eq_b8 y6 x6) ⊗
1060    (eq_bool y7 x7) ⊗ (eq_bool y8 x8)));
1061  nrewrite > (symmetric_eqb8 x1 y1);
1062  nrewrite > (symmetric_eqw16 x2 y2);
1063  nrewrite > (symmetric_eqw16 x3 y3);
1064  nrewrite > (symmetric_eqw16 x4 y4);
1065  nrewrite > (symmetric_eqb8 x5 y5);
1066  nrewrite > (symmetric_eqb8 x6 y6);
1067  nrewrite > (symmetric_eqbool x7 y7);
1068  nrewrite > (symmetric_eqbool x8 y8);
1069  napply refl_eq.
1070 nqed.
1071
1072 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_aluRS08 alu1 alu2 = true → alu1 = alu2.
1073  #alu1; #alu2;
1074  ncases alu1;
1075  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1076  ncases alu2;
1077  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1078  nchange in H:(%) with (
1079   ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
1080    (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
1081    (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
1082    (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) = true);
1083  nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
1084  nletin H1 ≝ (andb_true_true_l … H);
1085  nrewrite > (eqbool_to_eq … (andb_true_true_r … H1));
1086  nletin H2 ≝ (andb_true_true_l … H1);
1087  nrewrite > (eqb8_to_eq … (andb_true_true_r … H2));
1088  nletin H3 ≝ (andb_true_true_l … H2);
1089  nrewrite > (eqb8_to_eq … (andb_true_true_r … H3));
1090  nletin H4 ≝ (andb_true_true_l … H3);
1091  nrewrite > (eqw16_to_eq … (andb_true_true_r … H4));
1092  nletin H5 ≝ (andb_true_true_l … H4);
1093  nrewrite > (eqw16_to_eq … (andb_true_true_r … H5));
1094  nletin H6 ≝ (andb_true_true_l … H5);
1095  nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
1096  nrewrite > (eqb8_to_eq … (andb_true_true_l … H6));
1097  napply refl_eq.
1098 nqed.
1099
1100 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_aluRS08 alu1 alu2 = true.
1101  #alu1; #alu2;
1102  ncases alu1;
1103  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1104  ncases alu2;
1105  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
1106  nrewrite > (aluRS08_destruct_1 … H);
1107  nrewrite > (aluRS08_destruct_2 … H);
1108  nrewrite > (aluRS08_destruct_3 … H);
1109  nrewrite > (aluRS08_destruct_4 … H);
1110  nrewrite > (aluRS08_destruct_5 … H);
1111  nrewrite > (aluRS08_destruct_6 … H);
1112  nrewrite > (aluRS08_destruct_7 … H);
1113  nrewrite > (aluRS08_destruct_8 … H);
1114  nchange with (
1115   ((eq_b8 y1 y1) ⊗ (eq_w16 y2 y2) ⊗
1116    (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
1117    (eq_b8 y5 y5) ⊗ (eq_b8 y6 y6) ⊗
1118    (eq_bool y7 y7) ⊗ (eq_bool y8 y8)) = true);
1119  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
1120  nrewrite > (eq_to_eqw16 y2 y2 (refl_eq …));
1121  nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
1122  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
1123  nrewrite > (eq_to_eqb8 y5 y5 (refl_eq …));
1124  nrewrite > (eq_to_eqb8 y6 y6 (refl_eq …));
1125  nrewrite > (eq_to_eqbool y7 y7 (refl_eq …));
1126  nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
1127  napply refl_eq.
1128 nqed.
1129
1130 nlemma decidable_aluRS08_aux1
1131  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1132  (x1 ≠ y1) →
1133  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1134  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1135  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1136  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1137  nnormalize; #H; #H1;
1138  napply (H (aluRS08_destruct_1 … H1)).
1139 nqed.
1140
1141 nlemma decidable_aluRS08_aux2
1142  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1143  (x2 ≠ y2) →
1144  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1145  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1146  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1147  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1148  nnormalize; #H; #H1;
1149  napply (H (aluRS08_destruct_2 … H1)).
1150 nqed.
1151
1152 nlemma decidable_aluRS08_aux3
1153  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1154  (x3 ≠ y3) →
1155  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1156  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1157  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1158  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1159  nnormalize; #H; #H1;
1160  napply (H (aluRS08_destruct_3 … H1)).
1161 nqed.
1162
1163 nlemma decidable_aluRS08_aux4
1164  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1165  (x4 ≠ y4) →
1166  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1167  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1168  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1169  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1170  nnormalize; #H; #H1;
1171  napply (H (aluRS08_destruct_4 … H1)).
1172 nqed.
1173
1174 nlemma decidable_aluRS08_aux5
1175  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1176  (x5 ≠ y5) →
1177  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1178  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1179  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1180  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1181  nnormalize; #H; #H1;
1182  napply (H (aluRS08_destruct_5 … H1)).
1183 nqed.
1184
1185 nlemma decidable_aluRS08_aux6
1186  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1187  (x6 ≠ y6) →
1188  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1189  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1190  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1191  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1192  nnormalize; #H; #H1;
1193  napply (H (aluRS08_destruct_6 … H1)).
1194 nqed.
1195
1196 nlemma decidable_aluRS08_aux7
1197  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1198  (x7 ≠ y7) →
1199  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1200  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1201  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1202  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1203  nnormalize; #H; #H1;
1204  napply (H (aluRS08_destruct_7 … H1)).
1205 nqed.
1206
1207 nlemma decidable_aluRS08_aux8
1208  : ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
1209  (x8 ≠ y8) →
1210  (mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8) ≠
1211  (mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8).
1212  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1213  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1214  nnormalize; #H; #H1;
1215  napply (H (aluRS08_destruct_8 … H1)).
1216 nqed.
1217
1218 nlemma decidable_aluRS08 : ∀x,y:alu_RS08.decidable (x = y).
1219  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1220  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1221  nnormalize;
1222  napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
1223  ##[ ##2: #H; napply (or2_intro2 … (decidable_aluRS08_aux1 … H))
1224  ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x2 y2) …);
1225   ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluRS08_aux2 … H1))
1226   ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
1227    ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluRS08_aux3 … H2))
1228    ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
1229     ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluRS08_aux4 … H3))
1230     ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x5 y5) …);
1231      ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluRS08_aux5 … H4))
1232      ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x6 y6) …);
1233       ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluRS08_aux6 … H5))
1234       ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …);
1235        ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluRS08_aux7 … H6))
1236        ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
1237         ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluRS08_aux8 … H7))
1238         ##| ##1: #H7; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
1239                       nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
1240                       napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
1241         ##]
1242        ##]
1243       ##]
1244      ##]
1245     ##]
1246    ##]
1247   ##]
1248  ##]
1249 nqed.
1250
1251 nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 clk1.
1252  #mcu; #clk1; #clk2;
1253  ncases clk1;
1254  ncases clk2;
1255  ##[ ##1: napply refl_eq
1256  ##| ##2,3: nnormalize; #H; napply refl_eq
1257  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
1258           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5;
1259           nchange with (
1260            ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
1261            ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_im x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
1262           nrewrite > (symmetric_eqb8 x1 y1);
1263           nrewrite > (symmetric_eqanyop ? x2 y2);
1264           nrewrite > (symmetric_eqim x3 y3);
1265           nrewrite > (symmetric_eqb8 x4 y4);
1266           nrewrite > (symmetric_eqw16 x5 y5);
1267           napply refl_eq
1268  ##]
1269 nqed.
1270
1271 nlemma eqclk_to_eq : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = true → clk1 = clk2.
1272  #mcu; #clk1; #clk2;
1273  ncases clk1;
1274  ncases clk2;
1275  ##[ ##1: nnormalize; #H; napply refl_eq
1276  ##| ##2,3: nnormalize; #H; #H1; napply (bool_destruct … H1)
1277  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
1278           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
1279           nchange in H:(%) with (
1280            ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_im y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
1281            nrewrite > (eqw16_to_eq … (andb_true_true_r … H));
1282            nletin H1 ≝ (andb_true_true_l … H);
1283            nrewrite > (eqb8_to_eq … (andb_true_true_r … H1));
1284            nletin H2 ≝ (andb_true_true_l … H1);
1285            nrewrite > (eqim_to_eq … (andb_true_true_r … H2));
1286            nletin H3 ≝ (andb_true_true_l … H2);
1287            nrewrite > (eqanyop_to_eq … (andb_true_true_r … H3));
1288            nrewrite > (eqb8_to_eq … (andb_true_true_l … H3));
1289            napply refl_eq
1290  ##]
1291 nqed.
1292
1293 nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = true.
1294  #mcu; #clk1; #clk2;
1295  ncases clk1;
1296  ncases clk2;
1297  ##[ ##1: nnormalize; #H; napply refl_eq
1298  ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ? p … H1)
1299  ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ? p … H1)
1300  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
1301           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
1302           nrewrite > (quintuple_destruct_1 … (option_destruct_some_some … H));
1303           nrewrite > (quintuple_destruct_2 … (option_destruct_some_some … H));
1304           nrewrite > (quintuple_destruct_3 … (option_destruct_some_some … H));
1305           nrewrite > (quintuple_destruct_4 … (option_destruct_some_some … H));
1306           nrewrite > (quintuple_destruct_5 … (option_destruct_some_some … H));
1307           nchange with (
1308            ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_im x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
1309           nrewrite > (eq_to_eqb8 x1 x1 (refl_eq …));
1310           nrewrite > (eq_to_eqanyop mcu x2 x2 (refl_eq ? x2));
1311           nrewrite > (eq_to_eqim x3 x3 (refl_eq …));
1312           nrewrite > (eq_to_eqb8 x4 x4 (refl_eq …));
1313           nrewrite > (eq_to_eqw16 x5 x5 (refl_eq …));
1314           nnormalize;
1315           napply refl_eq
1316  ##]
1317 nqed.
1318
1319 nlemma symmetric_forallmemoryranged :
1320 ∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀addrl.
1321  forall_memory_ranged t chk1 chk2 mem1 mem2 addrl =
1322  forall_memory_ranged t chk2 chk1 mem2 mem1 addrl.
1323  #t; #chk1; #chk2; #mem1; #mem2; #addrl;
1324  napply (list_ind word16 … addrl);
1325  ##[ ##1: nnormalize; napply refl_eq
1326  ##| ##2: #a; #l; #H;
1327           nchange with (
1328            ((eq_option byte8 (mem_read t mem1 chk1 a)
1329                             (mem_read t mem2 chk2 a) eq_b8) ⊗
1330            (forall_memory_ranged t chk1 chk2 mem1 mem2 l)) =
1331            ((eq_option byte8 (mem_read t mem2 chk2 a)
1332                             (mem_read t mem1 chk1 a) eq_b8) ⊗
1333            (forall_memory_ranged t chk2 chk1 mem2 mem1 l)));
1334            nrewrite > H;
1335            nrewrite > (symmetric_eqoption ? (mem_read t mem1 chk1 a) (mem_read t mem2 chk2 a) eq_b8 symmetric_eqb8);
1336            napply refl_eq
1337  ##]
1338 nqed.
1339
1340 nlemma anystatus_destruct_1 :
1341 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
1342  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
1343  x1 = y1.
1344  #m; #t;
1345  #x1; #x2; #x3; #x4;
1346  #y1; #y2; #y3; #y4; #H;
1347  nchange with (match mk_any_status m t y1 y2 y3 y4
1348                 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
1349  nrewrite < H;
1350  nnormalize;
1351  napply refl_eq.
1352 nqed.
1353
1354 nlemma anystatus_destruct_2 :
1355 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
1356  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
1357  x2 = y2.
1358  #m; #t;
1359  #x1; #x2; #x3; #x4;
1360  #y1; #y2; #y3; #y4; #H;
1361  nchange with (match mk_any_status m t y1 y2 y3 y4
1362                 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
1363  nrewrite < H;
1364  nnormalize;
1365  napply refl_eq.
1366 nqed.
1367
1368 nlemma anystatus_destruct_3 :
1369 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
1370  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
1371  x3 = y3.
1372  #m; #t;
1373  #x1; #x2; #x3; #x4;
1374  #y1; #y2; #y3; #y4; #H;
1375  nchange with (match mk_any_status m t y1 y2 y3 y4
1376                 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
1377  nrewrite < H;
1378  nnormalize;
1379  napply refl_eq.
1380 nqed.
1381
1382 nlemma anystatus_destruct_4 :
1383 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
1384  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
1385  x4 = y4.
1386  #m; #t;
1387  #x1; #x2; #x3; #x4;
1388  #y1; #y2; #y3; #y4; #H;
1389  nchange with (match mk_any_status m t y1 y2 y3 y4
1390                 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
1391  nrewrite < H;
1392  nnormalize;
1393  napply refl_eq.
1394 nqed.
1395
1396 nlemma symmetric_eqanystatus :
1397 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1398  eq_anystatus m t s1 s2 addrl = eq_anystatus m t s2 s1 addrl.
1399  #addrl; #m;
1400  ncases m; #t; #s1;
1401  ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
1402           #s2; ncases s2; #y1; #y2; #y3; #y4;
1403           nchange with (
1404            ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) =
1405            ((eq_aluHC05 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4)));
1406            nrewrite > (symmetric_eqaluHC05 x1 y1)
1407  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
1408           #s2; ncases s2; #y1; #y2; #y3; #y4;
1409           nchange with (
1410            ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) =
1411            ((eq_aluHC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4)));
1412            nrewrite > (symmetric_eqaluHC08 x1 y1)
1413  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
1414           #s2; ncases s2; #y1; #y2; #y3; #y4;
1415           nchange with (
1416            ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) =
1417            ((eq_aluRS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4)));
1418            nrewrite > (symmetric_eqaluRS08 x1 y1)
1419  ##]
1420  nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
1421  nrewrite > (symmetric_eqclk ? x4 y4);
1422  napply refl_eq.
1423 nqed.
1424
1425 nlemma eqanystatus_to_eq :
1426 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1427  (eq_anystatus m t s1 s2 addrl = true) →
1428   And3 (alu m t s1 = alu m t s2)
1429        (clk_desc m t s1 = clk_desc m t s2)
1430        ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
1431                                 (mem_desc m t s1) (mem_desc m t s2) addrl) = true).
1432  #addrl; #m; #t;
1433  ncases m; #s1;
1434  ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
1435           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1436           nchange in H:(%) with (
1437            ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1438            nrewrite > (eqaluHC05_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
1439  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
1440           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1441           nchange in H:(%) with (
1442            ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1443            nrewrite > (eqaluHC08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
1444  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
1445           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1446           nchange in H:(%) with (
1447            ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1448            nrewrite > (eqaluRS08_to_eq … (andb_true_true_l … (andb_true_true_l … H)))
1449  ##]
1450  nchange with (And3 (y1 = y1) (x4 = y4) (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
1451  nrewrite > (andb_true_true_r … (andb_true_true_l … H));
1452  nrewrite > (eqclk_to_eq … (andb_true_true_r … H));
1453  napply (conj3 … (refl_eq ? y1) (refl_eq ? y4) (refl_eq ? true)).
1454 nqed.
1455
1456 nlemma eq_to_eqanystatus_strong :
1457 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1458  s1 = s2 → (eq_anystatus m t s1 s2 addrl = true).
1459  #addrl; #m; #t;
1460  ncases m;
1461  ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
1462           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1463           nchange with (
1464            ((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1465           nrewrite > (anystatus_destruct_1 … H);
1466           nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
1467  ##| ##2,3:  #s1; ncases s1; #x1; #x2; #x3; #x4;
1468           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1469           nchange with (
1470            ((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1471           nrewrite > (anystatus_destruct_1 … H);
1472           nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
1473  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
1474           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
1475           nchange with (
1476            ((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1477           nrewrite > (anystatus_destruct_1 … H);
1478           nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))
1479  ##]
1480  nrewrite > (anystatus_destruct_2 … H);
1481  nrewrite > (anystatus_destruct_3 … H);
1482  nrewrite > (anystatus_destruct_4 … H);
1483  nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …));
1484  nchange with ((forall_memory_ranged … ⊗ true) =true);
1485  nrewrite > (symmetric_andbool (forall_memory_ranged t y3 y3 y2 y2 addrl) true);
1486  nchange with ((forall_memory_ranged t y3 y3 y2 y2 ?) = true);
1487  napply (list_ind word16 … addrl);
1488  ##[ ##1,3,5,7: nnormalize; napply refl_eq
1489  ##| ##2,4,6,8: #a; #l'; #H;
1490           nchange with (
1491           ((eq_option byte8 (mem_read t y2 y3 a)
1492                             (mem_read t y2 y3 a) eq_b8) ⊗
1493            (forall_memory_ranged t y3 y3 y2 y2 l')) = true);
1494           nrewrite > H;
1495           nrewrite > (eq_to_eqoption ? (mem_read t y2 y3 a) (mem_read t y2 y3 a) eq_b8 eq_to_eqb8 (refl_eq …));
1496           nnormalize;
1497           napply refl_eq
1498  ##]
1499 nqed.
1500
1501 nlemma eq_to_eqanystatus_weak :
1502 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1503  (alu m t s1 = alu m t s2) →
1504  (clk_desc m t s1 = clk_desc m t s2) →
1505  ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
1506                             (mem_desc m t s1) (mem_desc m t s2) addrl) = true) →
1507  (eq_anystatus m t s1 s2 addrl = true).
1508  #addrl; #m; #t;
1509  ncases m;
1510  ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
1511           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1512           nchange with (((eq_aluHC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1513           nchange in H:(%) with (x1 = y1);
1514           nrewrite > H;
1515           nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq …))
1516  ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4;
1517           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1518           nchange with (((eq_aluHC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1519           nchange in H:(%) with (x1 = y1);
1520           nrewrite > H;
1521           nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq …))
1522  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
1523           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1524           nchange with (((eq_aluRS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1525           nchange in H:(%) with (x1 = y1);
1526           nrewrite > H;
1527           nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq …))
1528  ##]
1529  nchange in H2:(%) with (forall_memory_ranged t x3 y3 x2 y2 addrl = true);
1530  nrewrite > H2;
1531  nchange in H1:(%) with (x4 = y4);
1532  nrewrite > H1;
1533  nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq …));
1534  nnormalize;
1535  napply refl_eq.
1536 nqed.