matita/matita/contribs/ng_assembly/emulator/status/HC05_status_lemmas.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* ********************************************************************** *)
  16 (*                          Progetto FreeScale                            *)
  17 (*                                                                        *)
  18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/word16_lemmas.ma".
  24 include "emulator/status/HC05_status.ma".
  25
  26 (* *********************************** *)
  27 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  28 (* *********************************** *)
  29
  30 nlemma aluHC05_destruct_1 :
  31 ∀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.
  32  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 →
  33  x1 = y1.
  34  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  35  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  36  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  37                 with [ mk_alu_HC05 a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  38  nrewrite < H;
  39  nnormalize;
  40  napply refl_eq.
  41 nqed.
  42
  43 nlemma aluHC05_destruct_2 :
  44 ∀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.
  45  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 →
  46  x2 = y2.
  47  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  48  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  49  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  50                 with [ mk_alu_HC05 _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  51  nrewrite < H;
  52  nnormalize;
  53  napply refl_eq.
  54 nqed.
  55
  56 nlemma aluHC05_destruct_3 :
  57 ∀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.
  58  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 →
  59  x3 = y3.
  60  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  61  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  62  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  63                 with [ mk_alu_HC05 _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  64  nrewrite < H;
  65  nnormalize;
  66  napply refl_eq.
  67 nqed.
  68
  69 nlemma aluHC05_destruct_4 :
  70 ∀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.
  71  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 →
  72  x4 = y4.
  73  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  74  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  75  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  76                 with [ mk_alu_HC05 _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  77  nrewrite < H;
  78  nnormalize;
  79  napply refl_eq.
  80 nqed.
  81
  82 nlemma aluHC05_destruct_5 :
  83 ∀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.
  84  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 →
  85  x5 = y5.
  86  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  87  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  88  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  89                 with [ mk_alu_HC05 _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
  90  nrewrite < H;
  91  nnormalize;
  92  napply refl_eq.
  93 nqed.
  94
  95 nlemma aluHC05_destruct_6 :
  96 ∀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.
  97  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 →
  98  x6 = y6.
  99  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 100  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 101  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 102                 with [ mk_alu_HC05 _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x6 = a ]);
 103  nrewrite < H;
 104  nnormalize;
 105  napply refl_eq.
 106 nqed.
 107
 108 nlemma aluHC05_destruct_7 :
 109 ∀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.
 110  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 →
 111  x7 = y7.
 112  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 113  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 114  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 115                 with [ mk_alu_HC05 _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x7 = a ]);
 116  nrewrite < H;
 117  nnormalize;
 118  napply refl_eq.
 119 nqed.
 120
 121 nlemma aluHC05_destruct_8 :
 122 ∀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.
 123  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 →
 124  x8 = y8.
 125  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 126  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 127  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 128                 with [ mk_alu_HC05 _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x8 = a ]);
 129  nrewrite < H;
 130  nnormalize;
 131  napply refl_eq.
 132 nqed.
 133
 134 nlemma aluHC05_destruct_9 :
 135 ∀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.
 136  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 →
 137  x9 = y9.
 138  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 139  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 140  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 141                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x9 = a ]);
 142  nrewrite < H;
 143  nnormalize;
 144  napply refl_eq.
 145 nqed.
 146
 147 nlemma aluHC05_destruct_10 :
 148 ∀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.
 149  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 →
 150  x10 = y10.
 151  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 152  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 153  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 154                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x10 = a ]);
 155  nrewrite < H;
 156  nnormalize;
 157  napply refl_eq.
 158 nqed.
 159
 160 nlemma aluHC05_destruct_11 :
 161 ∀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.
 162  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 →
 163  x11 = y11.
 164  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 165  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 166  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 167                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x11 = a ]);
 168  nrewrite < H;
 169  nnormalize;
 170  napply refl_eq.
 171 nqed.
 172
 173 nlemma aluHC05_destruct_12 :
 174 ∀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.
 175  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 →
 176  x12 = y12.
 177  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 178  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 179  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 180                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x12 = a ]);
 181  nrewrite < H;
 182  nnormalize;
 183  napply refl_eq.
 184 nqed.
 185
 186 nlemma aluHC05_destruct_13 :
 187 ∀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.
 188  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 →
 189  x13 = y13.
 190  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 191  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 192  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 193                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x13 = a ]);
 194  nrewrite < H;
 195  nnormalize;
 196  napply refl_eq.
 197 nqed.
 198
 199 nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_HC05_alu.
 200  #alu1; #alu2;
 201  ncases alu1;
 202  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 203  ncases alu2;
 204  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 205  nchange with (
 206   ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 207   (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗  (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
 208   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗  (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
 209   (eq_bool x13 y13)) = ((eq_b8 y1 x1) ⊗  (eq_b8 y2 x2) ⊗ (eq_w16 y3 x3) ⊗
 210   (eq_w16 y4 x4) ⊗ (eq_w16 y5 x5) ⊗  (eq_w16 y6 x6) ⊗ (eq_w16 y7 x7) ⊗
 211   (eq_bool y8 x8) ⊗ (eq_bool y9 x9) ⊗  (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗
 212   (eq_bool y12 x12) ⊗ (eq_bool y13 x13)));
 213  nrewrite > (symmetric_eqb8 x1 y1);
 214  nrewrite > (symmetric_eqb8 x2 y2);
 215  nrewrite > (symmetric_eqw16 x3 y3);
 216  nrewrite > (symmetric_eqw16 x4 y4);
 217  nrewrite > (symmetric_eqw16 x5 y5);
 218  nrewrite > (symmetric_eqw16 x6 y6);
 219  nrewrite > (symmetric_eqw16 x7 y7);
 220  nrewrite > (symmetric_eqbool x8 y8);
 221  nrewrite > (symmetric_eqbool x9 y9);
 222  nrewrite > (symmetric_eqbool x10 y10);
 223  nrewrite > (symmetric_eqbool x11 y11);
 224  nrewrite > (symmetric_eqbool x12 y12);
 225  nrewrite > (symmetric_eqbool x13 y13);
 226  napply refl_eq.
 227 nqed.
 228
 229 nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_HC05_alu alu1 alu2 = true → alu1 = alu2.
 230  #alu1; #alu2;
 231  ncases alu1;
 232  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 233  ncases alu2;
 234  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 235  nchange in H:(%) with (
 236  ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗
 237   (eq_w16 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 238   (eq_w16 x5 y5) ⊗ (eq_w16 x6 y6) ⊗
 239   (eq_w16 x7 y7) ⊗ (eq_bool x8 y8) ⊗
 240   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗
 241   (eq_bool x11 y11) ⊗ (eq_bool x12 y12) ⊗
 242   (eq_bool x13 y13)) = true);
 243  nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
 244  nletin H1 ≝ (andb_true_true_l … H);
 245  nrewrite > (eqbool_to_eq x12 y12 (andb_true_true_r … (andb_true_true_l … H)));
 246  nletin H2 ≝ (andb_true_true_l … H1);
 247  nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
 248  nletin H3 ≝ (andb_true_true_l … H2);
 249  nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
 250  nletin H4 ≝ (andb_true_true_l … H3);
 251  nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
 252  nletin H5 ≝ (andb_true_true_l … H4);
 253  nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
 254  nletin H6 ≝ (andb_true_true_l … H5);
 255  nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
 256  nletin H7 ≝ (andb_true_true_l … H6);
 257  nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
 258  nletin H8 ≝ (andb_true_true_l … H7);
 259  nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
 260  nletin H9 ≝ (andb_true_true_l … H8);
 261  nrewrite > (eqw16_to_eq … (andb_true_true_r … H9));
 262  nletin H10 ≝ (andb_true_true_l … H9);
 263  nrewrite > (eqw16_to_eq … (andb_true_true_r … H10));
 264  nletin H11 ≝ (andb_true_true_l … H10);
 265  nrewrite > (eqb8_to_eq … (andb_true_true_r … H11));
 266  nrewrite > (eqb8_to_eq … (andb_true_true_l … H11));
 267  napply refl_eq.
 268 nqed.
 269
 270 nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_HC05_alu alu1 alu2 = true.
 271  #alu1; #alu2;
 272  ncases alu1;
 273  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 274  ncases alu2;
 275  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 276  nrewrite > (aluHC05_destruct_1 … H);
 277  nrewrite > (aluHC05_destruct_2 … H);
 278  nrewrite > (aluHC05_destruct_3 … H);
 279  nrewrite > (aluHC05_destruct_4 … H);
 280  nrewrite > (aluHC05_destruct_5 … H);
 281  nrewrite > (aluHC05_destruct_6 … H);
 282  nrewrite > (aluHC05_destruct_7 … H);
 283  nrewrite > (aluHC05_destruct_8 … H);
 284  nrewrite > (aluHC05_destruct_9 … H);
 285  nrewrite > (aluHC05_destruct_10 … H);
 286  nrewrite > (aluHC05_destruct_11 … H);
 287  nrewrite > (aluHC05_destruct_12 … H);
 288  nrewrite > (aluHC05_destruct_13 … H);
 289  nchange with (
 290  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗
 291   (eq_w16 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 292   (eq_w16 y5 y5) ⊗ (eq_w16 y6 y6) ⊗
 293   (eq_w16 y7 y7) ⊗ (eq_bool y8 y8) ⊗
 294   (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗
 295   (eq_bool y11 y11) ⊗ (eq_bool y12 y12) ⊗
 296   (eq_bool y13 y13)) = true);
 297  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
 298  nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
 299  nrewrite > (eq_to_eqw16 y3 y3 (refl_eq …));
 300  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
 301  nrewrite > (eq_to_eqw16 y5 y5 (refl_eq …));
 302  nrewrite > (eq_to_eqw16 y6 y6 (refl_eq …));
 303  nrewrite > (eq_to_eqw16 y7 y7 (refl_eq …));
 304  nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
 305  nrewrite > (eq_to_eqbool y9 y9 (refl_eq …));
 306  nrewrite > (eq_to_eqbool y10 y10 (refl_eq …));
 307  nrewrite > (eq_to_eqbool y11 y11 (refl_eq …));
 308  nrewrite > (eq_to_eqbool y12 y12 (refl_eq …));
 309  nrewrite > (eq_to_eqbool y13 y13 (refl_eq …));
 310  napply refl_eq.
 311 nqed.
 312
 313 nlemma decidable_aluHC05_aux1
 314  : ∀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.
 315  (x1 ≠ y1) →
 316  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 317  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 318  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 319  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 320  nnormalize; #H; #H1;
 321  napply (H (aluHC05_destruct_1 … H1)).
 322 nqed.
 323
 324 nlemma decidable_aluHC05_aux2
 325  : ∀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.
 326  (x2 ≠ y2) →
 327  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 328  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 329  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 330  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 331  nnormalize; #H; #H1;
 332  napply (H (aluHC05_destruct_2 … H1)).
 333 nqed.
 334
 335 nlemma decidable_aluHC05_aux3
 336  : ∀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.
 337  (x3 ≠ y3) →
 338  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 339  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 340  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 341  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 342  nnormalize; #H; #H1;
 343  napply (H (aluHC05_destruct_3 … H1)).
 344 nqed.
 345
 346 nlemma decidable_aluHC05_aux4
 347  : ∀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.
 348  (x4 ≠ y4) →
 349  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 350  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 351  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 352  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 353  nnormalize; #H; #H1;
 354  napply (H (aluHC05_destruct_4 … H1)).
 355 nqed.
 356
 357 nlemma decidable_aluHC05_aux5
 358  : ∀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.
 359  (x5 ≠ y5) →
 360  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 361  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 362  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 363  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 364  nnormalize; #H; #H1;
 365  napply (H (aluHC05_destruct_5 … H1)).
 366 nqed.
 367
 368 nlemma decidable_aluHC05_aux6
 369  : ∀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.
 370  (x6 ≠ y6) →
 371  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 372  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 373  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 374  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 375  nnormalize; #H; #H1;
 376  napply (H (aluHC05_destruct_6 … H1)).
 377 nqed.
 378
 379 nlemma decidable_aluHC05_aux7
 380  : ∀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.
 381  (x7 ≠ y7) →
 382  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 383  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 384  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 385  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 386  nnormalize; #H; #H1;
 387  napply (H (aluHC05_destruct_7 … H1)).
 388 nqed.
 389
 390 nlemma decidable_aluHC05_aux8
 391  : ∀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.
 392  (x8 ≠ y8) →
 393  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 394  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 395  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 396  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 397  nnormalize; #H; #H1;
 398  napply (H (aluHC05_destruct_8 … H1)).
 399 nqed.
 400
 401 nlemma decidable_aluHC05_aux9
 402  : ∀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.
 403  (x9 ≠ y9) →
 404  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 405  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 406  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 407  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 408  nnormalize; #H; #H1;
 409  napply (H (aluHC05_destruct_9 … H1)).
 410 nqed.
 411
 412 nlemma decidable_aluHC05_aux10
 413  : ∀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.
 414  (x10 ≠ y10) →
 415  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 416  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 417  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 418  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 419  nnormalize; #H; #H1;
 420  napply (H (aluHC05_destruct_10 … H1)).
 421 nqed.
 422
 423 nlemma decidable_aluHC05_aux11
 424  : ∀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.
 425  (x11 ≠ y11) →
 426  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 427  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 428  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 429  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 430  nnormalize; #H; #H1;
 431  napply (H (aluHC05_destruct_11 … H1)).
 432 nqed.
 433
 434 nlemma decidable_aluHC05_aux12
 435  : ∀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.
 436  (x12 ≠ y12) →
 437  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 438  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 439  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 440  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 441  nnormalize; #H; #H1;
 442  napply (H (aluHC05_destruct_12 … H1)).
 443 nqed.
 444
 445 nlemma decidable_aluHC05_aux13
 446  : ∀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.
 447  (x13 ≠ y13) →
 448  (mk_alu_HC05 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13) ≠
 449  (mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13).
 450  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 451  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 452  nnormalize; #H; #H1;
 453  napply (H (aluHC05_destruct_13 … H1)).
 454 nqed.
 455
 456 nlemma decidable_aluHC05 : ∀x,y:alu_HC05.decidable (x = y).
 457  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 458  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 459  nnormalize;
 460  napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
 461  ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC05_aux1 … H))
 462  ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
 463   ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC05_aux2 … H1))
 464   ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x3 y3) …);
 465    ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC05_aux3 … H2))
 466    ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
 467     ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC05_aux4 … H3))
 468     ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …);
 469      ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC05_aux5 … H4))
 470      ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x6 y6) …);
 471       ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC05_aux6 … H5))
 472       ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x7 y7) …);
 473        ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC05_aux7 … H6))
 474        ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
 475         ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC05_aux8 … H7))
 476         ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …);
 477          ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC05_aux9 … H8))
 478          ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …);
 479           ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC05_aux10 … H9))
 480           ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …);
 481            ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC05_aux11 … H10))
 482            ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …);
 483             ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC05_aux12 … H11))
 484             ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x13 y13) …);
 485              ##[ ##2: #H12; napply (or2_intro2 … (decidable_aluHC05_aux13 … H12))
 486              ##| ##1: #H12; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
 487                       nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
 488                       nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
 489                       nrewrite > H12; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 490              ##]
 491             ##]
 492            ##]
 493           ##]
 494          ##]
 495         ##]
 496        ##]
 497       ##]
 498      ##]
 499     ##]
 500    ##]
 501   ##]
 502  ##]
 503 nqed.