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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/word16_lemmas.ma".
  28 include "freescale/opcode_base_lemmas1.ma".
  29 include "freescale/status.ma".
  30 include "freescale/option_lemmas.ma".
  31 include "freescale/prod_lemmas.ma".
  32
  33 (* *********************************** *)
  34 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  35 (* *********************************** *)
  36
  37 nlemma aluHC05_destruct_1 :
  38 ∀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.
  39  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 →
  40  x1 = y1.
  41  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  42  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  43  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  44                 with [ mk_alu_HC05 a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  45  nrewrite < H;
  46  nnormalize;
  47  napply (refl_eq ??).
  48 nqed.
  49
  50 nlemma aluHC05_destruct_2 :
  51 ∀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.
  52  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 →
  53  x2 = y2.
  54  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  55  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  56  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  57                 with [ mk_alu_HC05 _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  58  nrewrite < H;
  59  nnormalize;
  60  napply (refl_eq ??).
  61 nqed.
  62
  63 nlemma aluHC05_destruct_3 :
  64 ∀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.
  65  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 →
  66  x3 = y3.
  67  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  68  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  69  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  70                 with [ mk_alu_HC05 _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  71  nrewrite < H;
  72  nnormalize;
  73  napply (refl_eq ??).
  74 nqed.
  75
  76 nlemma aluHC05_destruct_4 :
  77 ∀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.
  78  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 →
  79  x4 = y4.
  80  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  81  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  82  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  83                 with [ mk_alu_HC05 _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  84  nrewrite < H;
  85  nnormalize;
  86  napply (refl_eq ??).
  87 nqed.
  88
  89 nlemma aluHC05_destruct_5 :
  90 ∀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.
  91  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 →
  92  x5 = y5.
  93  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  94  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  95  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  96                 with [ mk_alu_HC05 _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
  97  nrewrite < H;
  98  nnormalize;
  99  napply (refl_eq ??).
 100 nqed.
 101
 102 nlemma aluHC05_destruct_6 :
 103 ∀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.
 104  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 →
 105  x6 = y6.
 106  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 107  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 108  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 109                 with [ mk_alu_HC05 _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x6 = a ]);
 110  nrewrite < H;
 111  nnormalize;
 112  napply (refl_eq ??).
 113 nqed.
 114
 115 nlemma aluHC05_destruct_7 :
 116 ∀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.
 117  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 →
 118  x7 = y7.
 119  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 120  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 121  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 122                 with [ mk_alu_HC05 _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x7 = a ]);
 123  nrewrite < H;
 124  nnormalize;
 125  napply (refl_eq ??).
 126 nqed.
 127
 128 nlemma aluHC05_destruct_8 :
 129 ∀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.
 130  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 →
 131  x8 = y8.
 132  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 133  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 134  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 135                 with [ mk_alu_HC05 _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x8 = a ]);
 136  nrewrite < H;
 137  nnormalize;
 138  napply (refl_eq ??).
 139 nqed.
 140
 141 nlemma aluHC05_destruct_9 :
 142 ∀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.
 143  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 →
 144  x9 = y9.
 145  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 146  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 147  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 148                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x9 = a ]);
 149  nrewrite < H;
 150  nnormalize;
 151  napply (refl_eq ??).
 152 nqed.
 153
 154 nlemma aluHC05_destruct_10 :
 155 ∀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.
 156  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 →
 157  x10 = y10.
 158  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 159  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 160  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 161                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x10 = a ]);
 162  nrewrite < H;
 163  nnormalize;
 164  napply (refl_eq ??).
 165 nqed.
 166
 167 nlemma aluHC05_destruct_11 :
 168 ∀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.
 169  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 →
 170  x11 = y11.
 171  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 172  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 173  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 174                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x11 = a ]);
 175  nrewrite < H;
 176  nnormalize;
 177  napply (refl_eq ??).
 178 nqed.
 179
 180 nlemma aluHC05_destruct_12 :
 181 ∀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.
 182  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 →
 183  x12 = y12.
 184  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 185  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 186  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 187                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x12 = a ]);
 188  nrewrite < H;
 189  nnormalize;
 190  napply (refl_eq ??).
 191 nqed.
 192
 193 nlemma aluHC05_destruct_13 :
 194 ∀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.
 195  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 →
 196  x13 = y13.
 197  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 198  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 199  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 200                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x13 = a ]);
 201  nrewrite < H;
 202  nnormalize;
 203  napply (refl_eq ??).
 204 nqed.
 205
 206 nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_alu_HC05.
 207  #alu1; #alu2;
 208  ncases alu1;
 209  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 210  ncases alu2;
 211  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 212  nchange with (
 213   ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 214   (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗  (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
 215   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗  (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
 216   (eq_bool x13 y13)) = ((eq_b8 y1 x1) ⊗  (eq_b8 y2 x2) ⊗ (eq_w16 y3 x3) ⊗
 217   (eq_w16 y4 x4) ⊗ (eq_w16 y5 x5) ⊗  (eq_w16 y6 x6) ⊗ (eq_w16 y7 x7) ⊗
 218   (eq_bool y8 x8) ⊗ (eq_bool y9 x9) ⊗  (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗
 219   (eq_bool y12 x12) ⊗ (eq_bool y13 x13)));
 220  nrewrite > (symmetric_eqb8 x1 y1);
 221  nrewrite > (symmetric_eqb8 x2 y2);
 222  nrewrite > (symmetric_eqw16 x3 y3);
 223  nrewrite > (symmetric_eqw16 x4 y4);
 224  nrewrite > (symmetric_eqw16 x5 y5);
 225  nrewrite > (symmetric_eqw16 x6 y6);
 226  nrewrite > (symmetric_eqw16 x7 y7);
 227  nrewrite > (symmetric_eqbool x8 y8);
 228  nrewrite > (symmetric_eqbool x9 y9);
 229  nrewrite > (symmetric_eqbool x10 y10);
 230  nrewrite > (symmetric_eqbool x11 y11);
 231  nrewrite > (symmetric_eqbool x12 y12);
 232  nrewrite > (symmetric_eqbool x13 y13);
 233  napply (refl_eq ??).
 234 nqed.
 235
 236 nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_alu_HC05 alu1 alu2 = true → alu1 = alu2.
 237  #alu1; #alu2;
 238  ncases alu1;
 239  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 240  ncases alu2;
 241  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 242  nchange in H:(%) with (
 243  ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗
 244   (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 245   (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗
 246   (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
 247   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗
 248   (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
 249   (eq_bool x13 y13)) = true);
 250  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
 251  nletin H1 ≝ (andb_true_true_l ?? H);
 252  nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r ?? (andb_true_true_l ?? H)));
 253  nletin H2 ≝ (andb_true_true_l ?? H1);
 254  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
 255  nletin H3 ≝ (andb_true_true_l ?? H2);
 256  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
 257  nletin H4 ≝ (andb_true_true_l ?? H3);
 258  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
 259  nletin H5 ≝ (andb_true_true_l ?? H4);
 260  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
 261  nletin H6 ≝ (andb_true_true_l ?? H5);
 262  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
 263  nletin H7 ≝ (andb_true_true_l ?? H6);
 264  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
 265  nletin H8 ≝ (andb_true_true_l ?? H7);
 266  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
 267  nletin H9 ≝ (andb_true_true_l ?? H8);
 268  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H9));
 269  nletin H10 ≝ (andb_true_true_l ?? H9);
 270  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H10));
 271  nletin H11 ≝ (andb_true_true_l ?? H10);
 272  nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H11));
 273  nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H11));
 274  napply (refl_eq ??).
 275 nqed.
 276
 277 nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC05 alu1 alu2 = true.
 278  #alu1; #alu2;
 279  ncases alu1;
 280  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 281  ncases alu2;
 282  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 283  nrewrite > (aluHC05_destruct_1 ?????????????????????????? H);
 284  nrewrite > (aluHC05_destruct_2 ?????????????????????????? H);
 285  nrewrite > (aluHC05_destruct_3 ?????????????????????????? H);
 286  nrewrite > (aluHC05_destruct_4 ?????????????????????????? H);
 287  nrewrite > (aluHC05_destruct_5 ?????????????????????????? H);
 288  nrewrite > (aluHC05_destruct_6 ?????????????????????????? H);
 289  nrewrite > (aluHC05_destruct_7 ?????????????????????????? H);
 290  nrewrite > (aluHC05_destruct_8 ?????????????????????????? H);
 291  nrewrite > (aluHC05_destruct_9 ?????????????????????????? H);
 292  nrewrite > (aluHC05_destruct_10 ?????????????????????????? H);
 293  nrewrite > (aluHC05_destruct_11 ?????????????????????????? H);
 294  nrewrite > (aluHC05_destruct_12 ?????????????????????????? H);
 295  nrewrite > (aluHC05_destruct_13 ?????????????????????????? H);
 296  nchange with (
 297  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗
 298   (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 299   (eq_w16 y5 y5) ⊗ (eq_w16 y6 y6) ⊗
 300   (eq_w16 y7 y7) ⊗ (eq_bool y8 y8) ⊗
 301   (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗
 302   (eq_bool y11 y11) ⊗ (eq_bool y12 y12) ⊗
 303   (eq_bool y13 y13)) = true);
 304  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
 305  nrewrite > (eq_to_eqb8 y2 y2 (refl_eq ??));
 306  nrewrite > (eq_to_eqw16 y3 y3 (refl_eq ??));
 307  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
 308  nrewrite > (eq_to_eqw16 y5 y5 (refl_eq ??));
 309  nrewrite > (eq_to_eqw16 y6 y6 (refl_eq ??));
 310  nrewrite > (eq_to_eqw16 y7 y7 (refl_eq ??));
 311  nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
 312  nrewrite > (eq_to_eqbool y9 y9 (refl_eq ??));
 313  nrewrite > (eq_to_eqbool y10 y10 (refl_eq ??));
 314  nrewrite > (eq_to_eqbool y11 y11 (refl_eq ??));
 315  nrewrite > (eq_to_eqbool y12 y12 (refl_eq ??));
 316  nrewrite > (eq_to_eqbool y13 y13 (refl_eq ??));
 317  napply (refl_eq ??).
 318 nqed.
 319
 320 nlemma aluHC08_destruct_1 :
 321 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 322  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 →
 323  x1 = y1.
 324  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 325  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 326  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 327                 with [ mk_alu_HC08 a _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
 328  nrewrite < H;
 329  nnormalize;
 330  napply (refl_eq ??).
 331 nqed.
 332
 333 nlemma aluHC08_destruct_2 :
 334 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 335  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 →
 336  x2 = y2.
 337  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 338  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 339  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 340                 with [ mk_alu_HC08 _ a _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
 341  nrewrite < H;
 342  nnormalize;
 343  napply (refl_eq ??).
 344 nqed.
 345
 346 nlemma aluHC08_destruct_3 :
 347 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 348  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 →
 349  x3 = y3.
 350  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 351  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 352  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 353                 with [ mk_alu_HC08 _ _ a _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
 354  nrewrite < H;
 355  nnormalize;
 356  napply (refl_eq ??).
 357 nqed.
 358
 359 nlemma aluHC08_destruct_4 :
 360 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 361  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 →
 362  x4 = y4.
 363  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 364  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 365  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 366                 with [ mk_alu_HC08 _ _ _ a _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
 367  nrewrite < H;
 368  nnormalize;
 369  napply (refl_eq ??).
 370 nqed.
 371
 372 nlemma aluHC08_destruct_5 :
 373 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 374  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 →
 375  x5 = y5.
 376  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 377  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 378  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 379                 with [ mk_alu_HC08 _ _ _ _ a _ _ _ _ _ _ _ ⇒ x5 = a ]);
 380  nrewrite < H;
 381  nnormalize;
 382  napply (refl_eq ??).
 383 nqed.
 384
 385 nlemma aluHC08_destruct_6 :
 386 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 387  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 →
 388  x6 = y6.
 389  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 390  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 391  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 392                 with [ mk_alu_HC08 _ _ _ _ _ a _ _ _ _ _ _ ⇒ x6 = a ]);
 393  nrewrite < H;
 394  nnormalize;
 395  napply (refl_eq ??).
 396 nqed.
 397
 398 nlemma aluHC08_destruct_7 :
 399 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 400  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 →
 401  x7 = y7.
 402  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 403  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 404  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 405                 with [ mk_alu_HC08 _ _ _ _ _ _ a _ _ _ _ _ ⇒ x7 = a ]);
 406  nrewrite < H;
 407  nnormalize;
 408  napply (refl_eq ??).
 409 nqed.
 410
 411 nlemma aluHC08_destruct_8 :
 412 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 413  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 →
 414  x8 = y8.
 415  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 416  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 417  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 418                 with [ mk_alu_HC08 _ _ _ _ _ _ _ a _ _ _ _ ⇒ x8 = a ]);
 419  nrewrite < H;
 420  nnormalize;
 421  napply (refl_eq ??).
 422 nqed.
 423
 424 nlemma aluHC08_destruct_9 :
 425 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 426  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 →
 427  x9 = y9.
 428  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 429  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 430  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 431                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ a _ _ _ ⇒ x9 = a ]);
 432  nrewrite < H;
 433  nnormalize;
 434  napply (refl_eq ??).
 435 nqed.
 436
 437 nlemma aluHC08_destruct_10 :
 438 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 439  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 →
 440  x10 = y10.
 441  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 442  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 443  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 444                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ a _ _ ⇒ x10 = a ]);
 445  nrewrite < H;
 446  nnormalize;
 447  napply (refl_eq ??).
 448 nqed.
 449
 450 nlemma aluHC08_destruct_11 :
 451 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 452  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 →
 453  x11 = y11.
 454  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 455  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 456  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 457                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ a _ ⇒ x11 = a ]);
 458  nrewrite < H;
 459  nnormalize;
 460  napply (refl_eq ??).
 461 nqed.
 462
 463 nlemma aluHC08_destruct_12 :
 464 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 465  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 →
 466  x12 = y12.
 467  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 468  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 469  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 470                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ a ⇒ x12 = a ]);
 471  nrewrite < H;
 472  nnormalize;
 473  napply (refl_eq ??).
 474 nqed.
 475
 476 nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_alu_HC08.
 477  #alu1; #alu2;
 478  ncases alu1;
 479  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 480  ncases alu2;
 481  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 482  nchange with (
 483   ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 484    (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
 485    (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) =
 486    ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_b8 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
 487    (eq_w16 y5 x5) ⊗ (eq_bool y6 x6) ⊗ (eq_bool y7 x7) ⊗ (eq_bool y8 x8) ⊗
 488    (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗ (eq_bool y12 x12)));
 489  nrewrite > (symmetric_eqb8 x1 y1);
 490  nrewrite > (symmetric_eqb8 x2 y2);
 491  nrewrite > (symmetric_eqb8 x3 y3);
 492  nrewrite > (symmetric_eqw16 x4 y4);
 493  nrewrite > (symmetric_eqw16 x5 y5);
 494  nrewrite > (symmetric_eqbool x6 y6);
 495  nrewrite > (symmetric_eqbool x7 y7);
 496  nrewrite > (symmetric_eqbool x8 y8);
 497  nrewrite > (symmetric_eqbool x9 y9);
 498  nrewrite > (symmetric_eqbool x10 y10);
 499  nrewrite > (symmetric_eqbool x11 y11);
 500  nrewrite > (symmetric_eqbool x12 y12);
 501  napply (refl_eq ??).
 502 nqed.
 503
 504 nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_alu_HC08 alu1 alu2 = true → alu1 = alu2.
 505  #alu1; #alu2;
 506  ncases alu1;
 507  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 508  ncases alu2;
 509  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 510  nchange in H:(%) with (
 511  ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 512   (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
 513   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) = true);
 514  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
 515  nletin H1 ≝ (andb_true_true_l ?? H);
 516  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
 517  nletin H2 ≝ (andb_true_true_l ?? H1);
 518  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H2));
 519  nletin H3 ≝ (andb_true_true_l ?? H2);
 520  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H3));
 521  nletin H4 ≝ (andb_true_true_l ?? H3);
 522  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H4));
 523  nletin H5 ≝ (andb_true_true_l ?? H4);
 524  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H5));
 525  nletin H6 ≝ (andb_true_true_l ?? H5);
 526  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H6));
 527  nletin H7 ≝ (andb_true_true_l ?? H6);
 528  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H7));
 529  nletin H8 ≝ (andb_true_true_l ?? H7);
 530  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H8));
 531  nletin H9 ≝ (andb_true_true_l ?? H8);
 532  nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H9));
 533  nletin H10 ≝ (andb_true_true_l ?? H9);
 534  nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H10));
 535  nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H10));
 536  napply (refl_eq ??).
 537 nqed.
 538
 539 nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_HC08 alu1 alu2 = true.
 540  #alu1; #alu2;
 541  ncases alu1;
 542  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 543  ncases alu2;
 544  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 545  nrewrite > (aluHC08_destruct_1 ???????????????????????? H);
 546  nrewrite > (aluHC08_destruct_2 ???????????????????????? H);
 547  nrewrite > (aluHC08_destruct_3 ???????????????????????? H);
 548  nrewrite > (aluHC08_destruct_4 ???????????????????????? H);
 549  nrewrite > (aluHC08_destruct_5 ???????????????????????? H);
 550  nrewrite > (aluHC08_destruct_6 ???????????????????????? H);
 551  nrewrite > (aluHC08_destruct_7 ???????????????????????? H);
 552  nrewrite > (aluHC08_destruct_8 ???????????????????????? H);
 553  nrewrite > (aluHC08_destruct_9 ???????????????????????? H);
 554  nrewrite > (aluHC08_destruct_10 ???????????????????????? H);
 555  nrewrite > (aluHC08_destruct_11 ???????????????????????? H);
 556  nrewrite > (aluHC08_destruct_12 ???????????????????????? H);
 557  nchange with (
 558  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 559   (eq_w16 y5 y5) ⊗ (eq_bool y6 y6) ⊗ (eq_bool y7 y7) ⊗ (eq_bool y8 y8) ⊗
 560   (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗ (eq_bool y11 y11) ⊗ (eq_bool y12 y12)) = true);
 561  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
 562  nrewrite > (eq_to_eqb8 y2 y2 (refl_eq ??));
 563  nrewrite > (eq_to_eqb8 y3 y3 (refl_eq ??));
 564  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
 565  nrewrite > (eq_to_eqw16 y5 y5 (refl_eq ??));
 566  nrewrite > (eq_to_eqbool y6 y6 (refl_eq ??));
 567  nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
 568  nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
 569  nrewrite > (eq_to_eqbool y9 y9 (refl_eq ??));
 570  nrewrite > (eq_to_eqbool y10 y10 (refl_eq ??));
 571  nrewrite > (eq_to_eqbool y11 y11 (refl_eq ??));
 572  nrewrite > (eq_to_eqbool y12 y12 (refl_eq ??));
 573  napply (refl_eq ??).
 574 nqed.
 575
 576 nlemma aluRS08_destruct_1 :
 577 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 578  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 579  x1 = y1.
 580  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 581  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 582  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 583                 with [ mk_alu_RS08 a _ _ _ _ _ _ _ ⇒ x1 = a ]);
 584  nrewrite < H;
 585  nnormalize;
 586  napply (refl_eq ??).
 587 nqed.
 588
 589 nlemma aluRS08_destruct_2 :
 590 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 591  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 592  x2 = y2.
 593  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 594  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 595  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 596                 with [ mk_alu_RS08 _ a _ _ _ _ _ _ ⇒ x2 = a ]);
 597  nrewrite < H;
 598  nnormalize;
 599  napply (refl_eq ??).
 600 nqed.
 601
 602 nlemma aluRS08_destruct_3 :
 603 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 604  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 605  x3 = y3.
 606  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 607  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 608  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 609                 with [ mk_alu_RS08 _ _ a _ _ _ _ _ ⇒ x3 = a ]);
 610  nrewrite < H;
 611  nnormalize;
 612  napply (refl_eq ??).
 613 nqed.
 614
 615 nlemma aluRS08_destruct_4 :
 616 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 617  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 618  x4 = y4.
 619  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 620  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 621  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 622                 with [ mk_alu_RS08 _ _ _ a _ _ _ _ ⇒ x4 = a ]);
 623  nrewrite < H;
 624  nnormalize;
 625  napply (refl_eq ??).
 626 nqed.
 627
 628 nlemma aluRS08_destruct_5 :
 629 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 630  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 631  x5 = y5.
 632  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 633  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 634  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 635                 with [ mk_alu_RS08 _ _ _ _ a _ _ _ ⇒ x5 = a ]);
 636  nrewrite < H;
 637  nnormalize;
 638  napply (refl_eq ??).
 639 nqed.
 640
 641 nlemma aluRS08_destruct_6 :
 642 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 643  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 644  x6 = y6.
 645  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 646  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 647  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 648                 with [ mk_alu_RS08 _ _ _ _ _ a _ _ ⇒ x6 = a ]);
 649  nrewrite < H;
 650  nnormalize;
 651  napply (refl_eq ??).
 652 nqed.
 653
 654 nlemma aluRS08_destruct_7 :
 655 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 656  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 657  x7 = y7.
 658  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 659  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 660  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 661                 with [ mk_alu_RS08 _ _ _ _ _ _ a _ ⇒ x7 = a ]);
 662  nrewrite < H;
 663  nnormalize;
 664  napply (refl_eq ??).
 665 nqed.
 666
 667 nlemma aluRS08_destruct_8 :
 668 ∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8.
 669  mk_alu_RS08 x1 x2 x3 x4 x5 x6 x7 x8 = mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8 →
 670  x8 = y8.
 671  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 672  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 673  nchange with (match mk_alu_RS08 y1 y2 y3 y4 y5 y6 y7 y8
 674                 with [ mk_alu_RS08 _ _ _ _ _ _ _ a ⇒ x8 = a ]);
 675  nrewrite < H;
 676  nnormalize;
 677  napply (refl_eq ??).
 678 nqed.
 679
 680 nlemma symmetric_eqaluRS08 : symmetricT alu_RS08 bool eq_alu_RS08.
 681  #alu1; #alu2;
 682  ncases alu1;
 683  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 684  ncases alu2;
 685  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 686  nchange with (
 687   ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
 688    (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 689    (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
 690    (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) =
 691   ((eq_b8 y1 x1) ⊗ (eq_w16 y2 x2) ⊗
 692    (eq_w16 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
 693    (eq_b8 y5 x5) ⊗ (eq_b8 y6 x6) ⊗
 694    (eq_bool y7 x7) ⊗ (eq_bool y8 x8)));
 695  nrewrite > (symmetric_eqb8 x1 y1);
 696  nrewrite > (symmetric_eqw16 x2 y2);
 697  nrewrite > (symmetric_eqw16 x3 y3);
 698  nrewrite > (symmetric_eqw16 x4 y4);
 699  nrewrite > (symmetric_eqb8 x5 y5);
 700  nrewrite > (symmetric_eqb8 x6 y6);
 701  nrewrite > (symmetric_eqbool x7 y7);
 702  nrewrite > (symmetric_eqbool x8 y8);
 703  napply (refl_eq ??).
 704 nqed.
 705
 706 nlemma eqaluRS08_to_eq : ∀alu1,alu2.eq_alu_RS08 alu1 alu2 = true → alu1 = alu2.
 707  #alu1; #alu2;
 708  ncases alu1;
 709  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 710  ncases alu2;
 711  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 712  nchange in H:(%) with (
 713   ((eq_b8 x1 y1) ⊗ (eq_w16 x2 y2) ⊗
 714    (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 715    (eq_b8 x5 y5) ⊗ (eq_b8 x6 y6) ⊗
 716    (eq_bool x7 y7) ⊗ (eq_bool x8 y8)) = true);
 717  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H));
 718  nletin H1 ≝ (andb_true_true_l ?? H);
 719  nrewrite > (eqbool_to_eq ?? (andb_true_true_r ?? H1));
 720  nletin H2 ≝ (andb_true_true_l ?? H1);
 721  nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H2));
 722  nletin H3 ≝ (andb_true_true_l ?? H2);
 723  nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H3));
 724  nletin H4 ≝ (andb_true_true_l ?? H3);
 725  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H4));
 726  nletin H5 ≝ (andb_true_true_l ?? H4);
 727  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H5));
 728  nletin H6 ≝ (andb_true_true_l ?? H5);
 729  nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H6));
 730  nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H6));
 731  napply (refl_eq ??).
 732 nqed.
 733
 734 nlemma eq_to_eqaluRS08 : ∀alu1,alu2.alu1 = alu2 → eq_alu_RS08 alu1 alu2 = true.
 735  #alu1; #alu2;
 736  ncases alu1;
 737  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 738  ncases alu2;
 739  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 740  nrewrite > (aluRS08_destruct_1 ???????????????? H);
 741  nrewrite > (aluRS08_destruct_2 ???????????????? H);
 742  nrewrite > (aluRS08_destruct_3 ???????????????? H);
 743  nrewrite > (aluRS08_destruct_4 ???????????????? H);
 744  nrewrite > (aluRS08_destruct_5 ???????????????? H);
 745  nrewrite > (aluRS08_destruct_6 ???????????????? H);
 746  nrewrite > (aluRS08_destruct_7 ???????????????? H);
 747  nrewrite > (aluRS08_destruct_8 ???????????????? H);
 748  nchange with (
 749   ((eq_b8 y1 y1) ⊗ (eq_w16 y2 y2) ⊗
 750    (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 751    (eq_b8 y5 y5) ⊗ (eq_b8 y6 y6) ⊗
 752    (eq_bool y7 y7) ⊗ (eq_bool y8 y8)) = true);
 753  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq ??));
 754  nrewrite > (eq_to_eqw16 y2 y2 (refl_eq ??));
 755  nrewrite > (eq_to_eqw16 y3 y3 (refl_eq ??));
 756  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq ??));
 757  nrewrite > (eq_to_eqb8 y5 y5 (refl_eq ??));
 758  nrewrite > (eq_to_eqb8 y6 y6 (refl_eq ??));
 759  nrewrite > (eq_to_eqbool y7 y7 (refl_eq ??));
 760  nrewrite > (eq_to_eqbool y8 y8 (refl_eq ??));
 761  napply (refl_eq ??).
 762 nqed.
 763
 764 nlemma symmetric_eqclk : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = eq_clk mcu clk2 clk1.
 765  #mcu; #clk1; #clk2;
 766  ncases clk1;
 767  ncases clk2;
 768  ##[ ##1: napply (refl_eq ??)
 769  ##| ##2,3: nnormalize; #H; napply (refl_eq ??)
 770  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
 771           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5;
 772           nchange with (
 773            ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) =
 774            ((eq_b8 x1 y1) ⊗ (eq_anyop ? x2 y2) ⊗ (eq_instrmode x3 y3) ⊗ (eq_b8 x4 y4) ⊗ (eq_w16 x5 y5)));
 775           nrewrite > (symmetric_eqb8 x1 y1);
 776           nrewrite > (symmetric_eqanyop ? x2 y2);
 777           nrewrite > (symmetric_eqinstrmode x3 y3);
 778           nrewrite > (symmetric_eqb8 x4 y4);
 779           nrewrite > (symmetric_eqw16 x5 y5);
 780           napply (refl_eq ??)
 781  ##]
 782 nqed.
 783
 784 nlemma eqclk_to_eq : ∀mcu,clk1,clk2.eq_clk mcu clk1 clk2 = true → clk1 = clk2.
 785  #mcu; #clk1; #clk2;
 786  ncases clk1;
 787  ncases clk2;
 788  ##[ ##1: nnormalize; #H; napply (refl_eq ??)
 789  ##| ##2,3: nnormalize; #H; #H1; napply (bool_destruct ??? H1)
 790  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
 791           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
 792           nchange in H:(%) with (
 793            ((eq_b8 y1 x1) ⊗ (eq_anyop ? y2 x2) ⊗ (eq_instrmode y3 x3) ⊗ (eq_b8 y4 x4) ⊗ (eq_w16 y5 x5)) = true);
 794            nrewrite > (eqw16_to_eq ?? (andb_true_true_r ?? H));
 795            nletin H1 ≝ (andb_true_true_l ?? H);
 796            nrewrite > (eqb8_to_eq ?? (andb_true_true_r ?? H1));
 797            nletin H2 ≝ (andb_true_true_l ?? H1);
 798            nrewrite > (eqinstrmode_to_eq ?? (andb_true_true_r ?? H2));
 799            nletin H3 ≝ (andb_true_true_l ?? H2);
 800            nrewrite > (eqanyop_to_eq ??? (andb_true_true_r ?? H3));
 801            nrewrite > (eqb8_to_eq ?? (andb_true_true_l ?? H3));
 802            napply (refl_eq ??)
 803  ##]
 804 nqed.
 805
 806 nlemma eq_to_eqclk : ∀mcu,clk1,clk2.clk1 = clk2 → eq_clk mcu clk1 clk2 = true.
 807  #mcu; #clk1; #clk2;
 808  ncases clk1;
 809  ncases clk2;
 810  ##[ ##1: nnormalize; #H; napply (refl_eq ??)
 811  ##| ##2: nnormalize; #p; #H1; nelim (option_destruct_none_some ?? H1)
 812  ##| ##3: nnormalize; #p; #H1; nelim (option_destruct_some_none ?? H1)
 813  ##| ##4: #p1; ncases p1; #x1; #x2; #x3; #x4; #x5;
 814           #p2; ncases p2; #y1; #y2; #y3; #y4; #y5; #H;
 815           nrewrite > (quintuple_destruct_1 ??????????????? (option_destruct_some_some ??? H));
 816           nrewrite > (quintuple_destruct_2 ??????????????? (option_destruct_some_some ??? H));
 817           nrewrite > (quintuple_destruct_3 ??????????????? (option_destruct_some_some ??? H));
 818           nrewrite > (quintuple_destruct_4 ??????????????? (option_destruct_some_some ??? H));
 819           nrewrite > (quintuple_destruct_5 ??????????????? (option_destruct_some_some ??? H));
 820           nchange with (
 821            ((eq_b8 x1 x1) ⊗ (eq_anyop ? x2 x2) ⊗ (eq_instrmode x3 x3) ⊗ (eq_b8 x4 x4) ⊗ (eq_w16 x5 x5)) = true);
 822           nrewrite > (eq_to_eqb8 x1 x1 (refl_eq ??));
 823           nrewrite > (eq_to_eqanyop mcu x2 x2 (refl_eq ? x2));
 824           nrewrite > (eq_to_eqinstrmode x3 x3 (refl_eq ??));
 825           nrewrite > (eq_to_eqb8 x4 x4 (refl_eq ??));
 826           nrewrite > (eq_to_eqw16 x5 x5 (refl_eq ??));
 827           nnormalize;
 828           napply (refl_eq ??)
 829  ##]
 830 nqed.
 831
 832 nlemma symmetric_forallmemoryranged :
 833 ∀t.∀chk1,chk2:aux_chk_type t.∀mem1,mem2:aux_mem_type t.∀addrl.
 834  forall_memory_ranged t chk1 chk2 mem1 mem2 addrl =
 835  forall_memory_ranged t chk2 chk1 mem2 mem1 addrl.
 836  #t; #chk1; #chk2; #mem1; #mem2; #addrl;
 837  napply (list_ind word16 ??? addrl);
 838  ##[ ##1: nnormalize; napply (refl_eq ??)
 839  ##| ##2: #a; #l; #H;
 840           nchange with (
 841            ((eq_option byte8 (mem_read t mem1 chk1 a)
 842                             (mem_read t mem2 chk2 a) eq_b8) ⊗
 843            (forall_memory_ranged t chk1 chk2 mem1 mem2 l)) =
 844            ((eq_option byte8 (mem_read t mem2 chk2 a)
 845                             (mem_read t mem1 chk1 a) eq_b8) ⊗
 846            (forall_memory_ranged t chk2 chk1 mem2 mem1 l)));
 847            nrewrite > H;
 848            nrewrite > (symmetric_eqoption ? (mem_read t mem1 chk1 a) (mem_read t mem2 chk2 a) eq_b8 symmetric_eqb8);
 849            napply (refl_eq ??)
 850  ##]
 851 nqed.
 852
 853 nlemma anystatus_destruct_1 :
 854 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 855  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 856  x1 = y1.
 857  #m; #t;
 858  #x1; #x2; #x3; #x4;
 859  #y1; #y2; #y3; #y4; #H;
 860  nchange with (match mk_any_status m t y1 y2 y3 y4
 861                 with [ mk_any_status a _ _ _ ⇒ x1 = a ]);
 862  nrewrite < H;
 863  nnormalize;
 864  napply (refl_eq ??).
 865 nqed.
 866
 867 nlemma anystatus_destruct_2 :
 868 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 869  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 870  x2 = y2.
 871  #m; #t;
 872  #x1; #x2; #x3; #x4;
 873  #y1; #y2; #y3; #y4; #H;
 874  nchange with (match mk_any_status m t y1 y2 y3 y4
 875                 with [ mk_any_status _ a _ _ ⇒ x2 = a ]);
 876  nrewrite < H;
 877  nnormalize;
 878  napply (refl_eq ??).
 879 nqed.
 880
 881 nlemma anystatus_destruct_3 :
 882 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 883  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 884  x3 = y3.
 885  #m; #t;
 886  #x1; #x2; #x3; #x4;
 887  #y1; #y2; #y3; #y4; #H;
 888  nchange with (match mk_any_status m t y1 y2 y3 y4
 889                 with [ mk_any_status _ _ a _ ⇒ x3 = a ]);
 890  nrewrite < H;
 891  nnormalize;
 892  napply (refl_eq ??).
 893 nqed.
 894
 895 nlemma anystatus_destruct_4 :
 896 ∀m,t.∀x1,x2,x3,x4,y1,y2,y3,y4.
 897  mk_any_status m t x1 x2 x3 x4 = mk_any_status m t y1 y2 y3 y4 →
 898  x4 = y4.
 899  #m; #t;
 900  #x1; #x2; #x3; #x4;
 901  #y1; #y2; #y3; #y4; #H;
 902  nchange with (match mk_any_status m t y1 y2 y3 y4
 903                 with [ mk_any_status _ _ _ a ⇒ x4 = a ]);
 904  nrewrite < H;
 905  nnormalize;
 906  napply (refl_eq ??).
 907 nqed.
 908
 909 nlemma symmetric_eqstatus :
 910 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 911  eq_status m t s1 s2 addrl = eq_status m t s2 s1 addrl.
 912  #addrl; #m;
 913  ncases m; #t; #s1;
 914  ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
 915           #s2; ncases s2; #y1; #y2; #y3; #y4;
 916           nchange with (
 917            ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk HC05 x4 y4)) =
 918            ((eq_alu_HC05 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk HC05 y4 x4)));
 919            nrewrite > (symmetric_eqaluHC05 x1 y1)
 920  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
 921           #s2; ncases s2; #y1; #y2; #y3; #y4;
 922           nchange with (
 923            ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) =
 924            ((eq_alu_HC08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk ? y4 x4)));
 925            nrewrite > (symmetric_eqaluHC08 x1 y1)
 926  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
 927           #s2; ncases s2; #y1; #y2; #y3; #y4;
 928           nchange with (
 929            ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk RS08 x4 y4)) =
 930            ((eq_alu_RS08 y1 x1) ⊗ (forall_memory_ranged t y3 x3 y2 x2 addrl) ⊗ (eq_clk RS08 y4 x4)));
 931            nrewrite > (symmetric_eqaluRS08 x1 y1)
 932  ##]
 933  nrewrite > (symmetric_forallmemoryranged t x3 y3 x2 y2 addrl);
 934  nrewrite > (symmetric_eqclk ? x4 y4);
 935  napply (refl_eq ??).
 936 nqed.
 937
 938 nlemma eqstatus_to_eq :
 939 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 940  (eq_status m t s1 s2 addrl = true) →
 941   ((alu m t s1 = alu m t s2) ∧
 942    (clk_desc m t s1 = clk_desc m t s2) ∧
 943    ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
 944                             (mem_desc m t s1) (mem_desc m t s2) addrl) = true)).
 945  #addrl; #m; #t;
 946  ncases m; #s1;
 947  ##[ ##1: ncases s1; #x1; #x2; #x3; #x4;
 948           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 949           nchange in H:(%) with (
 950            ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 951            nrewrite > (eqaluHC05_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
 952  ##| ##2,3: ncases s1; #x1; #x2; #x3; #x4;
 953           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 954           nchange in H:(%) with (
 955            ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 956            nrewrite > (eqaluHC08_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
 957  ##| ##4: ncases s1; #x1; #x2; #x3; #x4;
 958           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 959           nchange in H:(%) with (
 960            ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 961            nrewrite > (eqaluRS08_to_eq ?? (andb_true_true_l ?? (andb_true_true_l ?? H)))
 962  ##]
 963  nchange with ((y1 = y1) ∧ (x4 = y4) ∧ (forall_memory_ranged t x3 y3 x2 y2 addrl = true));
 964  nrewrite > (andb_true_true_r ?? (andb_true_true_l ?? H));
 965  nrewrite > (eqclk_to_eq ??? (andb_true_true_r ?? H));
 966  napply (conj ?? (conj ?? (refl_eq ??) (refl_eq ??)) (refl_eq ??)).
 967 nqed.
 968
 969 nlemma eq_to_eqstatus_strong :
 970 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
 971  s1 = s2 → (eq_status m t s1 s2 addrl = true).
 972  #addrl; #m; #t;
 973  ncases m;
 974  ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
 975           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 976           nchange with (
 977            ((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 978           nrewrite > (anystatus_destruct_1 ?????????? H);
 979           nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq ??))
 980  ##| ##2,3:  #s1; ncases s1; #x1; #x2; #x3; #x4;
 981           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 982           nchange with (
 983            ((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 984           nrewrite > (anystatus_destruct_1 ?????????? H);
 985           nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq ??))
 986  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
 987           #s2; ncases s2; #y1; #y2; #y3; #y4; #H;
 988           nchange with (
 989            ((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
 990           nrewrite > (anystatus_destruct_1 ?????????? H);
 991           nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
 992  ##]
 993  nrewrite > (anystatus_destruct_2 ?????????? H);
 994  nrewrite > (anystatus_destruct_3 ?????????? H);
 995  nrewrite > (anystatus_destruct_4 ?????????? H);
 996  nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
 997  nchange with ((forall_memory_ranged ?????? ⊗ true) =true);
 998  nrewrite > (symmetric_andbool (forall_memory_ranged t y3 y3 y2 y2 addrl) true);
 999  nchange with (forall_memory_ranged ?????? = true);
1000  napply (list_ind word16 ??? addrl);
1001  ##[ ##1,3,5,7: nnormalize; napply (refl_eq ??)
1002  ##| ##2,4,6,8: #a; #l'; #H;
1003           nchange with (
1004           ((eq_option byte8 (mem_read t y2 y3 a)
1005                             (mem_read t y2 y3 a) eq_b8) ⊗
1006            (forall_memory_ranged t y3 y3 y2 y2 l')) = true);
1007           nrewrite > H;
1008           nrewrite > (eq_to_eqoption ? (mem_read t y2 y3 a) (mem_read t y2 y3 a) eq_b8 eq_to_eqb8 (refl_eq ??));
1009           nnormalize;
1010           napply (refl_eq ??)
1011  ##]
1012 nqed.
1013
1014 nlemma eq_to_eqstatus_weak :
1015 ∀addrl:list word16.∀m:mcu_type.∀t:memory_impl.∀s1,s2:any_status m t.
1016  (alu m t s1 = alu m t s2) →
1017  (clk_desc m t s1 = clk_desc m t s2) →
1018  ((forall_memory_ranged t (chk_desc m t s1) (chk_desc m t s2)
1019                             (mem_desc m t s1) (mem_desc m t s2) addrl) = true) →
1020  (eq_status m t s1 s2 addrl = true).
1021  #addrl; #m; #t;
1022  ncases m;
1023  ##[ ##1: #s1; ncases s1; #x1; #x2; #x3; #x4;
1024           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1025           nchange with (((eq_alu_HC05 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1026           nchange in H:(%) with (x1 = y1);
1027           nrewrite > H;
1028           nrewrite > (eq_to_eqaluHC05 y1 y1 (refl_eq ??))
1029  ##| ##2,3: #s1; ncases s1; #x1; #x2; #x3; #x4;
1030           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1031           nchange with (((eq_alu_HC08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1032           nchange in H:(%) with (x1 = y1);
1033           nrewrite > H;
1034           nrewrite > (eq_to_eqaluHC08 y1 y1 (refl_eq ??))
1035  ##| ##4: #s1; ncases s1; #x1; #x2; #x3; #x4;
1036           #s2; ncases s2; #y1; #y2; #y3; #y4; #H; #H1; #H2;
1037           nchange with (((eq_alu_RS08 x1 y1) ⊗ (forall_memory_ranged t x3 y3 x2 y2 addrl) ⊗ (eq_clk ? x4 y4)) = true);
1038           nchange in H:(%) with (x1 = y1);
1039           nrewrite > H;
1040           nrewrite > (eq_to_eqaluRS08 y1 y1 (refl_eq ??))
1041  ##]
1042  nchange in H2:(%) with (forall_memory_ranged t x3 y3 x2 y2 addrl = true);
1043  nrewrite > H2;
1044  nchange in H1:(%) with (x4 = y4);
1045  nrewrite > H1;
1046  nrewrite > (eq_to_eqclk ? y4 y4 (refl_eq ??));
1047  nnormalize;
1048  napply (refl_eq ??).
1049 nqed.