helm/software/matita/contribs/ng_assembly/emulator/status/HC08_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/HC08_status.ma".
  25
  26 (* *********************************** *)
  27 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  28 (* *********************************** *)
  29
  30 nlemma aluHC08_destruct_1 :
  31 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
  32  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 →
  33  x1 = y1.
  34  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
  35  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
  36  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
  37                 with [ mk_alu_HC08 a _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  38  nrewrite < H;
  39  nnormalize;
  40  napply refl_eq.
  41 nqed.
  42
  43 nlemma aluHC08_destruct_2 :
  44 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
  45  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 →
  46  x2 = y2.
  47  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
  48  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
  49  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
  50                 with [ mk_alu_HC08 _ a _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  51  nrewrite < H;
  52  nnormalize;
  53  napply refl_eq.
  54 nqed.
  55
  56 nlemma aluHC08_destruct_3 :
  57 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
  58  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 →
  59  x3 = y3.
  60  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
  61  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
  62  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
  63                 with [ mk_alu_HC08 _ _ a _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  64  nrewrite < H;
  65  nnormalize;
  66  napply refl_eq.
  67 nqed.
  68
  69 nlemma aluHC08_destruct_4 :
  70 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
  71  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 →
  72  x4 = y4.
  73  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
  74  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
  75  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
  76                 with [ mk_alu_HC08 _ _ _ a _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  77  nrewrite < H;
  78  nnormalize;
  79  napply refl_eq.
  80 nqed.
  81
  82 nlemma aluHC08_destruct_5 :
  83 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
  84  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 →
  85  x5 = y5.
  86  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
  87  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
  88  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
  89                 with [ mk_alu_HC08 _ _ _ _ a _ _ _ _ _ _ _ ⇒ x5 = a ]);
  90  nrewrite < H;
  91  nnormalize;
  92  napply refl_eq.
  93 nqed.
  94
  95 nlemma aluHC08_destruct_6 :
  96 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
  97  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 →
  98  x6 = y6.
  99  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 100  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 101  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 102                 with [ mk_alu_HC08 _ _ _ _ _ a _ _ _ _ _ _ ⇒ x6 = a ]);
 103  nrewrite < H;
 104  nnormalize;
 105  napply refl_eq.
 106 nqed.
 107
 108 nlemma aluHC08_destruct_7 :
 109 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 110  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 →
 111  x7 = y7.
 112  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 113  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 114  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 115                 with [ mk_alu_HC08 _ _ _ _ _ _ a _ _ _ _ _ ⇒ x7 = a ]);
 116  nrewrite < H;
 117  nnormalize;
 118  napply refl_eq.
 119 nqed.
 120
 121 nlemma aluHC08_destruct_8 :
 122 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 123  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 →
 124  x8 = y8.
 125  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 126  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 127  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 128                 with [ mk_alu_HC08 _ _ _ _ _ _ _ a _ _ _ _ ⇒ x8 = a ]);
 129  nrewrite < H;
 130  nnormalize;
 131  napply refl_eq.
 132 nqed.
 133
 134 nlemma aluHC08_destruct_9 :
 135 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 136  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 →
 137  x9 = y9.
 138  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 139  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 140  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 141                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ a _ _ _ ⇒ x9 = a ]);
 142  nrewrite < H;
 143  nnormalize;
 144  napply refl_eq.
 145 nqed.
 146
 147 nlemma aluHC08_destruct_10 :
 148 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 149  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 →
 150  x10 = y10.
 151  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 152  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 153  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 154                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ a _ _ ⇒ x10 = a ]);
 155  nrewrite < H;
 156  nnormalize;
 157  napply refl_eq.
 158 nqed.
 159
 160 nlemma aluHC08_destruct_11 :
 161 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 162  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 →
 163  x11 = y11.
 164  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 165  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 166  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 167                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ a _ ⇒ x11 = a ]);
 168  nrewrite < H;
 169  nnormalize;
 170  napply refl_eq.
 171 nqed.
 172
 173 nlemma aluHC08_destruct_12 :
 174 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 175  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 →
 176  x12 = y12.
 177  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 178  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 179  nchange with (match mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12
 180                 with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ a ⇒ x12 = a ]);
 181  nrewrite < H;
 182  nnormalize;
 183  napply refl_eq.
 184 nqed.
 185
 186 nlemma symmetric_eqaluHC08 : symmetricT alu_HC08 bool eq_HC08_alu.
 187  #alu1; #alu2;
 188  ncases alu1;
 189  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 190  ncases alu2;
 191  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 192  nchange with (
 193   ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 194    (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
 195    (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) =
 196    ((eq_b8 y1 x1) ⊗ (eq_b8 y2 x2) ⊗ (eq_b8 y3 x3) ⊗ (eq_w16 y4 x4) ⊗
 197    (eq_w16 y5 x5) ⊗ (eq_bool y6 x6) ⊗ (eq_bool y7 x7) ⊗ (eq_bool y8 x8) ⊗
 198    (eq_bool y9 x9) ⊗ (eq_bool y10 x10) ⊗ (eq_bool y11 x11) ⊗ (eq_bool y12 x12)));
 199  nrewrite > (symmetric_eqb8 x1 y1);
 200  nrewrite > (symmetric_eqb8 x2 y2);
 201  nrewrite > (symmetric_eqb8 x3 y3);
 202  nrewrite > (symmetric_eqw16 x4 y4);
 203  nrewrite > (symmetric_eqw16 x5 y5);
 204  nrewrite > (symmetric_eqbool x6 y6);
 205  nrewrite > (symmetric_eqbool x7 y7);
 206  nrewrite > (symmetric_eqbool x8 y8);
 207  nrewrite > (symmetric_eqbool x9 y9);
 208  nrewrite > (symmetric_eqbool x10 y10);
 209  nrewrite > (symmetric_eqbool x11 y11);
 210  nrewrite > (symmetric_eqbool x12 y12);
 211  napply refl_eq.
 212 nqed.
 213
 214 nlemma eqaluHC08_to_eq : ∀alu1,alu2.eq_HC08_alu alu1 alu2 = true → alu1 = alu2.
 215  #alu1; #alu2;
 216  ncases alu1;
 217  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 218  ncases alu2;
 219  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 220  nchange in H:(%) with (
 221  ((eq_b8 x1 y1) ⊗ (eq_b8 x2 y2) ⊗ (eq_b8 x3 y3) ⊗ (eq_w16 x4 y4) ⊗
 222   (eq_w16 x5 y5) ⊗ (eq_bool x6 y6) ⊗ (eq_bool x7 y7) ⊗ (eq_bool x8 y8) ⊗
 223   (eq_bool x9 y9) ⊗ (eq_bool x10 y10) ⊗ (eq_bool x11 y11) ⊗ (eq_bool x12 y12)) = true);
 224  nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
 225  nletin H1 ≝ (andb_true_true_l … H);
 226  nrewrite > (eqbool_to_eq … (andb_true_true_r … H1));
 227  nletin H2 ≝ (andb_true_true_l … H1);
 228  nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
 229  nletin H3 ≝ (andb_true_true_l … H2);
 230  nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
 231  nletin H4 ≝ (andb_true_true_l … H3);
 232  nrewrite > (eqbool_to_eq … (andb_true_true_r … H4));
 233  nletin H5 ≝ (andb_true_true_l … H4);
 234  nrewrite > (eqbool_to_eq … (andb_true_true_r … H5));
 235  nletin H6 ≝ (andb_true_true_l … H5);
 236  nrewrite > (eqbool_to_eq … (andb_true_true_r … H6));
 237  nletin H7 ≝ (andb_true_true_l … H6);
 238  nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
 239  nletin H8 ≝ (andb_true_true_l … H7);
 240  nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
 241  nletin H9 ≝ (andb_true_true_l … H8);
 242  nrewrite > (eqb8_to_eq … (andb_true_true_r … H9));
 243  nletin H10 ≝ (andb_true_true_l … H9);
 244  nrewrite > (eqb8_to_eq … (andb_true_true_r … H10));
 245  nrewrite > (eqb8_to_eq … (andb_true_true_l … H10));
 246  napply refl_eq.
 247 nqed.
 248
 249 nlemma eq_to_eqaluHC08 : ∀alu1,alu2.alu1 = alu2 → eq_HC08_alu alu1 alu2 = true.
 250  #alu1; #alu2;
 251  ncases alu1;
 252  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 253  ncases alu2;
 254  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #H;
 255  nrewrite > (aluHC08_destruct_1 … H);
 256  nrewrite > (aluHC08_destruct_2 … H);
 257  nrewrite > (aluHC08_destruct_3 … H);
 258  nrewrite > (aluHC08_destruct_4 … H);
 259  nrewrite > (aluHC08_destruct_5 … H);
 260  nrewrite > (aluHC08_destruct_6 … H);
 261  nrewrite > (aluHC08_destruct_7 … H);
 262  nrewrite > (aluHC08_destruct_8 … H);
 263  nrewrite > (aluHC08_destruct_9 … H);
 264  nrewrite > (aluHC08_destruct_10 … H);
 265  nrewrite > (aluHC08_destruct_11 … H);
 266  nrewrite > (aluHC08_destruct_12 … H);
 267  nchange with (
 268  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_w16 y4 y4) ⊗
 269   (eq_w16 y5 y5) ⊗ (eq_bool y6 y6) ⊗ (eq_bool y7 y7) ⊗ (eq_bool y8 y8) ⊗
 270   (eq_bool y9 y9) ⊗ (eq_bool y10 y10) ⊗ (eq_bool y11 y11) ⊗ (eq_bool y12 y12)) = true);
 271  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
 272  nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
 273  nrewrite > (eq_to_eqb8 y3 y3 (refl_eq …));
 274  nrewrite > (eq_to_eqw16 y4 y4 (refl_eq …));
 275  nrewrite > (eq_to_eqw16 y5 y5 (refl_eq …));
 276  nrewrite > (eq_to_eqbool y6 y6 (refl_eq …));
 277  nrewrite > (eq_to_eqbool y7 y7 (refl_eq …));
 278  nrewrite > (eq_to_eqbool y8 y8 (refl_eq …));
 279  nrewrite > (eq_to_eqbool y9 y9 (refl_eq …));
 280  nrewrite > (eq_to_eqbool y10 y10 (refl_eq …));
 281  nrewrite > (eq_to_eqbool y11 y11 (refl_eq …));
 282  nrewrite > (eq_to_eqbool y12 y12 (refl_eq …));
 283  napply refl_eq.
 284 nqed.
 285
 286 nlemma decidable_aluHC08_aux1
 287  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 288  (x1 ≠ y1) →
 289  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 290  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 291  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 292  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 293  nnormalize; #H; #H1;
 294  napply (H (aluHC08_destruct_1 … H1)).
 295 nqed.
 296
 297 nlemma decidable_aluHC08_aux2
 298  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 299  (x2 ≠ y2) →
 300  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 301  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 302  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 303  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 304  nnormalize; #H; #H1;
 305  napply (H (aluHC08_destruct_2 … H1)).
 306 nqed.
 307
 308 nlemma decidable_aluHC08_aux3
 309  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 310  (x3 ≠ y3) →
 311  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 312  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 313  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 314  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 315  nnormalize; #H; #H1;
 316  napply (H (aluHC08_destruct_3 … H1)).
 317 nqed.
 318
 319 nlemma decidable_aluHC08_aux4
 320  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 321  (x4 ≠ y4) →
 322  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 323  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 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;
 326  nnormalize; #H; #H1;
 327  napply (H (aluHC08_destruct_4 … H1)).
 328 nqed.
 329
 330 nlemma decidable_aluHC08_aux5
 331  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 332  (x5 ≠ y5) →
 333  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 334  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 335  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 336  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 337  nnormalize; #H; #H1;
 338  napply (H (aluHC08_destruct_5 … H1)).
 339 nqed.
 340
 341 nlemma decidable_aluHC08_aux6
 342  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 343  (x6 ≠ y6) →
 344  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 345  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 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;
 348  nnormalize; #H; #H1;
 349  napply (H (aluHC08_destruct_6 … H1)).
 350 nqed.
 351
 352 nlemma decidable_aluHC08_aux7
 353  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 354  (x7 ≠ y7) →
 355  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 356  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 357  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 358  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 359  nnormalize; #H; #H1;
 360  napply (H (aluHC08_destruct_7 … H1)).
 361 nqed.
 362
 363 nlemma decidable_aluHC08_aux8
 364  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 365  (x8 ≠ y8) →
 366  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 367  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 368  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 369  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 370  nnormalize; #H; #H1;
 371  napply (H (aluHC08_destruct_8 … H1)).
 372 nqed.
 373
 374 nlemma decidable_aluHC08_aux9
 375  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 376  (x9 ≠ y9) →
 377  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 378  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 379  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 380  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 381  nnormalize; #H; #H1;
 382  napply (H (aluHC08_destruct_9 … H1)).
 383 nqed.
 384
 385 nlemma decidable_aluHC08_aux10
 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  (x10 ≠ y10) →
 388  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 389  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 390  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 391  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 392  nnormalize; #H; #H1;
 393  napply (H (aluHC08_destruct_10 … H1)).
 394 nqed.
 395
 396 nlemma decidable_aluHC08_aux11
 397  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12.
 398  (x11 ≠ y11) →
 399  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 400  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 401  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 402  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 403  nnormalize; #H; #H1;
 404  napply (H (aluHC08_destruct_11 … H1)).
 405 nqed.
 406
 407 nlemma decidable_aluHC08_aux12
 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  (x12 ≠ y12) →
 410  (mk_alu_HC08 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12) ≠
 411  (mk_alu_HC08 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12).
 412  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 413  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 414  nnormalize; #H; #H1;
 415  napply (H (aluHC08_destruct_12 … H1)).
 416 nqed.
 417
 418 nlemma decidable_aluHC08 : ∀x,y:alu_HC08.decidable (x = y).
 419  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12;
 420  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12;
 421  nnormalize;
 422  napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
 423  ##[ ##2: #H; napply (or2_intro2 … (decidable_aluHC08_aux1 … H))
 424  ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
 425   ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluHC08_aux2 … H1))
 426   ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x3 y3) …);
 427    ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluHC08_aux3 … H2))
 428    ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x4 y4) …);
 429     ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluHC08_aux4 … H3))
 430     ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x5 y5) …);
 431      ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluHC08_aux5 … H4))
 432      ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x6 y6) …);
 433       ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluHC08_aux6 … H5))
 434       ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x7 y7) …);
 435        ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluHC08_aux7 … H6))
 436        ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x8 y8) …);
 437         ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluHC08_aux8 … H7))
 438         ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x9 y9) …);
 439          ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluHC08_aux9 … H8))
 440          ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x10 y10) …);
 441           ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluHC08_aux10 … H9))
 442           ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x11 y11) …);
 443            ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluHC08_aux11 … H10))
 444            ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x12 y12) …);
 445             ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluHC08_aux12 … H11))
 446             ##| ##1: #H11; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
 447                       nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
 448                       nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
 449                       napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 450             ##]
 451            ##]
 452           ##]
 453          ##]
 454         ##]
 455        ##]
 456       ##]
 457      ##]
 458     ##]
 459    ##]
 460   ##]
 461  ##]
 462 nqed.