matita/matita/contribs/ng_assembly/emulator/status/IP2022_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/oct_lemmas.ma".
  24 include "num/word16_lemmas.ma".
  25 include "num/word24_lemmas.ma".
  26 include "emulator/status/IP2022_status.ma".
  27 include "emulator/memory/memory_struct_lemmas.ma".
  28
  29 (* *********************************** *)
  30 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  31 (* *********************************** *)
  32
  33 nlemma aluIP2022_destruct_1 :
  34 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
  35  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  36  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  37  x1 = y1.
  38  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  39  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  40  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  41                 with [ mk_alu_IP2022 a _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  42  nrewrite < H;
  43  nnormalize;
  44  napply refl_eq.
  45 nqed.
  46
  47 nlemma aluIP2022_destruct_2 :
  48 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
  49  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  50  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  51  x2 = y2.
  52  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  53  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  54  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  55                 with [ mk_alu_IP2022 _ a _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  56  nrewrite < H;
  57  nnormalize;
  58  napply refl_eq.
  59 nqed.
  60
  61 nlemma aluIP2022_destruct_3 :
  62 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
  63  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  64  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  65  x3 = y3.
  66  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  67  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  68  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  69                 with [ mk_alu_IP2022 _ _ a _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  70  nrewrite < H;
  71  nnormalize;
  72  napply refl_eq.
  73 nqed.
  74
  75 nlemma aluIP2022_destruct_4 :
  76 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
  77  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  78  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  79  x4 = y4.
  80  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  81  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  82  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  83                 with [ mk_alu_IP2022 _ _ _ a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  84  nrewrite < H;
  85  nnormalize;
  86  napply refl_eq.
  87 nqed.
  88
  89 nlemma aluIP2022_destruct_5 :
  90 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
  91  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  92  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  93  x5 = y5.
  94  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  95  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  96  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  97                 with [ mk_alu_IP2022 _ _ _ _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
  98  nrewrite < H;
  99  nnormalize;
 100  napply refl_eq.
 101 nqed.
 102
 103 nlemma aluIP2022_destruct_6 :
 104 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 105  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 106  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 107  x6 = y6.
 108  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 109  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 110  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 111                 with [ mk_alu_IP2022 _ _ _ _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x6 = a ]);
 112  nrewrite < H;
 113  nnormalize;
 114  napply refl_eq.
 115 nqed.
 116
 117 nlemma aluIP2022_destruct_7 :
 118 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 119  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 120  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 121  x7 = y7.
 122  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 123  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 124  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 125                 with [ mk_alu_IP2022 _ _ _ _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x7 = a ]);
 126  nrewrite < H;
 127  nnormalize;
 128  napply refl_eq.
 129 nqed.
 130
 131 nlemma aluIP2022_destruct_8 :
 132 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 133  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 134  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 135  x8 = y8.
 136  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 137  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 138  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 139                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x8 = a ]);
 140  nrewrite < H;
 141  nnormalize;
 142  napply refl_eq.
 143 nqed.
 144
 145 nlemma aluIP2022_destruct_9 :
 146 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 147  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 148  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 149  x9 = y9.
 150  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 151  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 152  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 153                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x9 = a ]);
 154  nrewrite < H;
 155  nnormalize;
 156  napply refl_eq.
 157 nqed.
 158
 159 nlemma aluIP2022_destruct_10 :
 160 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 161  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 162  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 163  x10 = y10.
 164  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 165  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 166  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 167                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x10 = a ]);
 168  nrewrite < H;
 169  nnormalize;
 170  napply refl_eq.
 171 nqed.
 172
 173 nlemma aluIP2022_destruct_11 :
 174 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 175  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 176  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 177  x11 = y11.
 178  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 179  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 180  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 181                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x11 = a ]);
 182  nrewrite < H;
 183  nnormalize;
 184  napply refl_eq.
 185 nqed.
 186
 187 nlemma aluIP2022_destruct_12 :
 188 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 189  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 190  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 191  x12 = y12.
 192  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 193  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 194  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 195                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x12 = a ]);
 196  nrewrite < H;
 197  nnormalize;
 198  napply refl_eq.
 199 nqed.
 200
 201 nlemma aluIP2022_destruct_13 :
 202 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 203  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 204  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 205  x13 = y13.
 206  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 207  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 208  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 209                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x13 = a ]);
 210  nrewrite < H;
 211  nnormalize;
 212  napply refl_eq.
 213 nqed.
 214
 215 nlemma aluIP2022_destruct_14 :
 216 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 217  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 218  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 219  x14 = y14.
 220  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 221  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 222  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 223                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x14 = a ]);
 224  nrewrite < H;
 225  nnormalize;
 226  napply refl_eq.
 227 nqed.
 228
 229 nlemma aluIP2022_destruct_15 :
 230 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 231  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 232  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 233  x15 = y15.
 234  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 235  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 236  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 237                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x15 = a ]);
 238  nrewrite < H;
 239  nnormalize;
 240  napply refl_eq.
 241 nqed.
 242
 243 nlemma aluIP2022_destruct_16 :
 244 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 245  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 246  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 247  x16 = y16.
 248  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 249  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 250  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 251                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x16 = a ]);
 252  nrewrite < H;
 253  nnormalize;
 254  napply refl_eq.
 255 nqed.
 256
 257 naxiom symmetric_eqaluIP2022 : symmetricT alu_IP2022 bool eq_IP2022_alu.
 258 (* !!! la compilazione avviene ma il tempo e' troppo lungo...
 259  #alu1; ncases alu1;
 260  #z1; #z2; #z3; #z4; #z5; #z6; #z7; #z8; #z9; #z10; #z11; #z12; #z13; #z14; #z15; #z16;
 261  #alu2; ncases alu2;
 262  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 263  nchange with (
 264   ((eq_b8 z1 y1) ⊗ (eq_b8 z2 y2) ⊗ (eq_b8 z3 y3) ⊗ (eq_ar8 ? eq_w24 z4 y4) ⊗
 265   (eq_ar16 ? eq_w16 z5 y5) ⊗ (eq_w16 z6 y6) ⊗ (eq_w16 z7 y7) ⊗ (eq_w16 z8 y8) ⊗
 266   (eq_w16 z9 y9) ⊗ (eq_w16 z10 y10) ⊗ (eq_ex z11 y11) ⊗ (eq_oct z12 y12) ⊗
 267   (eq_bool z13 y13) ⊗ (eq_bool z14 y14) ⊗ (eq_bool z15 y15) ⊗ (eq_bool z16 y16)) =
 268   ((eq_b8 y1 z1) ⊗ (eq_b8 y2 z2) ⊗ (eq_b8 y3 z3) ⊗ (eq_ar8 ? eq_w24 y4 z4) ⊗
 269   (eq_ar16 ? eq_w16 y5 z5) ⊗ (eq_w16 y6 z6) ⊗ (eq_w16 y7 z7) ⊗ (eq_w16 y8 z8) ⊗
 270   (eq_w16 y9 z9) ⊗ (eq_w16 y10 z10) ⊗ (eq_ex y11 z11) ⊗ (eq_oct y12 z12) ⊗
 271   (eq_bool y13 z13) ⊗ (eq_bool y14 z14) ⊗ (eq_bool y15 z15) ⊗ (eq_bool y16 z16)));
 272  nrewrite > (symmetric_eqb8 z1 y1);
 273  nrewrite > (symmetric_eqb8 z2 y2);
 274  nrewrite > (symmetric_eqb8 z3 y3);
 275  nrewrite > (symmetric_eqar8 ? eq_w24 symmetric_eqw24 z4 y4);
 276  nrewrite > (symmetric_eqar16 ? eq_w16 symmetric_eqw16 z5 y5);
 277  nrewrite > (symmetric_eqw16 z6 y6);
 278  nrewrite > (symmetric_eqw16 z7 y7);
 279  nrewrite > (symmetric_eqw16 z8 y8);
 280  nrewrite > (symmetric_eqw16 z9 y9);
 281  nrewrite > (symmetric_eqw16 z10 y10);
 282  nrewrite > (symmetric_eqex z11 y11);
 283  nrewrite > (symmetric_eqoct z12 y12);
 284  nrewrite > (symmetric_eqbool z13 y13);
 285  nrewrite > (symmetric_eqbool z14 y14);
 286  nrewrite > (symmetric_eqbool z15 y15);
 287  nrewrite > (symmetric_eqbool z16 y16);
 288  napply refl_eq.
 289 nqed.
 290 *)
 291
 292 nlemma eqaluIP2022_to_eq : ∀alu1,alu2.eq_IP2022_alu alu1 alu2 = true → alu1 = alu2.
 293  #alu1; ncases alu1;
 294  #z1; #z2; #z3; #z4; #z5; #z6; #z7; #z8; #z9; #z10; #z11; #z12; #z13; #z14; #z15; #z16;
 295  #alu2; ncases alu2;
 296  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 297  nchange in H:(%) with (
 298  ((eq_b8 z1 y1) ⊗ (eq_b8 z2 y2) ⊗ (eq_b8 z3 y3) ⊗ (eq_ar8 ? eq_w24 z4 y4) ⊗
 299   (eq_ar16 ? eq_w16 z5 y5) ⊗ (eq_w16 z6 y6) ⊗ (eq_w16 z7 y7) ⊗ (eq_w16 z8 y8) ⊗
 300   (eq_w16 z9 y9) ⊗ (eq_w16 z10 y10) ⊗ (eq_ex z11 y11) ⊗ (eq_oct z12 y12) ⊗
 301   (eq_bool z13 y13) ⊗ (eq_bool z14 y14) ⊗ (eq_bool z15 y15) ⊗ (eq_bool z16 y16)) = true);
 302  nrewrite > (eqbool_to_eq … (andb_true_true_r … H));
 303  nletin H1 ≝ (andb_true_true_l … H);
 304  nrewrite > (eqbool_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
 305  nletin H2 ≝ (andb_true_true_l … H1);
 306  nrewrite > (eqbool_to_eq … (andb_true_true_r … H2));
 307  nletin H3 ≝ (andb_true_true_l … H2);
 308  nrewrite > (eqbool_to_eq … (andb_true_true_r … H3));
 309  nletin H4 ≝ (andb_true_true_l … H3);
 310  nrewrite > (eqoct_to_eq … (andb_true_true_r … H4));
 311  nletin H5 ≝ (andb_true_true_l … H4);
 312  nrewrite > (eqex_to_eq … (andb_true_true_r … H5));
 313  nletin H6 ≝ (andb_true_true_l … H5);
 314  nrewrite > (eqw16_to_eq … (andb_true_true_r … H6));
 315  nletin H7 ≝ (andb_true_true_l … H6);
 316  nrewrite > (eqw16_to_eq … (andb_true_true_r … H7));
 317  nletin H8 ≝ (andb_true_true_l … H7);
 318  nrewrite > (eqw16_to_eq … (andb_true_true_r … H8));
 319  nletin H9 ≝ (andb_true_true_l … H8);
 320  nrewrite > (eqw16_to_eq … (andb_true_true_r … H9));
 321  nletin H10 ≝ (andb_true_true_l … H9);
 322  nrewrite > (eqw16_to_eq … (andb_true_true_r … H10));
 323  nletin H11 ≝ (andb_true_true_l … H10);
 324  nrewrite > (eqar16_to_eq ? eq_w16 eqw16_to_eq … (andb_true_true_r … H11));
 325  nletin H12 ≝ (andb_true_true_l … H11);
 326  nrewrite > (eqar8_to_eq ? eq_w24 eqw24_to_eq … (andb_true_true_r … H12));
 327  nletin H13 ≝ (andb_true_true_l … H12);
 328  nrewrite > (eqb8_to_eq … (andb_true_true_r … H13));
 329  nletin H14 ≝ (andb_true_true_l … H13);
 330  nrewrite > (eqb8_to_eq … (andb_true_true_r … H14));
 331  nrewrite > (eqb8_to_eq … (andb_true_true_l … H14));
 332  napply refl_eq.
 333 nqed.
 334
 335 naxiom eq_to_eqaluIP2022 : ∀alu1,alu2.alu1 = alu2 → eq_IP2022_alu alu1 alu2 = true.
 336 (* !!! la compilazione avviene ma il tempo e' troppo lungo...
 337  #alu1; ncases alu1;
 338  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 339  #alu2; ncases alu2;
 340  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 341  nrewrite > (aluIP2022_destruct_1 … H);
 342  nrewrite > (aluIP2022_destruct_2 … H);
 343  nrewrite > (aluIP2022_destruct_3 … H);
 344  nrewrite > (aluIP2022_destruct_4 … H);
 345  nrewrite > (aluIP2022_destruct_5 … H);
 346  nrewrite > (aluIP2022_destruct_6 … H);
 347  nrewrite > (aluIP2022_destruct_7 … H);
 348  nrewrite > (aluIP2022_destruct_8 … H);
 349  nrewrite > (aluIP2022_destruct_9 … H);
 350  nrewrite > (aluIP2022_destruct_10 … H);
 351  nrewrite > (aluIP2022_destruct_11 … H);
 352  nrewrite > (aluIP2022_destruct_12 … H);
 353  nrewrite > (aluIP2022_destruct_13 … H);
 354  nrewrite > (aluIP2022_destruct_14 … H);
 355  nrewrite > (aluIP2022_destruct_15 … H);
 356  nrewrite > (aluIP2022_destruct_16 … H);
 357  nchange with (
 358  ((eq_b8 y1 y1) ⊗ (eq_b8 y2 y2) ⊗ (eq_b8 y3 y3) ⊗ (eq_ar8 ? eq_w24 y4 y4) ⊗
 359   (eq_ar16 ? eq_w16 y5 y5) ⊗ (eq_w16 y6 y6) ⊗ (eq_w16 y7 y7) ⊗ (eq_w16 y8 y8) ⊗
 360   (eq_w16 y9 y9) ⊗ (eq_w16 y10 y10) ⊗ (eq_ex y11 y11) ⊗ (eq_oct y12 y12) ⊗
 361   (eq_bool y13 y13) ⊗ (eq_bool y14 y14) ⊗ (eq_bool y15 y15) ⊗ (eq_bool y16 y16)) = true);
 362  nrewrite > (eq_to_eqb8 y1 y1 (refl_eq …));
 363  nrewrite > (eq_to_eqb8 y2 y2 (refl_eq …));
 364  nrewrite > (eq_to_eqb8 y3 y3 (refl_eq …));
 365  nrewrite > (eq_to_eqar8 ? eq_w24 eq_to_eqw24 y4 y4 (refl_eq …));
 366  nrewrite > (eq_to_eqar16 ? eq_w16 eq_to_eqw16 y5 y5 (refl_eq …));
 367  nrewrite > (eq_to_eqw16 y6 y6 (refl_eq …));
 368  nrewrite > (eq_to_eqw16 y7 y7 (refl_eq …));
 369  nrewrite > (eq_to_eqw16 y8 y8 (refl_eq …));
 370  nrewrite > (eq_to_eqw16 y9 y9 (refl_eq …));
 371  nrewrite > (eq_to_eqw16 y10 y10 (refl_eq …));
 372  nrewrite > (eq_to_ex y11 y11 (refl_eq …));
 373  nrewrite > (eq_to_oct y12 y12 (refl_eq …));
 374  nrewrite > (eq_to_eqbool y13 y13 (refl_eq …));
 375  nrewrite > (eq_to_eqbool y14 y14 (refl_eq …));
 376  nrewrite > (eq_to_eqbool y15 y15 (refl_eq …));
 377  nrewrite > (eq_to_eqbool y16 y16 (refl_eq …));
 378  napply refl_eq.
 379 nqed.
 380 *)
 381
 382 nlemma decidable_aluIP2022_aux1
 383  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 384  (x1 ≠ y1) →
 385  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 386  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 387  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 388  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 389  nnormalize; #H; #H1;
 390  napply (H (aluIP2022_destruct_1 … H1)).
 391 nqed.
 392
 393 nlemma decidable_aluIP2022_aux2
 394  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 395  (x2 ≠ y2) →
 396  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 397  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 398  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 399  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 400  nnormalize; #H; #H1;
 401  napply (H (aluIP2022_destruct_2 … H1)).
 402 nqed.
 403
 404 nlemma decidable_aluIP2022_aux3
 405  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 406  (x3 ≠ y3) →
 407  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 408  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 409  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 410  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 411  nnormalize; #H; #H1;
 412  napply (H (aluIP2022_destruct_3 … H1)).
 413 nqed.
 414
 415 nlemma decidable_aluIP2022_aux4
 416  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 417  (x4 ≠ y4) →
 418  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 419  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 420  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 421  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 422  nnormalize; #H; #H1;
 423  napply (H (aluIP2022_destruct_4 … H1)).
 424 nqed.
 425
 426 nlemma decidable_aluIP2022_aux5
 427  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 428  (x5 ≠ y5) →
 429  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 430  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 431  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 432  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 433  nnormalize; #H; #H1;
 434  napply (H (aluIP2022_destruct_5 … H1)).
 435 nqed.
 436
 437 nlemma decidable_aluIP2022_aux6
 438  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 439  (x6 ≠ y6) →
 440  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 441  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 442  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 443  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 444  nnormalize; #H; #H1;
 445  napply (H (aluIP2022_destruct_6 … H1)).
 446 nqed.
 447
 448 nlemma decidable_aluIP2022_aux7
 449  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 450  (x7 ≠ y7) →
 451  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 452  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 453  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 454  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 455  nnormalize; #H; #H1;
 456  napply (H (aluIP2022_destruct_7 … H1)).
 457 nqed.
 458
 459 nlemma decidable_aluIP2022_aux8
 460  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 461  (x8 ≠ y8) →
 462  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 463  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 464  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 465  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 466  nnormalize; #H; #H1;
 467  napply (H (aluIP2022_destruct_8 … H1)).
 468 nqed.
 469
 470 nlemma decidable_aluIP2022_aux9
 471  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 472  (x9 ≠ y9) →
 473  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 474  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 475  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 476  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 477  nnormalize; #H; #H1;
 478  napply (H (aluIP2022_destruct_9 … H1)).
 479 nqed.
 480
 481 nlemma decidable_aluIP2022_aux10
 482  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 483  (x10 ≠ y10) →
 484  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 485  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 486  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 487  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 488  nnormalize; #H; #H1;
 489  napply (H (aluIP2022_destruct_10 … H1)).
 490 nqed.
 491
 492 nlemma decidable_aluIP2022_aux11
 493  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 494  (x11 ≠ y11) →
 495  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 496  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 497  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 498  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 499  nnormalize; #H; #H1;
 500  napply (H (aluIP2022_destruct_11 … H1)).
 501 nqed.
 502
 503 nlemma decidable_aluIP2022_aux12
 504  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 505  (x12 ≠ y12) →
 506  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 507  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 508  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 509  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 510  nnormalize; #H; #H1;
 511  napply (H (aluIP2022_destruct_12 … H1)).
 512 nqed.
 513
 514 nlemma decidable_aluIP2022_aux13
 515  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 516  (x13 ≠ y13) →
 517  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 518  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 519  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 520  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 521  nnormalize; #H; #H1;
 522  napply (H (aluIP2022_destruct_13 … H1)).
 523 nqed.
 524
 525 nlemma decidable_aluIP2022_aux14
 526  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 527  (x14 ≠ y14) →
 528  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 529  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 530  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 531  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 532  nnormalize; #H; #H1;
 533  napply (H (aluIP2022_destruct_14 … H1)).
 534 nqed.
 535
 536 nlemma decidable_aluIP2022_aux15
 537  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 538  (x15 ≠ y15) →
 539  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 540  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 541  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 542  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 543  nnormalize; #H; #H1;
 544  napply (H (aluIP2022_destruct_15 … H1)).
 545 nqed.
 546
 547 nlemma decidable_aluIP2022_aux16
 548  : ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16,y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16.
 549  (x16 ≠ y16) →
 550  (mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 551  (mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 552  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 553  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 554  nnormalize; #H; #H1;
 555  napply (H (aluIP2022_destruct_16 … H1)).
 556 nqed.
 557
 558 nlemma decidable_aluIP2022 : ∀x,y:alu_IP2022.decidable (x = y).
 559  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 560  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 561  nnormalize;
 562  napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x1 y1) …);
 563  ##[ ##2: #H; napply (or2_intro2 … (decidable_aluIP2022_aux1 … H))
 564  ##| ##1: #H; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x2 y2) …);
 565   ##[ ##2: #H1; napply (or2_intro2 … (decidable_aluIP2022_aux2 … H1))
 566   ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_b8 x3 y3) …);
 567    ##[ ##2: #H2; napply (or2_intro2 … (decidable_aluIP2022_aux3 … H2))
 568    ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_ar8 ? decidable_w24 x4 y4) …);
 569     ##[ ##2: #H3; napply (or2_intro2 … (decidable_aluIP2022_aux4 … H3))
 570     ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_ar16 ? decidable_w16 x5 y5) …);
 571      ##[ ##2: #H4; napply (or2_intro2 … (decidable_aluIP2022_aux5 … H4))
 572      ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x6 y6) …);
 573       ##[ ##2: #H5; napply (or2_intro2 … (decidable_aluIP2022_aux6 … H5))
 574       ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x7 y7) …);
 575        ##[ ##2: #H6; napply (or2_intro2 … (decidable_aluIP2022_aux7 … H6))
 576        ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x8 y8) …);
 577         ##[ ##2: #H7; napply (or2_intro2 … (decidable_aluIP2022_aux8 … H7))
 578         ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x9 y9) …);
 579          ##[ ##2: #H8; napply (or2_intro2 … (decidable_aluIP2022_aux9 … H8))
 580          ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_w16 x10 y10) …);
 581           ##[ ##2: #H9; napply (or2_intro2 … (decidable_aluIP2022_aux10 … H9))
 582           ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_ex x11 y11) …);
 583            ##[ ##2: #H10; napply (or2_intro2 … (decidable_aluIP2022_aux11 … H10))
 584            ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_oct x12 y12) …);
 585             ##[ ##2: #H11; napply (or2_intro2 … (decidable_aluIP2022_aux12 … H11))
 586             ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x13 y13) …);
 587              ##[ ##2: #H12; napply (or2_intro2 … (decidable_aluIP2022_aux13 … H12))
 588              ##| ##1: #H12; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x14 y14) …);
 589               ##[ ##2: #H13; napply (or2_intro2 … (decidable_aluIP2022_aux14 … H13))
 590               ##| ##1: #H13; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x15 y15) …);
 591                ##[ ##2: #H14; napply (or2_intro2 … (decidable_aluIP2022_aux15 … H14))
 592                ##| ##1: #H14; napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_bool x16 y16) …);
 593                 ##[ ##2: #H15; napply (or2_intro2 … (decidable_aluIP2022_aux16 … H15))
 594                 ##| ##1: #H15; nrewrite > H; nrewrite > H1; nrewrite > H2; nrewrite > H3;
 595                       nrewrite > H4; nrewrite > H5; nrewrite > H6; nrewrite > H7;
 596                       nrewrite > H8; nrewrite > H9; nrewrite > H10; nrewrite > H11;
 597                       nrewrite > H12; nrewrite > H13; nrewrite > H14; nrewrite > H15;
 598                       napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …));
 599                 ##]
 600                ##]
 601               ##]
 602              ##]
 603             ##]
 604            ##]
 605           ##]
 606          ##]
 607         ##]
 608        ##]
 609       ##]
 610      ##]
 611     ##]
 612    ##]
 613   ##]
 614  ##]
 615 nqed.