matitaB/matita/contribs/ng_assembly2/emulator/status/IP2022_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/IP2022_status_base.ma".
  24
  25 (* *********************************** *)
  26 (* STATUS INTERNO DEL PROCESSORE (ALU) *)
  27 (* *********************************** *)
  28
  29 nlemma aluIP2022_destruct_1 :
  30 ∀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.
  31  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  32  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  33  x1 = y1.
  34  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  35  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  36  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  37                 with [ mk_alu_IP2022 a _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  38  nrewrite < H;
  39  nnormalize;
  40  napply refl_eq.
  41 nqed.
  42
  43 nlemma aluIP2022_destruct_2 :
  44 ∀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.
  45  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  46  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  47  x2 = y2.
  48  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  49  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  50  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  51                 with [ mk_alu_IP2022 _ a _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  52  nrewrite < H;
  53  nnormalize;
  54  napply refl_eq.
  55 nqed.
  56
  57 nlemma aluIP2022_destruct_3 :
  58 ∀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.
  59  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  60  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  61  x3 = y3.
  62  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  63  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  64  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  65                 with [ mk_alu_IP2022 _ _ a _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  66  nrewrite < H;
  67  nnormalize;
  68  napply refl_eq.
  69 nqed.
  70
  71 nlemma aluIP2022_destruct_4 :
  72 ∀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.
  73  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  74  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  75  x4 = y4.
  76  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  77  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  78  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  79                 with [ mk_alu_IP2022 _ _ _ a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  80  nrewrite < H;
  81  nnormalize;
  82  napply refl_eq.
  83 nqed.
  84
  85 nlemma aluIP2022_destruct_5 :
  86 ∀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.
  87  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  88  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  89  x5 = y5.
  90  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  91  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  92  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  93                 with [ mk_alu_IP2022 _ _ _ _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
  94  nrewrite < H;
  95  nnormalize;
  96  napply refl_eq.
  97 nqed.
  98
  99 nlemma aluIP2022_destruct_6 :
 100 ∀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.
 101  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 102  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 103  x6 = y6.
 104  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 105  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 106  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 107                 with [ mk_alu_IP2022 _ _ _ _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x6 = a ]);
 108  nrewrite < H;
 109  nnormalize;
 110  napply refl_eq.
 111 nqed.
 112
 113 nlemma aluIP2022_destruct_7 :
 114 ∀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.
 115  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 116  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 117  x7 = y7.
 118  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 119  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 120  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 121                 with [ mk_alu_IP2022 _ _ _ _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x7 = a ]);
 122  nrewrite < H;
 123  nnormalize;
 124  napply refl_eq.
 125 nqed.
 126
 127 nlemma aluIP2022_destruct_8 :
 128 ∀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.
 129  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 130  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 131  x8 = y8.
 132  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 133  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 134  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 135                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x8 = a ]);
 136  nrewrite < H;
 137  nnormalize;
 138  napply refl_eq.
 139 nqed.
 140
 141 nlemma aluIP2022_destruct_9 :
 142 ∀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.
 143  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 144  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 145  x9 = y9.
 146  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 147  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 148  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 149                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x9 = a ]);
 150  nrewrite < H;
 151  nnormalize;
 152  napply refl_eq.
 153 nqed.
 154
 155 nlemma aluIP2022_destruct_10 :
 156 ∀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.
 157  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 158  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 159  x10 = y10.
 160  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 161  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 162  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 163                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x10 = a ]);
 164  nrewrite < H;
 165  nnormalize;
 166  napply refl_eq.
 167 nqed.
 168
 169 nlemma aluIP2022_destruct_11 :
 170 ∀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.
 171  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 172  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 173  x11 = y11.
 174  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 175  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 176  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 177                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x11 = a ]);
 178  nrewrite < H;
 179  nnormalize;
 180  napply refl_eq.
 181 nqed.
 182
 183 nlemma aluIP2022_destruct_12 :
 184 ∀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.
 185  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 186  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 187  x12 = y12.
 188  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 189  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 190  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 191                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x12 = a ]);
 192  nrewrite < H;
 193  nnormalize;
 194  napply refl_eq.
 195 nqed.
 196
 197 nlemma aluIP2022_destruct_13 :
 198 ∀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.
 199  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 200  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 201  x13 = y13.
 202  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 203  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 204  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 205                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x13 = a ]);
 206  nrewrite < H;
 207  nnormalize;
 208  napply refl_eq.
 209 nqed.
 210
 211 nlemma aluIP2022_destruct_14 :
 212 ∀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.
 213  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 214  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 215  x14 = y14.
 216  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 217  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 218  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 219                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x14 = a ]);
 220  nrewrite < H;
 221  nnormalize;
 222  napply refl_eq.
 223 nqed.
 224
 225 nlemma aluIP2022_destruct_15 :
 226 ∀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.
 227  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 228  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 229  x15 = y15.
 230  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 231  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 232  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 233                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x15 = a ]);
 234  nrewrite < H;
 235  nnormalize;
 236  napply refl_eq.
 237 nqed.
 238
 239 nlemma aluIP2022_destruct_16 :
 240 ∀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.
 241  mk_alu_IP2022 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 242  mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 243  x16 = y16.
 244  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 245  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 246  nchange with (match mk_alu_IP2022 y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 247                 with [ mk_alu_IP2022 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x16 = a ]);
 248  nrewrite < H;
 249  nnormalize;
 250  napply refl_eq.
 251 nqed.
 252
 253 (* !!! ci mette troppo tempo a compilare *)
 254 naxiom eq_to_eqaluIP2022 : ∀alu1,alu2.alu1 = alu2 → eq_IP2022_alu alu1 alu2 = true.
 255 (* #alu1; ncases alu1;
 256  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 257  #alu2; ncases alu2;
 258  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 259  nrewrite > (aluIP2022_destruct_1 … H);
 260  nrewrite > (aluIP2022_destruct_2 … H);
 261  nrewrite > (aluIP2022_destruct_3 … H);
 262  nrewrite > (aluIP2022_destruct_4 … H);
 263  nrewrite > (aluIP2022_destruct_5 … H);
 264  nrewrite > (aluIP2022_destruct_6 … H);
 265  nrewrite > (aluIP2022_destruct_7 … H);
 266  nrewrite > (aluIP2022_destruct_8 … H);
 267  nrewrite > (aluIP2022_destruct_9 … H);
 268  nrewrite > (aluIP2022_destruct_10 … H);
 269  nrewrite > (aluIP2022_destruct_11 … H);
 270  nrewrite > (aluIP2022_destruct_12 … H);
 271  nrewrite > (aluIP2022_destruct_13 … H);
 272  nrewrite > (aluIP2022_destruct_14 … H);
 273  nrewrite > (aluIP2022_destruct_15 … H);
 274  nrewrite > (aluIP2022_destruct_16 … H);
 275  nchange with (
 276  ((eqc ? y1 y1) ⊗ (eqc ? y2 y2) ⊗ (eqc ? y3 y3) ⊗ (eqc ? y4 y4) ⊗
 277   (eqc ? y5 y5) ⊗ (eqc ? y6 y6) ⊗ (eqc ? y7 y7) ⊗ (eqc ? y8 y8) ⊗
 278   (eqc ? y9 y9) ⊗ (eqc ? y10 y10) ⊗ (eqc ? y11 y11) ⊗ (eqc ? y12 y12) ⊗
 279   (eqc ? y13 y13) ⊗ (eqc ? y14 y14) ⊗ (eqc ? y15 y15) ⊗ (eqc ? y16 y16)) = true);
 280  nrewrite > (eq_to_eqc ? y1 y1 (refl_eq …));
 281  nrewrite > (eq_to_eqc ? y2 y2 (refl_eq …));
 282  nrewrite > (eq_to_eqc ? y3 y3 (refl_eq …));
 283  nrewrite > (eq_to_eqc ? y4 y4 (refl_eq …));
 284  nrewrite > (eq_to_eqc ? y5 y5 (refl_eq …));
 285  nrewrite > (eq_to_eqc ? y6 y6 (refl_eq …));
 286  nrewrite > (eq_to_eqc ? y7 y7 (refl_eq …));
 287  nrewrite > (eq_to_eqc ? y8 y8 (refl_eq …));
 288  nrewrite > (eq_to_eqc ? y9 y9 (refl_eq …));
 289  nrewrite > (eq_to_eqc ? y10 y10 (refl_eq …));
 290  nrewrite > (eq_to_eqc ? y11 y11 (refl_eq …));
 291  nrewrite > (eq_to_eqc ? y12 y12 (refl_eq …));
 292  nrewrite > (eq_to_eqc ? y13 y13 (refl_eq …));
 293  nrewrite > (eq_to_eqc ? y14 y14 (refl_eq …));
 294  nrewrite > (eq_to_eqc ? y15 y15 (refl_eq …));
 295  nrewrite > (eq_to_eqc ? y16 y16 (refl_eq …));
 296  napply refl_eq.
 297 nqed.*)
 298
 299 nlemma neqaluIP2022_to_neq : ∀alu1,alu2.eq_IP2022_alu alu1 alu2 = false → alu1 ≠ alu2.
 300  #s1; #s2; #H;
 301  napply (not_to_not (s1 = s2) (eq_IP2022_alu s1 s2 = true) …);
 302  ##[ ##1: napply (eq_to_eqaluIP2022 s1 s2)
 303  ##| ##2: napply (eqfalse_to_neqtrue … H)
 304  ##]
 305 nqed.
 306
 307 nlemma eqaluIP2022_to_eq : ∀alu1,alu2.eq_IP2022_alu alu1 alu2 = true → alu1 = alu2.
 308  #alu1; ncases alu1;
 309  #z1; #z2; #z3; #z4; #z5; #z6; #z7; #z8; #z9; #z10; #z11; #z12; #z13; #z14; #z15; #z16;
 310  #alu2; ncases alu2;
 311  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 312  nchange in H:(%) with (
 313  ((eqc ? z1 y1) ⊗ (eqc ? z2 y2) ⊗ (eqc ? z3 y3) ⊗ (eqc ? z4 y4) ⊗
 314   (eqc ? z5 y5) ⊗ (eqc ? z6 y6) ⊗ (eqc ? z7 y7) ⊗ (eqc ? z8 y8) ⊗
 315   (eqc ? z9 y9) ⊗ (eqc ? z10 y10) ⊗ (eqc ? z11 y11) ⊗ (eqc ? z12 y12) ⊗
 316   (eqc ? z13 y13) ⊗ (eqc ? z14 y14) ⊗ (eqc ? z15 y15) ⊗ (eqc ? z16 y16)) = true);
 317  nrewrite > (eqc_to_eq … (andb_true_true_r … H));
 318  nletin H1 ≝ (andb_true_true_l … H);
 319  nrewrite > (eqc_to_eq … (andb_true_true_r … (andb_true_true_l … H)));
 320  nletin H2 ≝ (andb_true_true_l … H1);
 321  nrewrite > (eqc_to_eq … (andb_true_true_r … H2));
 322  nletin H3 ≝ (andb_true_true_l … H2);
 323  nrewrite > (eqc_to_eq … (andb_true_true_r … H3));
 324  nletin H4 ≝ (andb_true_true_l … H3);
 325  nrewrite > (eqc_to_eq … (andb_true_true_r … H4));
 326  nletin H5 ≝ (andb_true_true_l … H4);
 327  nrewrite > (eqc_to_eq … (andb_true_true_r … H5));
 328  nletin H6 ≝ (andb_true_true_l … H5);
 329  nrewrite > (eqc_to_eq … (andb_true_true_r … H6));
 330  nletin H7 ≝ (andb_true_true_l … H6);
 331  nrewrite > (eqc_to_eq … (andb_true_true_r … H7));
 332  nletin H8 ≝ (andb_true_true_l … H7);
 333  nrewrite > (eqc_to_eq … (andb_true_true_r … H8));
 334  nletin H9 ≝ (andb_true_true_l … H8);
 335  nrewrite > (eqc_to_eq … (andb_true_true_r … H9));
 336  nletin H10 ≝ (andb_true_true_l … H9);
 337  nrewrite > (eqc_to_eq … (andb_true_true_r … H10));
 338  nletin H11 ≝ (andb_true_true_l … H10);
 339  nrewrite > (eqc_to_eq … (andb_true_true_r … H11));
 340  nletin H12 ≝ (andb_true_true_l … H11);
 341  nrewrite > (eqc_to_eq … (andb_true_true_r … H12));
 342  nletin H13 ≝ (andb_true_true_l … H12);
 343  nrewrite > (eqc_to_eq … (andb_true_true_r … H13));
 344  nletin H14 ≝ (andb_true_true_l … H13);
 345  nrewrite > (eqc_to_eq … (andb_true_true_r … H14));
 346  nrewrite > (eqc_to_eq … (andb_true_true_l … H14));
 347  napply refl_eq.
 348 nqed.
 349
 350 nlemma neq_to_neqaluIP2022 : ∀alu1,alu2.alu1 ≠ alu2 → eq_IP2022_alu alu1 alu2 = false.
 351  #s1; #s2; #H;
 352  napply (neqtrue_to_eqfalse (eq_IP2022_alu s1 s2));
 353  napply (not_to_not (eq_IP2022_alu s1 s2 = true) (s1 = s2) ? H);
 354  napply (eqaluIP2022_to_eq s1 s2).
 355 nqed.
 356
 357 nlemma decidable_aluIP2022 : ∀x,y:alu_IP2022.decidable (x = y).
 358  #x; #y; nnormalize;
 359  napply (or2_elim (eq_IP2022_alu x y = true) (eq_IP2022_alu x y = false) ? (decidable_bexpr ?));
 360  ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqaluIP2022_to_eq … H))
 361  ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqaluIP2022_to_neq … H))
 362  ##]
 363 nqed.
 364
 365 (* !!! ci mette troppo tempo a compilare *)
 366 naxiom symmetric_eqaluIP2022 : symmetricT alu_IP2022 bool eq_IP2022_alu.
 367 (* #alu1; ncases alu1;
 368  #z1; #z2; #z3; #z4; #z5; #z6; #z7; #z8; #z9; #z10; #z11; #z12; #z13; #z14; #z15; #z16;
 369  #alu2; ncases alu2;
 370  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 371  nchange with (
 372   ((eqc ? z1 y1) ⊗ (eqc ? z2 y2) ⊗ (eqc ? z3 y3) ⊗ (eqc ? z4 y4) ⊗
 373   (eqc ? z5 y5) ⊗ (eqc ? z6 y6) ⊗ (eqc ? z7 y7) ⊗ (eqc ? z8 y8) ⊗
 374   (eqc ? z9 y9) ⊗ (eqc ? z10 y10) ⊗ (eqc ? z11 y11) ⊗ (eqc ? z12 y12) ⊗
 375   (eqc ? z13 y13) ⊗ (eqc ? z14 y14) ⊗ (eqc ? z15 y15) ⊗ (eqc ? z16 y16)) =
 376   ((eqc ? y1 z1) ⊗ (eqc ? y2 z2) ⊗ (eqc ? y3 z3) ⊗ (eqc ? y4 z4) ⊗
 377   (eqc ? y5 z5) ⊗ (eqc ? y6 z6) ⊗ (eqc ? y7 z7) ⊗ (eqc ? y8 z8) ⊗
 378   (eqc ? y9 z9) ⊗ (eqc ? y10 z10) ⊗ (eqc ? y11 z11) ⊗ (eqc ? y12 z12) ⊗
 379   (eqc ? y13 z13) ⊗ (eqc ? y14 z14) ⊗ (eqc ? y15 z15) ⊗ (eqc ? y16 z16)));
 380  nrewrite > (symmetric_eqc ? z1 y1);
 381  nrewrite > (symmetric_eqc ? z2 y2);
 382  nrewrite > (symmetric_eqc ? z3 y3);
 383  nrewrite > (symmetric_eqc ? z4 y4);
 384  nrewrite > (symmetric_eqc ? z5 y5);
 385  nrewrite > (symmetric_eqc ? z6 y6);
 386  nrewrite > (symmetric_eqc ? z7 y7);
 387  nrewrite > (symmetric_eqc ? z8 y8);
 388  nrewrite > (symmetric_eqc ? z9 y9);
 389  nrewrite > (symmetric_eqc ? z10 y10);
 390  nrewrite > (symmetric_eqc ? z11 y11);
 391  nrewrite > (symmetric_eqc ? z12 y12);
 392  nrewrite > (symmetric_eqc ? z13 y13);
 393  nrewrite > (symmetric_eqc ? z14 y14);
 394  nrewrite > (symmetric_eqc ? z15 y15);
 395  nrewrite > (symmetric_eqc ? z16 y16);
 396  napply refl_eq.
 397 nqed.*)
 398
 399 nlemma aluIP2022_is_comparable : comparable.
 400  @ alu_IP2022
 401   ##[ napply (mk_alu_IP2022 (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
 402                             (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
 403                             (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
 404                             (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?))
 405   ##| napply forall_IP2022_alu
 406   ##| napply eq_IP2022_alu
 407   ##| napply eqaluIP2022_to_eq
 408   ##| napply eq_to_eqaluIP2022
 409   ##| napply neqaluIP2022_to_neq
 410   ##| napply neq_to_neqaluIP2022
 411   ##| napply decidable_aluIP2022
 412   ##| napply symmetric_eqaluIP2022
 413   ##]
 414 nqed.
 415
 416 unification hint 0 ≔ ⊢ carr aluIP2022_is_comparable ≡ alu_IP2022.