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: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
  19 (*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "freescale/word16_lemmas.ma".
  24 include "freescale/opcode_base_lemmas1.ma".
  25 include "freescale/status.ma".
  26 include "freescale/option_lemmas.ma".
  27 include "freescale/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_alu_HC05.
 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_alu_HC05 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_alu_HC05 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 aluHC08_destruct_1 :
 317 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 318  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 →
 319  x1 = y1.
 320  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 321  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 322  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 323                 with [ mk_alu_HC08 a _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
 324  nrewrite < H;
 325  nnormalize;
 326  napply (refl_eq ??).
 327 nqed.
 328
 329 nlemma aluHC08_destruct_2 :
 330 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 331  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 →
 332  x2 = y2.
 333  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 334  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 335  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 336                 with [ mk_alu_HC08 _ a _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
 337  nrewrite < H;
 338  nnormalize;
 339  napply (refl_eq ??).
 340 nqed.
 341
 342 nlemma aluHC08_destruct_3 :
 343 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 344  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 →
 345  x3 = y3.
 346  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 347  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 348  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 349                 with [ mk_alu_HC08 _ _ a _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
 350  nrewrite < H;
 351  nnormalize;
 352  napply (refl_eq ??).
 353 nqed.
 354
 355 nlemma aluHC08_destruct_4 :
 356 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 357  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 →
 358  x4 = y4.
 359  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 360  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 361  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 362                 with [ mk_alu_HC08 _ _ _ a _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
 363  nrewrite < H;
 364  nnormalize;
 365  napply (refl_eq ??).
 366 nqed.
 367
 368 nlemma aluHC08_destruct_5 :
 369 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 370  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 →
 371  x5 = y5.
 372  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 373  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 374  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 375                 with [ mk_alu_HC08 _ _ _ _ a _ _ _ _ _ _ _ ⇒ x5 = a ]);
 376  nrewrite < H;
 377  nnormalize;
 378  napply (refl_eq ??).
 379 nqed.
 380
 381 nlemma aluHC08_destruct_6 :
 382 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 383  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 →
 384  x6 = y6.
 385  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 386  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 387  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 388                 with [ mk_alu_HC08 _ _ _ _ _ a _ _ _ _ _ _ ⇒ x6 = a ]);
 389  nrewrite < H;
 390  nnormalize;
 391  napply (refl_eq ??).
 392 nqed.
 393
 394 nlemma aluHC08_destruct_7 :
 395 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 396  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 →
 397  x7 = y7.
 398  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 399  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 400  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 401                 with [ mk_alu_HC08 _ _ _ _ _ _ a _ _ _ _ _ ⇒ x7 = a ]);
 402  nrewrite < H;
 403  nnormalize;
 404  napply (refl_eq ??).
 405 nqed.
 406
 407 nlemma aluHC08_destruct_8 :
 408 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 409  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 →
 410  x8 = y8.
 411  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 412  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 413  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 414                 with [ mk_alu_HC08 _ _ _ _ _ _ _ a _ _ _ _ ⇒ x8 = a ]);
 415  nrewrite < H;
 416  nnormalize;
 417  napply (refl_eq ??).
 418 nqed.
 419
 420 nlemma aluHC08_destruct_9 :
 421 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 422  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 →
 423  x9 = y9.
 424  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 425  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 426  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 427                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ a _ _ _ ⇒ x9 = a ]);
 428  nrewrite < H;
 429  nnormalize;
 430  napply (refl_eq ??).
 431 nqed.
 432
 433 nlemma aluHC08_destruct_10 :
 434 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 435  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 →
 436  x10 = y10.
 437  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 438  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 439  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 440                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ a _ _ ⇒ x10 = a ]);
 441  nrewrite < H;
 442  nnormalize;
 443  napply (refl_eq ??).
 444 nqed.
 445
 446 nlemma aluHC08_destruct_11 :
 447 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 448  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 →
 449  x11 = y11.
 450  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 451  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 452  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 453                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ a _ ⇒ x11 = a ]);
 454  nrewrite < H;
 455  nnormalize;
 456  napply (refl_eq ??).
 457 nqed.
 458
 459 nlemma aluHC08_destruct_12 :
 460 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 461  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 →
 462  x12 = y12.
 463  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 464  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 465  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 466                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ a ⇒ x12 = a ]);
 467  nrewrite < H;
 468  nnormalize;
 469  napply (refl_eq ??).
 470 nqed.
 471
 472 nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08.
 473  #alu1; #alu2;
 474  ncases alu1;
 475  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 476  ncases alu2;
 477  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 478  nchange with (
 479   ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 480    (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
 481    (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) =
 482    ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_b8 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
 483    (eq_w16 y5 x5) ⊗ (eq_bool y6 x6) ⊗ (eq_bool y7 x7) ⊗ (eq_bool y8 x8) ⊗
 484    (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗ (eq_bool y12 x12)));
 485  nrewrite > (symmetric_eqb8 x1 y1);
 486  nrewrite > (symmetric_eqb8 x2 y2);
 487  nrewrite > (symmetric_eqb8 x3 y3);
 488  nrewrite > (symmetric_eqw16 x4 y4);
 489  nrewrite > (symmetric_eqw16 x5 y5);
 490  nrewrite > (symmetric_eqbool x6 y6);
 491  nrewrite > (symmetric_eqbool x7 y7);
 492  nrewrite > (symmetric_eqbool x8 y8);
 493  nrewrite > (symmetric_eqbool x9 y9);
 494  nrewrite > (symmetric_eqbool x10 y10);
 495  nrewrite > (symmetric_eqbool x11 y11);
 496  nrewrite > (symmetric_eqbool x12 y12);
 497  napply (refl_eq ??).
 498 nqed.
 499
 500 nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = alu2.
 501  #alu1; #alu2;
 502  ncases alu1;
 503  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 504  ncases alu2;
 505  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 506  nchange in H:(%) with (
 507  ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 508   (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
 509   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) = true);
 510  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
 511  nletin H1 ≝ (andb_true_true_l ?? H);
 512  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
 513  nletin H2 ≝ (andb_true_true_l ?? H1);
 514  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
 515  nletin H3 ≝ (andb_true_true_l ?? H2);
 516  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
 517  nletin H4 ≝ (andb_true_true_l ?? H3);
 518  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
 519  nletin H5 ≝ (andb_true_true_l ?? H4);
 520  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
 521  nletin H6 ≝ (andb_true_true_l ?? H5);
 522  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H6));
 523  nletin H7 ≝ (andb_true_true_l ?? H6);
 524  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
 525  nletin H8 ≝ (andb_true_true_l ?? H7);
 526  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
 527  nletin H9 ≝ (andb_true_true_l ?? H8);
 528  nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H9));
 529  nletin H10 ≝ (andb_true_true_l ?? H9);
 530  nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H10));
 531  nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H10));
 532  napply (refl_eq ??).
 533 nqed.
 534
 535 nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = true.
 536  #alu1; #alu2;
 537  ncases alu1;
 538  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 539  ncases alu2;
 540  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 541  nrewrite > (aluHC08_destruct_1 ???????????????????????? H);
 542  nrewrite > (aluHC08_destruct_2 ???????????????????????? H);
 543  nrewrite > (aluHC08_destruct_3 ???????????????????????? H);
 544  nrewrite > (aluHC08_destruct_4 ???????????????????????? H);
 545  nrewrite > (aluHC08_destruct_5 ???????????????????????? H);
 546  nrewrite > (aluHC08_destruct_6 ???????????????????????? H);
 547  nrewrite > (aluHC08_destruct_7 ???????????????????????? H);
 548  nrewrite > (aluHC08_destruct_8 ???????????????????????? H);
 549  nrewrite > (aluHC08_destruct_9 ???????????????????????? H);
 550  nrewrite > (aluHC08_destruct_10 ???????????????????????? H);
 551  nrewrite > (aluHC08_destruct_11 ???????????????????????? H);
 552  nrewrite > (aluHC08_destruct_12 ???????????????????????? H);
 553  nchange with (
 554  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 555   (eq_w16 y5 y5) ⊗ (eq_bool y6 y6) ⊗ (eq_bool y7 y7) ⊗ (eq_bool y8 y8) ⊗
 556   (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗ (eq_bool y11 y11) ⊗ (eq_bool y12 y12)) = true);
 557  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
 558  nrewrite > (eq_to_eqb8 y2 y2 (refl_eq ??));
 559  nrewrite > (eq_to_eqb8 y3 y3 (refl_eq ??));
 560  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
 561  nrewrite > (eq_to_eqw16 y5 y5 (refl_eq ??));
 562  nrewrite > (eq_to_eqbool y6 y6 (refl_eq ??));
 563  nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
 564  nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
 565  nrewrite > (eq_to_eqbool y9 y9 (refl_eq ??));
 566  nrewrite > (eq_to_eqbool y10 y10 (refl_eq ??));
 567  nrewrite > (eq_to_eqbool y11 y11 (refl_eq ??));
 568  nrewrite > (eq_to_eqbool y12 y12 (refl_eq ??));
 569  napply (refl_eq ??).
 570 nqed.
 571
 572 nlemma aluRS08_destruct_1 :
 573 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 574  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 575  x1 = y1.
 576  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 577  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 578  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 579                 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
 580  nrewrite < H;
 581  nnormalize;
 582  napply (refl_eq ??).
 583 nqed.
 584
 585 nlemma aluRS08_destruct_2 :
 586 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 587  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 588  x2 = y2.
 589  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 590  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 591  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 592                 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
 593  nrewrite < H;
 594  nnormalize;
 595  napply (refl_eq ??).
 596 nqed.
 597
 598 nlemma aluRS08_destruct_3 :
 599 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 600  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 601  x3 = y3.
 602  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 603  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 604  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 605                 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
 606  nrewrite < H;
 607  nnormalize;
 608  napply (refl_eq ??).
 609 nqed.
 610
 611 nlemma aluRS08_destruct_4 :
 612 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 613  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 614  x4 = y4.
 615  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 616  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 617  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 618                 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
 619  nrewrite < H;
 620  nnormalize;
 621  napply (refl_eq ??).
 622 nqed.
 623
 624 nlemma aluRS08_destruct_5 :
 625 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 626  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 627  x5 = y5.
 628  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 629  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 630  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 631                 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
 632  nrewrite < H;
 633  nnormalize;
 634  napply (refl_eq ??).
 635 nqed.
 636
 637 nlemma aluRS08_destruct_6 :
 638 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 639  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 640  x6 = y6.
 641  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 642  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 643  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 644                 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
 645  nrewrite < H;
 646  nnormalize;
 647  napply (refl_eq ??).
 648 nqed.
 649
 650 nlemma aluRS08_destruct_7 :
 651 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 652  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 653  x7 = y7.
 654  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 655  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 656  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 657                 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
 658  nrewrite < H;
 659  nnormalize;
 660  napply (refl_eq ??).
 661 nqed.
 662
 663 nlemma aluRS08_destruct_8 :
 664 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 665  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 666  x8 = y8.
 667  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 668  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 669  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 670                 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
 671  nrewrite < H;
 672  nnormalize;
 673  napply (refl_eq ??).
 674 nqed.
 675
 676 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08.
 677  #alu1; #alu2;
 678  ncases alu1;
 679  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 680  ncases alu2;
 681  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 682  nchange with (
 683   ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
 684    (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 685    (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
 686    (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) =
 687   ((eq_b8 y1 x1) ⊗ (eq_w16 y2 x2) ⊗
 688    (eq_w16 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
 689    (eq_b8 y5 x5) ⊗ (eq_b8 y6 x6) ⊗
 690    (eq_bool y7 x7) ⊗ (eq_bool y8 x8)));
 691  nrewrite > (symmetric_eqb8 x1 y1);
 692  nrewrite > (symmetric_eqw16 x2 y2);
 693  nrewrite > (symmetric_eqw16 x3 y3);
 694  nrewrite > (symmetric_eqw16 x4 y4);
 695  nrewrite > (symmetric_eqb8 x5 y5);
 696  nrewrite > (symmetric_eqb8 x6 y6);
 697  nrewrite > (symmetric_eqbool x7 y7);
 698  nrewrite > (symmetric_eqbool x8 y8);
 699  napply (refl_eq ??).
 700 nqed.
 701
 702 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = alu2.
 703  #alu1; #alu2;
 704  ncases alu1;
 705  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 706  ncases alu2;
 707  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 708  nchange in H:(%) with (
 709   ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
 710    (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 711    (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
 712    (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) = true);
 713  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
 714  nletin H1 ≝ (andb_true_true_l ?? H);
 715  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
 716  nletin H2 ≝ (andb_true_true_l ?? H1);
 717  nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H2));
 718  nletin H3 ≝ (andb_true_true_l ?? H2);
 719  nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H3));
 720  nletin H4 ≝ (andb_true_true_l ?? H3);
 721  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H4));
 722  nletin H5 ≝ (andb_true_true_l ?? H4);
 723  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H5));
 724  nletin H6 ≝ (andb_true_true_l ?? H5);
 725  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
 726  nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H6));
 727  napply (refl_eq ??).
 728 nqed.
 729
 730 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = true.
 731  #alu1; #alu2;
 732  ncases alu1;
 733  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 734  ncases alu2;
 735  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 736  nrewrite > (aluRS08_destruct_1 ???????????????? H);
 737  nrewrite > (aluRS08_destruct_2 ???????????????? H);
 738  nrewrite > (aluRS08_destruct_3 ???????????????? H);
 739  nrewrite > (aluRS08_destruct_4 ???????????????? H);
 740  nrewrite > (aluRS08_destruct_5 ???????????????? H);
 741  nrewrite > (aluRS08_destruct_6 ???????????????? H);
 742  nrewrite > (aluRS08_destruct_7 ???????????????? H);
 743  nrewrite > (aluRS08_destruct_8 ???????????????? H);
 744  nchange with (
 745   ((eq_b8 y1 y1) ⊗ (eq_w16 y2 y2) ⊗
 746    (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 747    (eq_b8 y5 y5) ⊗ (eq_b8 y6 y6) ⊗
 748    (eq_bool y7 y7) ⊗ (eq_bool y8 y8)) = true);
 749  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
 750  nrewrite > (eq_to_eqw16 y2 y2 (refl_eq ??));
 751  nrewrite > (eq_to_eqw16 y3 y3 (refl_eq ??));
 752  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
 753  nrewrite > (eq_to_eqb8 y5 y5 (refl_eq ??));
 754  nrewrite > (eq_to_eqb8 y6 y6 (refl_eq ??));
 755  nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
 756  nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
 757  napply (refl_eq ??).
 758 nqed.
 759
 760 nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 clk1.
 761  #mcu; #clk1; #clk2;
 762  ncases clk1;
 763  ncases clk2;
 764  ##[ ##1: napply (refl_eq ??)
 765  ##| ##2,3: nnormalize; #H; napply (refl_eq ??)
 766  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
 767           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5;
 768           nchange with (
 769            ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
 770            ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_instrmode x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
 771           nrewrite > (symmetric_eqb8 x1 y1);
 772           nrewrite > (symmetric_eqanyop ? x2 y2);
 773           nrewrite > (symmetric_eqinstrmode x3 y3);
 774           nrewrite > (symmetric_eqb8 x4 y4);
 775           nrewrite > (symmetric_eqw16 x5 y5);
 776           napply (refl_eq ??)
 777  ##]
 778 nqed.
 779
 780 nlemma eqclk_to_eq : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = true → clk1 = clk2.
 781  #mcu; #clk1; #clk2;
 782  ncases clk1;
 783  ncases clk2;
 784  ##[ ##1: nnormalize; #H; napply (refl_eq ??)
 785  ##| ##2,3: nnormalize; #H; #H1; napply (bool_destruct ??? H1)
 786  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
 787           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
 788           nchange in H:(%) with (
 789            ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
 790            nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H));
 791            nletin H1 ≝ (andb_true_true_l ?? H);
 792            nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H1));
 793            nletin H2 ≝ (andb_true_true_l ?? H1);
 794            nrewrite > (eqinstrmode_to_eq ?? (andb_true_true_r ?? H2));
 795            nletin H3 ≝ (andb_true_true_l ?? H2);
 796            nrewrite > (eqanyop_to_eq ??? (andb_true_true_r ?? H3));
 797            nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H3));
 798            napply (refl_eq ??)
 799  ##]
 800 nqed.
 801
 802 nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = true.
 803  #mcu; #clk1; #clk2;
 804  ncases clk1;
 805  ncases clk2;
 806  ##[ ##1: nnormalize; #H; napply (refl_eq ??)
 807  ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ?? H1)
 808  ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ?? H1)
 809  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
 810           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
 811           nrewrite > (quintuple_destruct_1 ??????????????? (option_destruct_some_some ??? H));
 812           nrewrite > (quintuple_destruct_2 ??????????????? (option_destruct_some_some ??? H));
 813           nrewrite > (quintuple_destruct_3 ??????????????? (option_destruct_some_some ??? H));
 814           nrewrite > (quintuple_destruct_4 ??????????????? (option_destruct_some_some ??? H));
 815           nrewrite > (quintuple_destruct_5 ??????????????? (option_destruct_some_some ??? H));
 816           nchange with (
 817            ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_instrmode x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
 818           nrewrite > (eq_to_eqb8 x1 x1 (refl_eq ??));
 819           nrewrite > (eq_to_eqanyop mcu x2 x2 (refl_eq ? x2));
 820           nrewrite > (eq_to_eqinstrmode x3 x3 (refl_eq ??));
 821           nrewrite > (eq_to_eqb8 x4 x4 (refl_eq ??));
 822           nrewrite > (eq_to_eqw16 x5 x5 (refl_eq ??));
 823           nnormalize;
 824           napply (refl_eq ??)
 825  ##]
 826 nqed.
 827
 828 nlemma symmetric_forallmemoryranged :
 829 ∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀addrl.
 830  forall_memory_ranged t chk1 chk2 mem1 mem2 addrl =
 831  forall_memory_ranged t chk2 chk1 mem2 mem1 addrl.
 832  #t; #chk1; #chk2; #mem1; #mem2; #addrl;
 833  napply (list_ind word16 ??? addrl);
 834  ##[ ##1: nnormalize; napply (refl_eq ??)
 835  ##| ##2: #a; #l; #H;
 836           nchange with (
 837            ((eq_option byte8 (mem_read t mem1 chk1 a)
 838                             (mem_read t mem2 chk2 a) eq_b8) ⊗
 839            (forall_memory_ranged t chk1 chk2 mem1 mem2 l)) =
 840            ((eq_option byte8 (mem_read t mem2 chk2 a)
 841                             (mem_read t mem1 chk1 a) eq_b8) ⊗
 842            (forall_memory_ranged t chk2 chk1 mem2 mem1 l)));
 843            nrewrite > H;
 844            nrewrite > (symmetric_eqoption ? (mem_read t mem1 chk1 a) (mem_read t mem2 chk2 a) eq_b8 symmetric_eqb8);
 845            napply (refl_eq ??)
 846  ##]
 847 nqed.
 848
 849 nlemma anystatus_destruct_1 :
 850 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 851  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 852  x1 = y1.
 853  #m; #t;
 854  #x1; #x2; #x3; #x4;
 855  #y1; #y2; #y3; #y4; #H;
 856  nchange with (match mk_any_status m t y1 y2 y3 y4
 857                 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
 858  nrewrite < H;
 859  nnormalize;
 860  napply (refl_eq ??).
 861 nqed.
 862
 863 nlemma anystatus_destruct_2 :
 864 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 865  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 866  x2 = y2.
 867  #m; #t;
 868  #x1; #x2; #x3; #x4;
 869  #y1; #y2; #y3; #y4; #H;
 870  nchange with (match mk_any_status m t y1 y2 y3 y4
 871                 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
 872  nrewrite < H;
 873  nnormalize;
 874  napply (refl_eq ??).
 875 nqed.
 876
 877 nlemma anystatus_destruct_3 :
 878 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 879  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 880  x3 = y3.
 881  #m; #t;
 882  #x1; #x2; #x3; #x4;
 883  #y1; #y2; #y3; #y4; #H;
 884  nchange with (match mk_any_status m t y1 y2 y3 y4
 885                 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
 886  nrewrite < H;
 887  nnormalize;
 888  napply (refl_eq ??).
 889 nqed.
 890
 891 nlemma anystatus_destruct_4 :
 892 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 893  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 894  x4 = y4.
 895  #m; #t;
 896  #x1; #x2; #x3; #x4;
 897  #y1; #y2; #y3; #y4; #H;
 898  nchange with (match mk_any_status m t y1 y2 y3 y4
 899                 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
 900  nrewrite < H;
 901  nnormalize;
 902  napply (refl_eq ??).
 903 nqed.
 904
 905 nlemma symmetric_eqstatus :
 906 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 907  eq_status m t s1 s2 addrl = eq_status m t s2 s1 addrl.
 908  #addrl; #m;
 909  ncases m; #t; #s1;
 910  ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
 911           #s2; ncases s2; #y1; #y2; #y3; #y4;
 912           nchange with (
 913            ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) =
 914            ((eq_alu_HC05 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4)));
 915            nrewrite > (symmetric_eqaluHC05 x1 y1)
 916  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
 917           #s2; ncases s2; #y1; #y2; #y3; #y4;
 918           nchange with (
 919            ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) =
 920            ((eq_alu_HC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4)));
 921            nrewrite > (symmetric_eqaluHC08 x1 y1)
 922  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
 923           #s2; ncases s2; #y1; #y2; #y3; #y4;
 924           nchange with (
 925            ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) =
 926            ((eq_alu_RS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4)));
 927            nrewrite > (symmetric_eqaluRS08 x1 y1)
 928  ##]
 929  nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
 930  nrewrite > (symmetric_eqclk ? x4 y4);
 931  napply (refl_eq ??).
 932 nqed.
 933
 934 nlemma eqstatus_to_eq :
 935 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 936  (eq_status m t s1 s2 addrl = true) →
 937   ((alu m t s1 = alu m t s2) ∧
 938    (clk_desc m t s1 = clk_desc m t s2) ∧
 939    ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
 940                             (mem_desc m t s1) (mem_desc m t s2) addrl) = true)).
 941  #addrl; #m; #t;
 942  ncases m; #s1;
 943  ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
 944           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 945           nchange in H:(%) with (
 946            ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 947            nrewrite > (eqaluHC05_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
 948  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
 949           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 950           nchange in H:(%) with (
 951            ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 952            nrewrite > (eqaluHC08_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
 953  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
 954           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 955           nchange in H:(%) with (
 956            ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 957            nrewrite > (eqaluRS08_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
 958  ##]
 959  nchange with ((y1 = y1) ∧ (x4 = y4) ∧ (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
 960  nrewrite > (andb_true_true_r ?? (andb_true_true_l ?? H));
 961  nrewrite > (eqclk_to_eq ??? (andb_true_true_r ?? H));
 962  napply (conj ?? (conj ?? (refl_eq ??) (refl_eq ??)) (refl_eq ??)).
 963 nqed.
 964
 965 nlemma eq_to_eqstatus_strong :
 966 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 967  s1 = s2 → (eq_status m t s1 s2 addrl = true).
 968  #addrl; #m; #t;
 969  ncases m;
 970  ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
 971           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 972           nchange with (
 973            ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 974           nrewrite > (anystatus_destruct_1 ?????????? H);
 975           nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq ??))
 976  ##| ##2,3:  #s1; ncases s1; #x1; #x2; #x3; #x4;
 977           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 978           nchange with (
 979            ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 980           nrewrite > (anystatus_destruct_1 ?????????? H);
 981           nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq ??))
 982  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
 983           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 984           nchange with (
 985            ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 986           nrewrite > (anystatus_destruct_1 ?????????? H);
 987           nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
 988  ##]
 989  nrewrite > (anystatus_destruct_2 ?????????? H);
 990  nrewrite > (anystatus_destruct_3 ?????????? H);
 991  nrewrite > (anystatus_destruct_4 ?????????? H);
 992  nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
 993  nchange with ((forall_memory_ranged ?????? ⊗ true) =true);
 994  nrewrite > (symmetric_andbool (forall_memory_ranged t y3 y3 y2 y2 addrl) true);
 995  nchange with (forall_memory_ranged ?????? = true);
 996  napply (list_ind word16 ??? addrl);
 997  ##[ ##1,3,5,7: nnormalize; napply (refl_eq ??)
 998  ##| ##2,4,6,8: #a; #l'; #H;
 999           nchange with (
1000           ((eq_option byte8 (mem_read t y2 y3 a)
1001                             (mem_read t y2 y3 a) eq_b8) ⊗
1002            (forall_memory_ranged t y3 y3 y2 y2 l')) = true);
1003           nrewrite > H;
1004           nrewrite > (eq_to_eqoption ? (mem_read t y2 y3 a) (mem_read t y2 y3 a) eq_b8 eq_to_eqb8 (refl_eq ??));
1005           nnormalize;
1006           napply (refl_eq ??)
1007  ##]
1008 nqed.
1009
1010 nlemma eq_to_eqstatus_weak :
1011 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1012  (alu m t s1 = alu m t s2) →
1013  (clk_desc m t s1 = clk_desc m t s2) →
1014  ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
1015                             (mem_desc m t s1) (mem_desc m t s2) addrl) = true) →
1016  (eq_status m t s1 s2 addrl = true).
1017  #addrl; #m; #t;
1018  ncases m;
1019  ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
1020           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1021           nchange with (((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1022           nchange in H:(%) with (x1 = y1);
1023           nrewrite > H;
1024           nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq ??))
1025  ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4;
1026           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1027           nchange with (((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1028           nchange in H:(%) with (x1 = y1);
1029           nrewrite > H;
1030           nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq ??))
1031  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
1032           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1033           nchange with (((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1034           nchange in H:(%) with (x1 = y1);
1035           nrewrite > H;
1036           nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
1037  ##]
1038  nchange in H2:(%) with (forall_memory_ranged t x3 y3 x2 y2 addrl = true);
1039  nrewrite > H2;
1040  nchange in H1:(%) with (x4 = y4);
1041  nrewrite > H1;
1042  nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
1043  nnormalize;
1044  napply (refl_eq ??).
1045 nqed.