helm/software/matita/contribs/ng_assembly2/emulator/memory/memory_struct.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/memory/memory_struct_base.ma".
  24
  25 (* **************** *)
  26 (* TIPO ARRAY DA 16 *)
  27 (* **************** *)
  28
  29 nlemma ar16_destruct_1 :
  30 ∀T.
  31 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  32 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  33  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  34  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  35  x1 = y1.
  36  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  37  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  38  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  39                 with [ mk_Array16T a _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x1 = a ]);
  40  nrewrite < H;
  41  nnormalize;
  42  napply refl_eq.
  43 nqed.
  44
  45 nlemma ar16_destruct_2 :
  46 ∀T.
  47 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  48 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  49  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  50  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  51  x2 = y2.
  52  #T; #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_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  55                 with [ mk_Array16T _ a _ _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x2 = a ]);
  56  nrewrite < H;
  57  nnormalize;
  58  napply refl_eq.
  59 nqed.
  60
  61 nlemma ar16_destruct_3 :
  62 ∀T.
  63 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  64 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  65  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  66  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  67  x3 = y3.
  68  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  69  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  70  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  71                 with [ mk_Array16T _ _ a _ _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x3 = a ]);
  72  nrewrite < H;
  73  nnormalize;
  74  napply refl_eq.
  75 nqed.
  76
  77 nlemma ar16_destruct_4 :
  78 ∀T.
  79 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  80 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  81  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  82  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  83  x4 = y4.
  84  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
  85  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
  86  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
  87                 with [ mk_Array16T _ _ _ a _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x4 = a ]);
  88  nrewrite < H;
  89  nnormalize;
  90  napply refl_eq.
  91 nqed.
  92
  93 nlemma ar16_destruct_5 :
  94 ∀T.
  95 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
  96 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
  97  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
  98  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
  99  x5 = y5.
 100  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 101  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 102  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 103                 with [ mk_Array16T _ _ _ _ a _ _ _ _ _ _ _ _ _ _ _ ⇒ x5 = a ]);
 104  nrewrite < H;
 105  nnormalize;
 106  napply refl_eq.
 107 nqed.
 108
 109 nlemma ar16_destruct_6 :
 110 ∀T.
 111 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 112 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 113  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 114  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 115  x6 = y6.
 116  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 117  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 118  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 119                 with [ mk_Array16T _ _ _ _ _ a _ _ _ _ _ _ _ _ _ _ ⇒ x6 = a ]);
 120  nrewrite < H;
 121  nnormalize;
 122  napply refl_eq.
 123 nqed.
 124
 125 nlemma ar16_destruct_7 :
 126 ∀T.
 127 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 128 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 129  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 130  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 131  x7 = y7.
 132  #T; #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_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 135                 with [ mk_Array16T _ _ _ _ _ _ a _ _ _ _ _ _ _ _ _ ⇒ x7 = a ]);
 136  nrewrite < H;
 137  nnormalize;
 138  napply refl_eq.
 139 nqed.
 140
 141 nlemma ar16_destruct_8 :
 142 ∀T.
 143 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 144 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 145  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 146  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 147  x8 = y8.
 148  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 149  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 150  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 151                 with [ mk_Array16T _ _ _ _ _ _ _ a _ _ _ _ _ _ _ _ ⇒ x8 = a ]);
 152  nrewrite < H;
 153  nnormalize;
 154  napply refl_eq.
 155 nqed.
 156
 157 nlemma ar16_destruct_9 :
 158 ∀T.
 159 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 160 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 161  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 162  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 163  x9 = y9.
 164  #T; #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_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 167                 with [ mk_Array16T _ _ _ _ _ _ _ _ a _ _ _ _ _ _ _ ⇒ x9 = a ]);
 168  nrewrite < H;
 169  nnormalize;
 170  napply refl_eq.
 171 nqed.
 172
 173 nlemma ar16_destruct_10 :
 174 ∀T.
 175 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 176 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 177  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 178  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 179  x10 = y10.
 180  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 181  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 182  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 183                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ a _ _ _ _ _ _ ⇒ x10 = a ]);
 184  nrewrite < H;
 185  nnormalize;
 186  napply refl_eq.
 187 nqed.
 188
 189 nlemma ar16_destruct_11 :
 190 ∀T.
 191 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 192 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 193  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 194  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 195  x11 = y11.
 196  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 197  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 198  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 199                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ a _ _ _ _ _ ⇒ x11 = a ]);
 200  nrewrite < H;
 201  nnormalize;
 202  napply refl_eq.
 203 nqed.
 204
 205 nlemma ar16_destruct_12 :
 206 ∀T.
 207 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 208 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 209  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 210  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 211  x12 = y12.
 212  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 213  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 214  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 215                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ a _ _ _ _ ⇒ x12 = a ]);
 216  nrewrite < H;
 217  nnormalize;
 218  napply refl_eq.
 219 nqed.
 220
 221 nlemma ar16_destruct_13 :
 222 ∀T.
 223 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 224 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 225  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 226  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 227  x13 = y13.
 228  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 229  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 230  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 231                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ a _ _ _ ⇒ x13 = a ]);
 232  nrewrite < H;
 233  nnormalize;
 234  napply refl_eq.
 235 nqed.
 236
 237 nlemma ar16_destruct_14 :
 238 ∀T.
 239 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 240 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 241  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 242  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 243  x14 = y14.
 244  #T; #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_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 247                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ a _ _ ⇒ x14 = a ]);
 248  nrewrite < H;
 249  nnormalize;
 250  napply refl_eq.
 251 nqed.
 252
 253 nlemma ar16_destruct_15 :
 254 ∀T.
 255 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 256 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 257  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 258  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 259  x15 = y15.
 260  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 261  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 262  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 263                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ _ a _ ⇒ x15 = a ]);
 264  nrewrite < H;
 265  nnormalize;
 266  napply refl_eq.
 267 nqed.
 268
 269 nlemma ar16_destruct_16 :
 270 ∀T.
 271 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 272 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 273  mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 =
 274  mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16 →
 275  x16 = y16.
 276  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 277  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H;
 278  nchange with (match mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16
 279                 with [ mk_Array16T _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ a ⇒ x16 = a ]);
 280  nrewrite < H;
 281  nnormalize;
 282  napply refl_eq.
 283 nqed.
 284
 285 nlemma symmetric_eqar16 :
 286 ∀T.∀f:T → T → bool.
 287  (symmetricT T bool f) →
 288  (symmetricT (Array16T T) bool (eq_ar16 T f)).
 289  #T; #f; #H;
 290  #alu1; ncases alu1;
 291  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 292  #alu2; ncases alu2;
 293  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 294  nchange with (
 295   ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
 296    (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8) ⊗
 297    (f x9 y9) ⊗ (f x10 y10) ⊗ (f x11 y11) ⊗ (f x12 y12) ⊗
 298    (f x13 y13) ⊗ (f x14 y14) ⊗ (f x15 y15) ⊗ (f x16 y16)) =
 299   ((f y1 x1) ⊗ (f y2 x2) ⊗ (f y3 x3) ⊗ (f y4 x4) ⊗
 300    (f y5 x5) ⊗ (f y6 x6) ⊗ (f y7 x7) ⊗ (f y8 x8) ⊗
 301    (f y9 x9) ⊗ (f y10 x10) ⊗ (f y11 x11) ⊗ (f y12 x12) ⊗
 302    (f y13 x13) ⊗ (f y14 x14) ⊗ (f y15 x15) ⊗ (f y16 x16)));
 303  nrewrite > (H x1 y1);
 304  nrewrite > (H x2 y2);
 305  nrewrite > (H x3 y3);
 306  nrewrite > (H x4 y4);
 307  nrewrite > (H x5 y5);
 308  nrewrite > (H x6 y6);
 309  nrewrite > (H x7 y7);
 310  nrewrite > (H x8 y8);
 311  nrewrite > (H x9 y9);
 312  nrewrite > (H x10 y10);
 313  nrewrite > (H x11 y11);
 314  nrewrite > (H x12 y12);
 315  nrewrite > (H x13 y13);
 316  nrewrite > (H x14 y14);
 317  nrewrite > (H x15 y15);
 318  nrewrite > (H x16 y16);
 319  napply refl_eq.
 320 nqed.
 321
 322 nlemma eqar16_to_eq :
 323 ∀T.∀f:T → T → bool.
 324  (∀x,y.(f x y = true) → (x = y)) →
 325  (∀a1,a2:Array16T T.(eq_ar16 T f a1 a2 = true) → (a1 = a2)).
 326  #T; #f; #H;
 327  #alu1; ncases alu1;
 328  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 329  #alu2; ncases alu2;
 330  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H1;
 331  nchange in H1:(%) with (
 332   ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
 333    (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8) ⊗
 334    (f x9 y9) ⊗ (f x10 y10) ⊗ (f x11 y11) ⊗ (f x12 y12) ⊗
 335    (f x13 y13) ⊗ (f x14 y14) ⊗ (f x15 y15) ⊗ (f x16 y16)) = true);
 336  nrewrite > (H … (andb_true_true_r … H1));
 337  nletin H2 ≝ (andb_true_true_l … H1);
 338  nrewrite > (H … (andb_true_true_r … H2));
 339  nletin H3 ≝ (andb_true_true_l … H2);
 340  nrewrite > (H … (andb_true_true_r … H3));
 341  nletin H4 ≝ (andb_true_true_l … H3);
 342  nrewrite > (H … (andb_true_true_r … H4));
 343  nletin H5 ≝ (andb_true_true_l … H4);
 344  nrewrite > (H … (andb_true_true_r … H5));
 345  nletin H6 ≝ (andb_true_true_l … H5);
 346  nrewrite > (H … (andb_true_true_r … H6));
 347  nletin H7 ≝ (andb_true_true_l … H6);
 348  nrewrite > (H … (andb_true_true_r … H7));
 349  nletin H8 ≝ (andb_true_true_l … H7);
 350  nrewrite > (H … (andb_true_true_r … H8));
 351  nletin H9 ≝ (andb_true_true_l … H8);
 352  nrewrite > (H … (andb_true_true_r … H9));
 353  nletin H10 ≝ (andb_true_true_l … H9);
 354  nrewrite > (H … (andb_true_true_r … H10));
 355  nletin H11 ≝ (andb_true_true_l … H10);
 356  nrewrite > (H … (andb_true_true_r … H11));
 357  nletin H12 ≝ (andb_true_true_l … H11);
 358  nrewrite > (H … (andb_true_true_r … H12));
 359  nletin H13 ≝ (andb_true_true_l … H12);
 360  nrewrite > (H … (andb_true_true_r … H13));
 361  nletin H14 ≝ (andb_true_true_l … H13);
 362  nrewrite > (H … (andb_true_true_r … H14));
 363  nletin H15 ≝ (andb_true_true_l … H14);
 364  nrewrite > (H … (andb_true_true_r … H15));
 365  nrewrite > (H … (andb_true_true_l … H15));
 366  napply refl_eq.
 367 nqed.
 368
 369 nlemma eq_to_eqar16 :
 370 ∀T.∀f:T → T → bool.
 371  (∀x,y.(x = y) → (f x y = true)) →
 372  (∀a1,a2:Array16T T.(a1 = a2) → (eq_ar16 T f a1 a2 = true)).
 373  #T; #f; #H;
 374  #alu1; ncases alu1;
 375  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 376  #alu2; ncases alu2;
 377  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16; #H1;
 378  nrewrite > (ar16_destruct_1 … H1);
 379  nrewrite > (ar16_destruct_2 … H1);
 380  nrewrite > (ar16_destruct_3 … H1);
 381  nrewrite > (ar16_destruct_4 … H1);
 382  nrewrite > (ar16_destruct_5 … H1);
 383  nrewrite > (ar16_destruct_6 … H1);
 384  nrewrite > (ar16_destruct_7 … H1);
 385  nrewrite > (ar16_destruct_8 … H1);
 386  nrewrite > (ar16_destruct_9 … H1);
 387  nrewrite > (ar16_destruct_10 … H1);
 388  nrewrite > (ar16_destruct_11 … H1);
 389  nrewrite > (ar16_destruct_12 … H1);
 390  nrewrite > (ar16_destruct_13 … H1);
 391  nrewrite > (ar16_destruct_14 … H1);
 392  nrewrite > (ar16_destruct_15 … H1);
 393  nrewrite > (ar16_destruct_16 … H1);
 394  nchange with (
 395   ((f y1 y1) ⊗ (f y2 y2) ⊗ (f y3 y3) ⊗ (f y4 y4) ⊗
 396    (f y5 y5) ⊗ (f y6 y6) ⊗ (f y7 y7) ⊗ (f y8 y8) ⊗
 397    (f y9 y9) ⊗ (f y10 y10) ⊗ (f y11 y11) ⊗ (f y12 y12) ⊗
 398    (f y13 y13) ⊗ (f y14 y14) ⊗ (f y15 y15) ⊗ (f y16 y16)) = true);
 399  nrewrite > (H … (refl_eq …));
 400  nrewrite > (H … (refl_eq …));
 401  nrewrite > (H … (refl_eq …));
 402  nrewrite > (H … (refl_eq …));
 403  nrewrite > (H … (refl_eq …));
 404  nrewrite > (H … (refl_eq …));
 405  nrewrite > (H … (refl_eq …));
 406  nrewrite > (H … (refl_eq …));
 407  nrewrite > (H … (refl_eq …));
 408  nrewrite > (H … (refl_eq …));
 409  nrewrite > (H … (refl_eq …));
 410  nrewrite > (H … (refl_eq …));
 411  nrewrite > (H … (refl_eq …));
 412  nrewrite > (H … (refl_eq …));
 413  nrewrite > (H … (refl_eq …));
 414  nrewrite > (H … (refl_eq …));
 415  napply refl_eq.
 416 nqed.
 417
 418 nlemma decidable_ar16_aux1 :
 419 ∀T.
 420 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 421 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 422  (x1 ≠ y1) →
 423  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 424  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 425  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 426  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 427  nnormalize; #H; #H1;
 428  napply (H (ar16_destruct_1 … H1)).
 429 nqed.
 430
 431 nlemma decidable_ar16_aux2 :
 432 ∀T.
 433 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 434 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 435  (x2 ≠ y2) →
 436  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 437  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 438  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 439  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 440  nnormalize; #H; #H1;
 441  napply (H (ar16_destruct_2 … H1)).
 442 nqed.
 443
 444 nlemma decidable_ar16_aux3 :
 445 ∀T.
 446 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 447 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 448  (x3 ≠ y3) →
 449  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 450  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 451  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 452  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 453  nnormalize; #H; #H1;
 454  napply (H (ar16_destruct_3 … H1)).
 455 nqed.
 456
 457 nlemma decidable_ar16_aux4 :
 458 ∀T.
 459 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 460 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 461  (x4 ≠ y4) →
 462  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 463  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 464  #T; #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 (ar16_destruct_4 … H1)).
 468 nqed.
 469
 470 nlemma decidable_ar16_aux5 :
 471 ∀T.
 472 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 473 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 474  (x5 ≠ y5) →
 475  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 476  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 477  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 478  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 479  nnormalize; #H; #H1;
 480  napply (H (ar16_destruct_5 … H1)).
 481 nqed.
 482
 483 nlemma decidable_ar16_aux6 :
 484 ∀T.
 485 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 486 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 487  (x6 ≠ y6) →
 488  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 489  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 490  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 491  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 492  nnormalize; #H; #H1;
 493  napply (H (ar16_destruct_6 … H1)).
 494 nqed.
 495
 496 nlemma decidable_ar16_aux7 :
 497 ∀T.
 498 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 499 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 500  (x7 ≠ y7) →
 501  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 502  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 503  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 504  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 505  nnormalize; #H; #H1;
 506  napply (H (ar16_destruct_7 … H1)).
 507 nqed.
 508
 509 nlemma decidable_ar16_aux8 :
 510 ∀T.
 511 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 512 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 513  (x8 ≠ y8) →
 514  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 515  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 516  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 517  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 518  nnormalize; #H; #H1;
 519  napply (H (ar16_destruct_8 … H1)).
 520 nqed.
 521
 522 nlemma decidable_ar16_aux9 :
 523 ∀T.
 524 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 525 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 526  (x9 ≠ y9) →
 527  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 528  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 529  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 530  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 531  nnormalize; #H; #H1;
 532  napply (H (ar16_destruct_9 … H1)).
 533 nqed.
 534
 535 nlemma decidable_ar16_aux10 :
 536 ∀T.
 537 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 538 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 539  (x10 ≠ y10) →
 540  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 541  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 542  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 543  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 544  nnormalize; #H; #H1;
 545  napply (H (ar16_destruct_10 … H1)).
 546 nqed.
 547
 548 nlemma decidable_ar16_aux11 :
 549 ∀T.
 550 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 551 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 552  (x11 ≠ y11) →
 553  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 554  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 555  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 556  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 557  nnormalize; #H; #H1;
 558  napply (H (ar16_destruct_11 … H1)).
 559 nqed.
 560
 561 nlemma decidable_ar16_aux12 :
 562 ∀T.
 563 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 564 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 565  (x12 ≠ y12) →
 566  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 567  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 568  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 569  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 570  nnormalize; #H; #H1;
 571  napply (H (ar16_destruct_12 … H1)).
 572 nqed.
 573
 574 nlemma decidable_ar16_aux13 :
 575 ∀T.
 576 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 577 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 578  (x13 ≠ y13) →
 579  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 580  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 581  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 582  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 583  nnormalize; #H; #H1;
 584  napply (H (ar16_destruct_13 … H1)).
 585 nqed.
 586
 587 nlemma decidable_ar16_aux14 :
 588 ∀T.
 589 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 590 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 591  (x14 ≠ y14) →
 592  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 593  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 594  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 595  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 596  nnormalize; #H; #H1;
 597  napply (H (ar16_destruct_14 … H1)).
 598 nqed.
 599
 600 nlemma decidable_ar16_aux15 :
 601 ∀T.
 602 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 603 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 604  (x15 ≠ y15) →
 605  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 606  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 607  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 608  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 609  nnormalize; #H; #H1;
 610  napply (H (ar16_destruct_15 … H1)).
 611 nqed.
 612
 613 nlemma decidable_ar16_aux16 :
 614 ∀T.
 615 ∀x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15,x16:T.
 616 ∀y1,y2,y3,y4,y5,y6,y7,y8,y9,y10,y11,y12,y13,y14,y15,y16:T.
 617  (x16 ≠ y16) →
 618  (mk_Array16T T x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16) ≠
 619  (mk_Array16T T y1 y2 y3 y4 y5 y6 y7 y8 y9 y10 y11 y12 y13 y14 y15 y16).
 620  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 621  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 622  nnormalize; #H; #H1;
 623  napply (H (ar16_destruct_16 … H1)).
 624 nqed.
 625
 626 nlemma decidable_ar16 :
 627 ∀T.(∀x,y:T.decidable (x = y)) →
 628    (∀a1,a2:Array16T T.decidable (a1 = a2)).
 629  #T; #H;
 630  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #x9; #x10; #x11; #x12; #x13; #x14; #x15; #x16;
 631  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #y9; #y10; #y11; #y12; #y13; #y14; #y15; #y16;
 632  nnormalize;
 633  napply (or2_elim (? = ?) (? ≠ ?) ? (H x1 y1) …);
 634  ##[ ##2: #H1; napply (or2_intro2 … (decidable_ar16_aux1 T … H1))
 635  ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (H x2 y2) …);
 636   ##[ ##2: #H2; napply (or2_intro2 … (decidable_ar16_aux2 T … H2))
 637   ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H x3 y3) …);
 638    ##[ ##2: #H3; napply (or2_intro2 … (decidable_ar16_aux3 T … H3))
 639    ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (H x4 y4) …);
 640     ##[ ##2: #H4; napply (or2_intro2 … (decidable_ar16_aux4 T … H4))
 641     ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (H x5 y5) …);
 642      ##[ ##2: #H5; napply (or2_intro2 … (decidable_ar16_aux5 T … H5))
 643      ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (H x6 y6) …);
 644       ##[ ##2: #H6; napply (or2_intro2 … (decidable_ar16_aux6 T … H6))
 645       ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (H x7 y7) …);
 646        ##[ ##2: #H7; napply (or2_intro2 … (decidable_ar16_aux7 T … H7))
 647        ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (H x8 y8) …);
 648         ##[ ##2: #H8; napply (or2_intro2 … (decidable_ar16_aux8 T … H8))
 649         ##| ##1: #H8; napply (or2_elim (? = ?) (? ≠ ?) ? (H x9 y9) …);
 650          ##[ ##2: #H9; napply (or2_intro2 … (decidable_ar16_aux9 T … H9))
 651          ##| ##1: #H9; napply (or2_elim (? = ?) (? ≠ ?) ? (H x10 y10) …);
 652           ##[ ##2: #H10; napply (or2_intro2 … (decidable_ar16_aux10 T … H10))
 653           ##| ##1: #H10; napply (or2_elim (? = ?) (? ≠ ?) ? (H x11 y11) …);
 654            ##[ ##2: #H11; napply (or2_intro2 … (decidable_ar16_aux11 T … H11))
 655            ##| ##1: #H11; napply (or2_elim (? = ?) (? ≠ ?) ? (H x12 y12) …);
 656             ##[ ##2: #H12; napply (or2_intro2 … (decidable_ar16_aux12 T … H12))
 657             ##| ##1: #H12; napply (or2_elim (? = ?) (? ≠ ?) ? (H x13 y13) …);
 658              ##[ ##2: #H13; napply (or2_intro2 … (decidable_ar16_aux13 T … H13))
 659              ##| ##1: #H13; napply (or2_elim (? = ?) (? ≠ ?) ? (H x14 y14) …);
 660               ##[ ##2: #H14; napply (or2_intro2 … (decidable_ar16_aux14 T … H14))
 661               ##| ##1: #H14; napply (or2_elim (? = ?) (? ≠ ?) ? (H x15 y15) …);
 662                ##[ ##2: #H15; napply (or2_intro2 … (decidable_ar16_aux15 T … H15))
 663                ##| ##1: #H15; napply (or2_elim (? = ?) (? ≠ ?) ? (H x16 y16) …);
 664                 ##[ ##2: #H16; napply (or2_intro2 … (decidable_ar16_aux16 T … H16))
 665                 ##| ##1: #H16; nrewrite > H1; nrewrite > H2; nrewrite > H3; nrewrite > H4;
 666                       nrewrite > H5; nrewrite > H6; nrewrite > H7; nrewrite > H8;
 667                       nrewrite > H9; nrewrite > H10; nrewrite > H11; nrewrite > H12;
 668                       nrewrite > H13; nrewrite > H14; nrewrite > H15; nrewrite > H16;
 669                       napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
 670                 ##]
 671                ##]
 672               ##]
 673              ##]
 674             ##]
 675            ##]
 676           ##]
 677          ##]
 678         ##]
 679        ##]
 680       ##]
 681      ##]
 682     ##]
 683    ##]
 684   ##]
 685  ##]
 686 nqed.
 687
 688 (* !!! per brevita *)
 689 naxiom neqar16_to_neq :
 690 ∀T.∀f:T → T → bool.
 691  (∀x,y:T.f x y = false → x ≠ y) →
 692  (∀p1,p2:Array16T T.(eq_ar16 T f p1 p2 = false → p1 ≠ p2)).
 693
 694 (* !!! per brevita *)
 695 naxiom neq_to_neqar16 :
 696 ∀T.∀f:T → T → bool.
 697  (∀x,y:T.decidable (x = y)) →
 698  (∀x,y:T.x ≠ y → f x y = false) →
 699  (∀p1,p2:Array16T T.(p1 ≠ p2 → eq_ar16 T f p1 p2 = false)).
 700
 701 nlemma ar16_is_comparable : comparable → comparable.
 702  #T; @ (Array16T T)
 703   ##[ napply (mk_Array16T ? (zeroc T) (zeroc T) (zeroc T) (zeroc T)
 704                             (zeroc T) (zeroc T) (zeroc T) (zeroc T)
 705                             (zeroc T) (zeroc T) (zeroc T) (zeroc T)
 706                             (zeroc T) (zeroc T) (zeroc T) (zeroc T))
 707   ##| napply (λP.(forallc T)
 708               (λe1.(forallc T)
 709                (λe2.(forallc T)
 710                 (λe3.(forallc T)
 711                  (λe4.(forallc T)
 712                   (λe5.(forallc T)
 713                    (λe6.(forallc T)
 714                     (λe7.(forallc T)
 715                      (λe8.(forallc T)
 716                       (λe9.(forallc T)
 717                        (λe10.(forallc T)
 718                         (λe11.(forallc T)
 719                          (λe12.(forallc T)
 720                           (λe13.(forallc T)
 721                            (λe14.(forallc T)
 722                             (λe15.(forallc T)
 723                              (λe16.P (mk_Array16T T e1 e2 e3 e4 e5 e6 e7 e8 e9 e10 e11 e12 e13 e14 e15 e16))))))))))))))))))
 724   ##| napply (eq_ar16 … (eqc T))
 725   ##| napply eqar16_to_eq;
 726       napply (eqc_to_eq T)
 727   ##| napply eq_to_eqar16;
 728       napply (eq_to_eqc T)
 729   ##| napply neqar16_to_neq;
 730       napply (neqc_to_neq T)
 731   ##| napply neq_to_neqar16;
 732       ##[ napply (decidable_c T)
 733       ##| napply (neq_to_neqc T) ##]
 734   ##| napply decidable_ar16;
 735       napply (decidable_c T)
 736   ##| napply symmetric_eqar16;
 737       napply (symmetric_eqc T)
 738   ##]
 739 nqed.
 740
 741 unification hint 0 ≔ S: comparable ;
 742          T ≟ (carr S),
 743          X ≟ (ar16_is_comparable S)
 744  (*********************************************) ⊢
 745          carr X ≡ Array16T T.
 746
 747 (* *************** *)
 748 (* TIPO ARRAY DA 8 *)
 749 (* *************** *)
 750
 751 nlemma ar8_destruct_1 :
 752 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 753  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 754  x1 = y1.
 755  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 756  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 757                 with [ mk_Array8T a _ _ _ _ _ _ _ ⇒ x1 = a ]);
 758  nrewrite < H;
 759  nnormalize;
 760  napply refl_eq.
 761 nqed.
 762
 763 nlemma ar8_destruct_2 :
 764 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 765  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 766  x2 = y2.
 767  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 768  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 769                 with [ mk_Array8T _ a _ _ _ _ _ _ ⇒ x2 = a ]);
 770  nrewrite < H;
 771  nnormalize;
 772  napply refl_eq.
 773 nqed.
 774
 775 nlemma ar8_destruct_3 :
 776 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 777  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 778  x3 = y3.
 779  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 780  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 781                 with [ mk_Array8T _ _ a _ _ _ _ _ ⇒ x3 = a ]);
 782  nrewrite < H;
 783  nnormalize;
 784  napply refl_eq.
 785 nqed.
 786
 787 nlemma ar8_destruct_4 :
 788 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 789  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 790  x4 = y4.
 791  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 792  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 793                 with [ mk_Array8T _ _ _ a _ _ _ _ ⇒ x4 = a ]);
 794  nrewrite < H;
 795  nnormalize;
 796  napply refl_eq.
 797 nqed.
 798
 799 nlemma ar8_destruct_5 :
 800 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 801  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 802  x5 = y5.
 803  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 804  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 805                 with [ mk_Array8T _ _ _ _ a _ _ _ ⇒ x5 = a ]);
 806  nrewrite < H;
 807  nnormalize;
 808  napply refl_eq.
 809 nqed.
 810
 811 nlemma ar8_destruct_6 :
 812 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 813  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 814  x6 = y6.
 815  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 816  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 817                 with [ mk_Array8T _ _ _ _ _ a _ _ ⇒ x6 = a ]);
 818  nrewrite < H;
 819  nnormalize;
 820  napply refl_eq.
 821 nqed.
 822
 823 nlemma ar8_destruct_7 :
 824 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 825  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 826  x7 = y7.
 827  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 828  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 829                 with [ mk_Array8T _ _ _ _ _ _ a _ ⇒ x7 = a ]);
 830  nrewrite < H;
 831  nnormalize;
 832  napply refl_eq.
 833 nqed.
 834
 835 nlemma ar8_destruct_8 :
 836 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8:T.∀y1,y2,y3,y4,y5,y6,y7,y8:T.
 837  mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8 = mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8  →
 838  x8 = y8.
 839  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H;
 840  nchange with (match mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8
 841                 with [ mk_Array8T _ _ _ _ _ _ _ a ⇒ x8 = a ]);
 842  nrewrite < H;
 843  nnormalize;
 844  napply refl_eq.
 845 nqed.
 846
 847 nlemma symmetric_eqar8 :
 848 ∀T.∀f:T → T → bool.
 849  (symmetricT T bool f) →
 850  (symmetricT (Array8T T) bool (eq_ar8 T f)).
 851  #T; #f; #H;
 852  #alu1; ncases alu1;
 853  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 854  #alu2; ncases alu2;
 855  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 856  nchange with (
 857   ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
 858    (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8)) =
 859   ((f y1 x1) ⊗ (f y2 x2) ⊗ (f y3 x3) ⊗ (f y4 x4) ⊗
 860    (f y5 x5) ⊗ (f y6 x6) ⊗ (f y7 x7) ⊗ (f y8 x8)));
 861  nrewrite > (H x1 y1);
 862  nrewrite > (H x2 y2);
 863  nrewrite > (H x3 y3);
 864  nrewrite > (H x4 y4);
 865  nrewrite > (H x5 y5);
 866  nrewrite > (H x6 y6);
 867  nrewrite > (H x7 y7);
 868  nrewrite > (H x8 y8);
 869  napply refl_eq.
 870 nqed.
 871
 872 nlemma eqar8_to_eq :
 873 ∀T.∀f:T → T → bool.
 874  (∀x,y.(f x y = true) → (x = y)) →
 875  (∀a1,a2:Array8T T.(eq_ar8 T f a1 a2 = true) → (a1 = a2)).
 876  #T; #f; #H;
 877  #alu1; ncases alu1;
 878  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 879  #alu2; ncases alu2;
 880  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H1;
 881  nchange in H1:(%) with (
 882   ((f x1 y1) ⊗ (f x2 y2) ⊗ (f x3 y3) ⊗ (f x4 y4) ⊗
 883    (f x5 y5) ⊗ (f x6 y6) ⊗ (f x7 y7) ⊗ (f x8 y8)) = true);
 884  nrewrite > (H … (andb_true_true_r … H1));
 885  nletin H2 ≝ (andb_true_true_l … H1);
 886  nrewrite > (H … (andb_true_true_r … H2));
 887  nletin H3 ≝ (andb_true_true_l … H2);
 888  nrewrite > (H … (andb_true_true_r … H3));
 889  nletin H4 ≝ (andb_true_true_l … H3);
 890  nrewrite > (H … (andb_true_true_r … H4));
 891  nletin H5 ≝ (andb_true_true_l … H4);
 892  nrewrite > (H … (andb_true_true_r … H5));
 893  nletin H6 ≝ (andb_true_true_l … H5);
 894  nrewrite > (H … (andb_true_true_r … H6));
 895  nletin H7 ≝ (andb_true_true_l … H6);
 896  nrewrite > (H … (andb_true_true_r … H7));
 897  nrewrite > (H … (andb_true_true_l … H7));
 898  napply refl_eq.
 899 nqed.
 900
 901 nlemma eq_to_eqar8 :
 902 ∀T.∀f:T → T → bool.
 903  (∀x,y.(x = y) → (f x y = true)) →
 904  (∀a1,a2:Array8T T.(a1 = a2) → (eq_ar8 T f a1 a2 = true)).
 905  #T; #f; #H;
 906  #alu1; ncases alu1;
 907  #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
 908  #alu2; ncases alu2;
 909  #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8; #H1;
 910  nrewrite > (ar8_destruct_1 … H1);
 911  nrewrite > (ar8_destruct_2 … H1);
 912  nrewrite > (ar8_destruct_3 … H1);
 913  nrewrite > (ar8_destruct_4 … H1);
 914  nrewrite > (ar8_destruct_5 … H1);
 915  nrewrite > (ar8_destruct_6 … H1);
 916  nrewrite > (ar8_destruct_7 … H1);
 917  nrewrite > (ar8_destruct_8 … H1);
 918  nchange with (
 919   ((f y1 y1) ⊗ (f y2 y2) ⊗ (f y3 y3) ⊗ (f y4 y4) ⊗
 920    (f y5 y5) ⊗ (f y6 y6) ⊗ (f y7 y7) ⊗ (f y8 y8)) = true);
 921  nrewrite > (H … (refl_eq …));
 922  nrewrite > (H … (refl_eq …));
 923  nrewrite > (H … (refl_eq …));
 924  nrewrite > (H … (refl_eq …));
 925  nrewrite > (H … (refl_eq …));
 926  nrewrite > (H … (refl_eq …));
 927  nrewrite > (H … (refl_eq …));
 928  nrewrite > (H … (refl_eq …));
 929  napply refl_eq.
 930 nqed.
 931
 932 nlemma decidable_ar8_aux1 :
 933 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 934  (x1 ≠ y1) →
 935  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 936  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 937  nnormalize; #H; #H1;
 938  napply (H (ar8_destruct_1 … H1)).
 939 nqed.
 940
 941 nlemma decidable_ar8_aux2 :
 942 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 943  (x2 ≠ y2) →
 944  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 945  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 946  nnormalize; #H; #H1;
 947  napply (H (ar8_destruct_2 … H1)).
 948 nqed.
 949
 950 nlemma decidable_ar8_aux3 :
 951 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 952  (x3 ≠ y3) →
 953  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 954  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 955  nnormalize; #H; #H1;
 956  napply (H (ar8_destruct_3 … H1)).
 957 nqed.
 958
 959 nlemma decidable_ar8_aux4 :
 960 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 961  (x4 ≠ y4) →
 962  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 963  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 964  nnormalize; #H; #H1;
 965  napply (H (ar8_destruct_4 … H1)).
 966 nqed.
 967
 968 nlemma decidable_ar8_aux5 :
 969 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 970  (x5 ≠ y5) →
 971  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 972  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 973  nnormalize; #H; #H1;
 974  napply (H (ar8_destruct_5 … H1)).
 975 nqed.
 976
 977 nlemma decidable_ar8_aux6 :
 978 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 979  (x6 ≠ y6) →
 980  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 981  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 982  nnormalize; #H; #H1;
 983  napply (H (ar8_destruct_6 … H1)).
 984 nqed.
 985
 986 nlemma decidable_ar8_aux7 :
 987 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 988  (x7 ≠ y7) →
 989  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 990  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
 991  nnormalize; #H; #H1;
 992  napply (H (ar8_destruct_7 … H1)).
 993 nqed.
 994
 995 nlemma decidable_ar8_aux8 :
 996 ∀T.∀x1,x2,x3,x4,x5,x6,x7,x8,y1,y2,y3,y4,y5,y6,y7,y8:T.
 997  (x8 ≠ y8) →
 998  (mk_Array8T T x1 x2 x3 x4 x5 x6 x7 x8) ≠ (mk_Array8T T y1 y2 y3 y4 y5 y6 y7 y8).
 999  #T; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1000  nnormalize; #H; #H1;
1001  napply (H (ar8_destruct_8 … H1)).
1002 nqed.
1003
1004 nlemma decidable_ar8 :
1005 ∀T.(∀x,y:T.decidable (x = y)) →
1006    (∀a1,a2:Array8T T.decidable (a1 = a2)).
1007  #T; #H;
1008  #x; nelim x; #x1; #x2; #x3; #x4; #x5; #x6; #x7; #x8;
1009  #y; nelim y; #y1; #y2; #y3; #y4; #y5; #y6; #y7; #y8;
1010  nnormalize;
1011  napply (or2_elim (? = ?) (? ≠ ?) ? (H x1 y1) …);
1012  ##[ ##2: #H1; napply (or2_intro2 … (decidable_ar8_aux1 T … H1))
1013  ##| ##1: #H1; napply (or2_elim (? = ?) (? ≠ ?) ? (H x2 y2) …);
1014   ##[ ##2: #H2; napply (or2_intro2 … (decidable_ar8_aux2 T … H2))
1015   ##| ##1: #H2; napply (or2_elim (? = ?) (? ≠ ?) ? (H x3 y3) …);
1016    ##[ ##2: #H3; napply (or2_intro2 … (decidable_ar8_aux3 T … H3))
1017    ##| ##1: #H3; napply (or2_elim (? = ?) (? ≠ ?) ? (H x4 y4) …);
1018     ##[ ##2: #H4; napply (or2_intro2 … (decidable_ar8_aux4 T … H4))
1019     ##| ##1: #H4; napply (or2_elim (? = ?) (? ≠ ?) ? (H x5 y5) …);
1020      ##[ ##2: #H5; napply (or2_intro2 … (decidable_ar8_aux5 T … H5))
1021      ##| ##1: #H5; napply (or2_elim (? = ?) (? ≠ ?) ? (H x6 y6) …);
1022       ##[ ##2: #H6; napply (or2_intro2 … (decidable_ar8_aux6 T … H6))
1023       ##| ##1: #H6; napply (or2_elim (? = ?) (? ≠ ?) ? (H x7 y7) …);
1024        ##[ ##2: #H7; napply (or2_intro2 … (decidable_ar8_aux7 T … H7))
1025        ##| ##1: #H7; napply (or2_elim (? = ?) (? ≠ ?) ? (H x8 y8) …);
1026         ##[ ##2: #H8; napply (or2_intro2 … (decidable_ar8_aux8 T … H8))
1027         ##| ##1: #H8; nrewrite > H1; nrewrite > H2; nrewrite > H3; nrewrite > H4;
1028                       nrewrite > H5; nrewrite > H6; nrewrite > H7; nrewrite > H8;
1029                       napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
1030         ##]
1031        ##]
1032       ##]
1033      ##]
1034     ##]
1035    ##]
1036   ##]
1037  ##]
1038 nqed.
1039
1040 (* !!! per brevita *)
1041 naxiom neqar8_to_neq :
1042 ∀T.∀f:T → T → bool.
1043  (∀x,y:T.f x y = false → x ≠ y) →
1044  (∀p1,p2:Array8T T.(eq_ar8 T f p1 p2 = false → p1 ≠ p2)).
1045
1046 (* !!! per brevita *)
1047 naxiom neq_to_neqar8 :
1048 ∀T.∀f:T → T → bool.
1049  (∀x,y:T.decidable (x = y)) →
1050  (∀x,y:T.x ≠ y → f x y = false) →
1051  (∀p1,p2:Array8T T.(p1 ≠ p2 → eq_ar8 T f p1 p2 = false)).
1052
1053 nlemma ar8_is_comparable : comparable → comparable.
1054  #T; @ (Array8T T)
1055   ##[ napply (mk_Array8T ? (zeroc T) (zeroc T) (zeroc T) (zeroc T)
1056                            (zeroc T) (zeroc T) (zeroc T) (zeroc T))
1057   ##| napply (λP.(forallc T)
1058               (λe1.(forallc T)
1059                (λe2.(forallc T)
1060                 (λe3.(forallc T)
1061                  (λe4.(forallc T)
1062                   (λe5.(forallc T)
1063                    (λe6.(forallc T)
1064                     (λe7.(forallc T)
1065                      (λe8.P (mk_Array8T T e1 e2 e3 e4 e5 e6 e7 e8))))))))))
1066   ##| napply (eq_ar8 … (eqc T))
1067   ##| napply eqar8_to_eq;
1068       napply (eqc_to_eq T)
1069   ##| napply eq_to_eqar8;
1070       napply (eq_to_eqc T)
1071   ##| napply neqar8_to_neq;
1072       napply (neqc_to_neq T)
1073   ##| napply neq_to_neqar8;
1074       ##[ napply (decidable_c T)
1075       ##| napply (neq_to_neqc T) ##]
1076   ##| napply decidable_ar8;
1077       napply (decidable_c T)
1078   ##| napply symmetric_eqar8;
1079       napply (symmetric_eqc T)
1080   ##]
1081 nqed.
1082
1083 unification hint 0 ≔ S: comparable ;
1084          T ≟ (carr S),
1085          X ≟ (ar8_is_comparable S)
1086  (*********************************************) ⊢
1087          carr X ≡ Array8T T.