helm/software/matita/contribs/ng_assembly2/emulator/status/HC05_status.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 "emulator/status/HC05_status_base.ma".
  24
  25 (* *********************************** *)
  26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  27 (* *********************************** *)
  28
  29 nlemma aluHC05_destruct_1 :
  30 ∀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.
  31  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 →
  32  x1 = y1.
  33  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  34  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  35  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  36                 with [ mk_alu_HC05 a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  37  nrewrite < H;
  38  nnormalize;
  39  napply refl_eq.
  40 nqed.
  41
  42 nlemma aluHC05_destruct_2 :
  43 ∀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.
  44  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 →
  45  x2 = y2.
  46  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  47  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  48  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  49                 with [ mk_alu_HC05 _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  50  nrewrite < H;
  51  nnormalize;
  52  napply refl_eq.
  53 nqed.
  54
  55 nlemma aluHC05_destruct_3 :
  56 ∀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.
  57  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 →
  58  x3 = y3.
  59  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  60  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  61  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  62                 with [ mk_alu_HC05 _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  63  nrewrite < H;
  64  nnormalize;
  65  napply refl_eq.
  66 nqed.
  67
  68 nlemma aluHC05_destruct_4 :
  69 ∀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.
  70  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 →
  71  x4 = y4.
  72  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  73  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  74  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  75                 with [ mk_alu_HC05 _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  76  nrewrite < H;
  77  nnormalize;
  78  napply refl_eq.
  79 nqed.
  80
  81 nlemma aluHC05_destruct_5 :
  82 ∀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.
  83  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 →
  84  x5 = y5.
  85  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  86  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
  87  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
  88                 with [ mk_alu_HC05 _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
  89  nrewrite < H;
  90  nnormalize;
  91  napply refl_eq.
  92 nqed.
  93
  94 nlemma aluHC05_destruct_6 :
  95 ∀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.
  96  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 →
  97  x6 = y6.
  98  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
  99  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 100  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 101                 with [ mk_alu_HC05 _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x6 = a ]);
 102  nrewrite < H;
 103  nnormalize;
 104  napply refl_eq.
 105 nqed.
 106
 107 nlemma aluHC05_destruct_7 :
 108 ∀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.
 109  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 →
 110  x7 = y7.
 111  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 112  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 113  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 114                 with [ mk_alu_HC05 _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x7 = a ]);
 115  nrewrite < H;
 116  nnormalize;
 117  napply refl_eq.
 118 nqed.
 119
 120 nlemma aluHC05_destruct_8 :
 121 ∀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.
 122  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 →
 123  x8 = y8.
 124  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 125  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 126  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 127                 with [ mk_alu_HC05 _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x8 = a ]);
 128  nrewrite < H;
 129  nnormalize;
 130  napply refl_eq.
 131 nqed.
 132
 133 nlemma aluHC05_destruct_9 :
 134 ∀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.
 135  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 →
 136  x9 = y9.
 137  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 138  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 139  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 140                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x9 = a ]);
 141  nrewrite < H;
 142  nnormalize;
 143  napply refl_eq.
 144 nqed.
 145
 146 nlemma aluHC05_destruct_10 :
 147 ∀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.
 148  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 →
 149  x10 = y10.
 150  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 151  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 152  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 153                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x10 = a ]);
 154  nrewrite < H;
 155  nnormalize;
 156  napply refl_eq.
 157 nqed.
 158
 159 nlemma aluHC05_destruct_11 :
 160 ∀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.
 161  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 →
 162  x11 = y11.
 163  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 164  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 165  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 166                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x11 = a ]);
 167  nrewrite < H;
 168  nnormalize;
 169  napply refl_eq.
 170 nqed.
 171
 172 nlemma aluHC05_destruct_12 :
 173 ∀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.
 174  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 →
 175  x12 = y12.
 176  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 177  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 178  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 179                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x12 = a ]);
 180  nrewrite < H;
 181  nnormalize;
 182  napply refl_eq.
 183 nqed.
 184
 185 nlemma aluHC05_destruct_13 :
 186 ∀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.
 187  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 →
 188  x13 = y13.
 189  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 190  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 191  nchange with (match mk_alu_HC05 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13
 192                 with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x13 = a ]);
 193  nrewrite < H;
 194  nnormalize;
 195  napply refl_eq.
 196 nqed.
 197
 198 nlemma eq_to_eqaluHC05 : ∀alu1,alu2.alu1 = alu2 → eq_HC05_alu alu1 alu2 = true.
 199  #alu1; #alu2;
 200  ncases alu1;
 201  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 202  ncases alu2;
 203  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 204  nrewrite > (aluHC05_destruct_1 … H);
 205  nrewrite > (aluHC05_destruct_2 … H);
 206  nrewrite > (aluHC05_destruct_3 … H);
 207  nrewrite > (aluHC05_destruct_4 … H);
 208  nrewrite > (aluHC05_destruct_5 … H);
 209  nrewrite > (aluHC05_destruct_6 … H);
 210  nrewrite > (aluHC05_destruct_7 … H);
 211  nrewrite > (aluHC05_destruct_8 … H);
 212  nrewrite > (aluHC05_destruct_9 … H);
 213  nrewrite > (aluHC05_destruct_10 … H);
 214  nrewrite > (aluHC05_destruct_11 … H);
 215  nrewrite > (aluHC05_destruct_12 … H);
 216  nrewrite > (aluHC05_destruct_13 … H);
 217  nchange with (
 218  ((eqc ? y1 y1) ⊗ (eqc ? y2 y2) ⊗
 219   (eqc ? y3 y3) ⊗ (eqc ? y4 y4) ⊗
 220   (eqc ? y5 y5) ⊗ (eqc ? y6 y6) ⊗
 221   (eqc ? y7 y7) ⊗ (eqc ? y8 y8) ⊗
 222   (eqc ? y9 y9) ⊗ (eqc ? y10 y10) ⊗
 223   (eqc ? y11 y11) ⊗ (eqc ? y12 y12) ⊗
 224   (eqc ? y13 y13)) = true);
 225  nrewrite > (eq_to_eqc ? y1 y1 (refl_eq …));
 226  nrewrite > (eq_to_eqc ? y2 y2 (refl_eq …));
 227  nrewrite > (eq_to_eqc ? y3 y3 (refl_eq …));
 228  nrewrite > (eq_to_eqc ? y4 y4 (refl_eq …));
 229  nrewrite > (eq_to_eqc ? y5 y5 (refl_eq …));
 230  nrewrite > (eq_to_eqc ? y6 y6 (refl_eq …));
 231  nrewrite > (eq_to_eqc ? y7 y7 (refl_eq …));
 232  nrewrite > (eq_to_eqc ? y8 y8 (refl_eq …));
 233  nrewrite > (eq_to_eqc ? y9 y9 (refl_eq …));
 234  nrewrite > (eq_to_eqc ? y10 y10 (refl_eq …));
 235  nrewrite > (eq_to_eqc ? y11 y11 (refl_eq …));
 236  nrewrite > (eq_to_eqc ? y12 y12 (refl_eq …));
 237  nrewrite > (eq_to_eqc ? y13 y13 (refl_eq …));
 238  napply refl_eq.
 239 nqed.
 240
 241 nlemma neqaluHC05_to_neq : ∀alu1,alu2.eq_HC05_alu alu1 alu2 = false → alu1 ≠ alu2.
 242  #s1; #s2; #H;
 243  napply (not_to_not (s1 = s2) (eq_HC05_alu s1 s2 = true) …);
 244  ##[ ##1: napply (eq_to_eqaluHC05 s1 s2)
 245  ##| ##2: napply (eqfalse_to_neqtrue … H)
 246  ##]
 247 nqed.
 248
 249 nlemma eqaluHC05_to_eq : ∀alu1,alu2.eq_HC05_alu alu1 alu2 = true → alu1 = alu2.
 250  #alu1; #alu2;
 251  ncases alu1;
 252  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 253  ncases alu2;
 254  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #H;
 255  nchange in H:(%) with (
 256  ((eqc ? x1 y1) ⊗ (eqc ? x2 y2) ⊗
 257   (eqc ? x3 y3) ⊗ (eqc ? x4 y4) ⊗
 258   (eqc ? x5 y5) ⊗ (eqc ? x6 y6) ⊗
 259   (eqc ? x7 y7) ⊗ (eqc ? x8 y8) ⊗
 260   (eqc ? x9 y9) ⊗ (eqc ? x10 y10) ⊗
 261   (eqc ? x11 y11) ⊗ (eqc ? x12 y12) ⊗
 262   (eqc ? x13 y13)) = true);
 263  nrewrite > (eqc_to_eq … (andb_true_true_r … H));
 264  nletin H1 ≝ (andb_true_true_l … H);
 265  nrewrite > (eqc_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
 266  nletin H2 ≝ (andb_true_true_l … H1);
 267  nrewrite > (eqc_to_eq … (andb_true_true_r … H2));
 268  nletin H3 ≝ (andb_true_true_l … H2);
 269  nrewrite > (eqc_to_eq … (andb_true_true_r … H3));
 270  nletin H4 ≝ (andb_true_true_l … H3);
 271  nrewrite > (eqc_to_eq … (andb_true_true_r … H4));
 272  nletin H5 ≝ (andb_true_true_l … H4);
 273  nrewrite > (eqc_to_eq … (andb_true_true_r … H5));
 274  nletin H6 ≝ (andb_true_true_l … H5);
 275  nrewrite > (eqc_to_eq … (andb_true_true_r … H6));
 276  nletin H7 ≝ (andb_true_true_l … H6);
 277  nrewrite > (eqc_to_eq … (andb_true_true_r … H7));
 278  nletin H8 ≝ (andb_true_true_l … H7);
 279  nrewrite > (eqc_to_eq … (andb_true_true_r … H8));
 280  nletin H9 ≝ (andb_true_true_l … H8);
 281  nrewrite > (eqc_to_eq … (andb_true_true_r … H9));
 282  nletin H10 ≝ (andb_true_true_l … H9);
 283  nrewrite > (eqc_to_eq … (andb_true_true_r … H10));
 284  nletin H11 ≝ (andb_true_true_l … H10);
 285  nrewrite > (eqc_to_eq … (andb_true_true_r … H11));
 286  nrewrite > (eqc_to_eq … (andb_true_true_l … H11));
 287  napply refl_eq.
 288 nqed.
 289
 290 nlemma neq_to_neqaluHC05 : ∀alu1,alu2.alu1 ≠ alu2 → eq_HC05_alu alu1 alu2 = false.
 291  #s1; #s2; #H;
 292  napply (neqtrue_to_eqfalse (eq_HC05_alu s1 s2));
 293  napply (not_to_not (eq_HC05_alu s1 s2 = true) (s1 = s2) ? H);
 294  napply (eqaluHC05_to_eq s1 s2).
 295 nqed.
 296
 297 nlemma decidable_aluHC05 : ∀x,y:alu_HC05.decidable (x = y).
 298  #x; #y; nnormalize;
 299  napply (or2_elim (eq_HC05_alu x y = true) (eq_HC05_alu x y = false) ? (decidable_bexpr ?));
 300  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqaluHC05_to_eq … H))
 301  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqaluHC05_to_neq … H))
 302  ##]
 303 nqed.
 304
 305 nlemma symmetric_eqaluHC05 : symmetricT alu_HC05 bool eq_HC05_alu.
 306  #alu1; #alu2;
 307  ncases alu1;
 308  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13;
 309  ncases alu2;
 310  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13;
 311  nchange with (
 312   ((eqc ? x1 y1) ⊗ (eqc ? x2 y2) ⊗ (eqc ? x3 y3) ⊗ (eqc ? x4 y4) ⊗
 313   (eqc ? x5 y5) ⊗ (eqc ? x6 y6) ⊗  (eqc ? x7 y7) ⊗ (eqc ? x8 y8) ⊗
 314   (eqc ? x9 y9) ⊗ (eqc ? x10 y10) ⊗  (eqc ? x11 y11) ⊗ (eqc ? x12 y12) ⊗
 315   (eqc ? x13 y13)) = ((eqc ? y1 x1) ⊗  (eqc ? y2 x2) ⊗ (eqc ? y3 x3) ⊗
 316   (eqc ? y4 x4) ⊗ (eqc ? y5 x5) ⊗  (eqc ? y6 x6) ⊗ (eqc ? y7 x7) ⊗
 317   (eqc ? y8 x8) ⊗ (eqc ? y9 x9) ⊗  (eqc ? y10 x10) ⊗ (eqc ? y11 x11) ⊗
 318   (eqc ? y12 x12) ⊗ (eqc ? y13 x13)));
 319  nrewrite > (symmetric_eqc ? x1 y1);
 320  nrewrite > (symmetric_eqc ? x2 y2);
 321  nrewrite > (symmetric_eqc ? x3 y3);
 322  nrewrite > (symmetric_eqc ? x4 y4);
 323  nrewrite > (symmetric_eqc ? x5 y5);
 324  nrewrite > (symmetric_eqc ? x6 y6);
 325  nrewrite > (symmetric_eqc ? x7 y7);
 326  nrewrite > (symmetric_eqc ? x8 y8);
 327  nrewrite > (symmetric_eqc ? x9 y9);
 328  nrewrite > (symmetric_eqc ? x10 y10);
 329  nrewrite > (symmetric_eqc ? x11 y11);
 330  nrewrite > (symmetric_eqc ? x12 y12);
 331  nrewrite > (symmetric_eqc ? x13 y13);
 332  napply refl_eq.
 333 nqed.
 334
 335 nlemma aluHC05_is_comparable : comparable.
 336  @ alu_HC05
 337   ##[ napply (mk_alu_HC05 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
 338                           (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
 339                           (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
 340                           (zeroc ?))
 341   ##| napply forall_HC05_alu
 342   ##| napply eq_HC05_alu
 343   ##| napply eqaluHC05_to_eq
 344   ##| napply eq_to_eqaluHC05
 345   ##| napply neqaluHC05_to_neq
 346   ##| napply neq_to_neqaluHC05
 347   ##| napply decidable_aluHC05
 348   ##| napply symmetric_eqaluHC05
 349   ##]
 350 nqed.
 351
 352 unification hint 0 ≔ ⊢ carr aluHC05_is_comparable ≡ alu_HC05.