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