helm/software/matita/contribs/ng_assembly/num/exadecim_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 (*   Ultima modifica: 05/08/2009                                          *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "num/exadecim.ma".
  24 include "num/bool_lemmas.ma".
  25
  26 (* *********** *)
  27 (* ESADECIMALI *)
  28 (* *********** *)
  29
  30 ndefinition exadecim_destruct_aux ≝
  31 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
  32  match eq_ex e1 e2 with [ true ⇒ P → P | false ⇒ P ].
  33
  34 ndefinition exadecim_destruct : exadecim_destruct_aux.
  35  #e1; #e2; #P; #H;
  36  nrewrite < H;
  37  nelim e1;
  38  nnormalize;
  39  napply (λx.x).
  40 nqed.
  41
  42 nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
  43  #e1; #e2;
  44  nelim e1;
  45  nelim e2;
  46  nnormalize;
  47  napply refl_eq.
  48 nqed.
  49
  50 nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
  51  #e1; #e2;
  52  nelim e1;
  53  nelim e2;
  54  nnormalize;
  55  napply refl_eq.
  56 nqed.
  57
  58 nlemma associative_andex1 : ∀e2,e3.(and_ex (and_ex x0 e2) e3) = (and_ex x0 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  59 nlemma associative_andex2 : ∀e2,e3.(and_ex (and_ex x1 e2) e3) = (and_ex x1 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  60 nlemma associative_andex3 : ∀e2,e3.(and_ex (and_ex x2 e2) e3) = (and_ex x2 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  61 nlemma associative_andex4 : ∀e2,e3.(and_ex (and_ex x3 e2) e3) = (and_ex x3 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  62 nlemma associative_andex5 : ∀e2,e3.(and_ex (and_ex x4 e2) e3) = (and_ex x4 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  63 nlemma associative_andex6 : ∀e2,e3.(and_ex (and_ex x5 e2) e3) = (and_ex x5 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  64 nlemma associative_andex7 : ∀e2,e3.(and_ex (and_ex x6 e2) e3) = (and_ex x6 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  65 nlemma associative_andex8 : ∀e2,e3.(and_ex (and_ex x7 e2) e3) = (and_ex x7 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  66 nlemma associative_andex9 : ∀e2,e3.(and_ex (and_ex x8 e2) e3) = (and_ex x8 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  67 nlemma associative_andex10 : ∀e2,e3.(and_ex (and_ex x9 e2) e3) = (and_ex x9 (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  68 nlemma associative_andex11 : ∀e2,e3.(and_ex (and_ex xA e2) e3) = (and_ex xA (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  69 nlemma associative_andex12 : ∀e2,e3.(and_ex (and_ex xB e2) e3) = (and_ex xB (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  70 nlemma associative_andex13 : ∀e2,e3.(and_ex (and_ex xC e2) e3) = (and_ex xC (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  71 nlemma associative_andex14 : ∀e2,e3.(and_ex (and_ex xD e2) e3) = (and_ex xD (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  72 nlemma associative_andex15 : ∀e2,e3.(and_ex (and_ex xE e2) e3) = (and_ex xE (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  73 nlemma associative_andex16 : ∀e2,e3.(and_ex (and_ex xF e2) e3) = (and_ex xF (and_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  74
  75 nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
  76  #e1; nelim e1;
  77  ##[ ##1: napply  associative_andex1 ##| ##2: napply  associative_andex2
  78  ##| ##3: napply  associative_andex3 ##| ##4: napply  associative_andex4
  79  ##| ##5: napply  associative_andex5 ##| ##6: napply  associative_andex6
  80  ##| ##7: napply  associative_andex7 ##| ##8: napply  associative_andex8
  81  ##| ##9: napply  associative_andex9 ##| ##10: napply  associative_andex10
  82  ##| ##11: napply  associative_andex11 ##| ##12: napply  associative_andex12
  83  ##| ##13: napply  associative_andex13 ##| ##14: napply  associative_andex14
  84  ##| ##15: napply  associative_andex15 ##| ##16: napply  associative_andex16
  85  ##]
  86 nqed.
  87
  88 nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
  89  #e1; #e2;
  90  nelim e1;
  91  nelim e2;
  92  nnormalize;
  93  napply refl_eq.
  94 nqed.
  95
  96 nlemma associative_orex1 : ∀e2,e3.(or_ex (or_ex x0 e2) e3) = (or_ex x0 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  97 nlemma associative_orex2 : ∀e2,e3.(or_ex (or_ex x1 e2) e3) = (or_ex x1 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  98 nlemma associative_orex3 : ∀e2,e3.(or_ex (or_ex x2 e2) e3) = (or_ex x2 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
  99 nlemma associative_orex4 : ∀e2,e3.(or_ex (or_ex x3 e2) e3) = (or_ex x3 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 100 nlemma associative_orex5 : ∀e2,e3.(or_ex (or_ex x4 e2) e3) = (or_ex x4 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 101 nlemma associative_orex6 : ∀e2,e3.(or_ex (or_ex x5 e2) e3) = (or_ex x5 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 102 nlemma associative_orex7 : ∀e2,e3.(or_ex (or_ex x6 e2) e3) = (or_ex x6 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 103 nlemma associative_orex8 : ∀e2,e3.(or_ex (or_ex x7 e2) e3) = (or_ex x7 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 104 nlemma associative_orex9 : ∀e2,e3.(or_ex (or_ex x8 e2) e3) = (or_ex x8 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 105 nlemma associative_orex10 : ∀e2,e3.(or_ex (or_ex x9 e2) e3) = (or_ex x9 (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 106 nlemma associative_orex11 : ∀e2,e3.(or_ex (or_ex xA e2) e3) = (or_ex xA (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 107 nlemma associative_orex12 : ∀e2,e3.(or_ex (or_ex xB e2) e3) = (or_ex xB (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 108 nlemma associative_orex13 : ∀e2,e3.(or_ex (or_ex xC e2) e3) = (or_ex xC (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 109 nlemma associative_orex14 : ∀e2,e3.(or_ex (or_ex xD e2) e3) = (or_ex xD (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 110 nlemma associative_orex15 : ∀e2,e3.(or_ex (or_ex xE e2) e3) = (or_ex xE (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 111 nlemma associative_orex16 : ∀e2,e3.(or_ex (or_ex xF e2) e3) = (or_ex xF (or_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 112
 113 nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
 114  #e1; nelim e1;
 115  ##[ ##1: napply associative_orex1 ##| ##2: napply associative_orex2
 116  ##| ##3: napply associative_orex3 ##| ##4: napply associative_orex4
 117  ##| ##5: napply associative_orex5 ##| ##6: napply associative_orex6
 118  ##| ##7: napply associative_orex7 ##| ##8: napply associative_orex8
 119  ##| ##9: napply associative_orex9 ##| ##10: napply associative_orex10
 120  ##| ##11: napply associative_orex11 ##| ##12: napply associative_orex12
 121  ##| ##13: napply associative_orex13 ##| ##14: napply associative_orex14
 122  ##| ##15: napply associative_orex15 ##| ##16: napply associative_orex16
 123  ##]
 124 nqed.
 125
 126 nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
 127  #e1; #e2;
 128  nelim e1;
 129  nelim e2;
 130  nnormalize;
 131  napply refl_eq.
 132 nqed.
 133
 134 nlemma associative_xorex1 : ∀e2,e3.(xor_ex (xor_ex x0 e2) e3) = (xor_ex x0 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 135 nlemma associative_xorex2 : ∀e2,e3.(xor_ex (xor_ex x1 e2) e3) = (xor_ex x1 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 136 nlemma associative_xorex3 : ∀e2,e3.(xor_ex (xor_ex x2 e2) e3) = (xor_ex x2 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 137 nlemma associative_xorex4 : ∀e2,e3.(xor_ex (xor_ex x3 e2) e3) = (xor_ex x3 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 138 nlemma associative_xorex5 : ∀e2,e3.(xor_ex (xor_ex x4 e2) e3) = (xor_ex x4 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 139 nlemma associative_xorex6 : ∀e2,e3.(xor_ex (xor_ex x5 e2) e3) = (xor_ex x5 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 140 nlemma associative_xorex7 : ∀e2,e3.(xor_ex (xor_ex x6 e2) e3) = (xor_ex x6 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 141 nlemma associative_xorex8 : ∀e2,e3.(xor_ex (xor_ex x7 e2) e3) = (xor_ex x7 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 142 nlemma associative_xorex9 : ∀e2,e3.(xor_ex (xor_ex x8 e2) e3) = (xor_ex x8 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 143 nlemma associative_xorex10 : ∀e2,e3.(xor_ex (xor_ex x9 e2) e3) = (xor_ex x9 (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 144 nlemma associative_xorex11 : ∀e2,e3.(xor_ex (xor_ex xA e2) e3) = (xor_ex xA (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 145 nlemma associative_xorex12 : ∀e2,e3.(xor_ex (xor_ex xB e2) e3) = (xor_ex xB (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 146 nlemma associative_xorex13 : ∀e2,e3.(xor_ex (xor_ex xC e2) e3) = (xor_ex xC (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 147 nlemma associative_xorex14 : ∀e2,e3.(xor_ex (xor_ex xD e2) e3) = (xor_ex xD (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 148 nlemma associative_xorex15 : ∀e2,e3.(xor_ex (xor_ex xE e2) e3) = (xor_ex xE (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 149 nlemma associative_xorex16 : ∀e2,e3.(xor_ex (xor_ex xF e2) e3) = (xor_ex xF (xor_ex e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 150
 151 nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
 152  #e1; nelim e1;
 153  ##[ ##1: napply associative_xorex1 ##| ##2: napply associative_xorex2
 154  ##| ##3: napply associative_xorex3 ##| ##4: napply associative_xorex4
 155  ##| ##5: napply associative_xorex5 ##| ##6: napply associative_xorex6
 156  ##| ##7: napply associative_xorex7 ##| ##8: napply associative_xorex8
 157  ##| ##9: napply associative_xorex9 ##| ##10: napply associative_xorex10
 158  ##| ##11: napply associative_xorex11 ##| ##12: napply associative_xorex12
 159  ##| ##13: napply associative_xorex13 ##| ##14: napply associative_xorex14
 160  ##| ##15: napply associative_xorex15 ##| ##16: napply associative_xorex16
 161  ##]
 162 nqed.
 163
 164 nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c.
 165  #e1; #e2; #c;
 166  nelim e1;
 167  nelim e2;
 168  nelim c;
 169  nnormalize;
 170  napply refl_eq.
 171 nqed.
 172
 173 nlemma plusex_dc_dc_to_dc_d : ∀e1,e2,c.fst … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_d e1 e2 c.
 174  #e1; #e2; #c;
 175  nelim e1;
 176  nelim e2;
 177  nelim c;
 178  nnormalize;
 179  napply refl_eq.
 180 nqed.
 181
 182 nlemma plusex_dc_dc_to_dc_c : ∀e1,e2,c.snd … (plus_ex_dc_dc e1 e2 c) = plus_ex_dc_c e1 e2 c.
 183  #e1; #e2; #c;
 184  nelim e1;
 185  nelim e2;
 186  nelim c;
 187  nnormalize;
 188  napply refl_eq.
 189 nqed.
 190
 191 nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
 192  #e1; #e2;
 193  nelim e1;
 194  nelim e2;
 195  nnormalize;
 196  napply refl_eq.
 197 nqed.
 198
 199 nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
 200  #e1; #e2;
 201  nelim e1;
 202  nelim e2;
 203  nnormalize;
 204  napply refl_eq.
 205 nqed.
 206
 207 nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
 208  #e1; #e2;
 209  nelim e1;
 210  nelim e2;
 211  nnormalize;
 212  napply refl_eq.
 213 nqed.
 214
 215 nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
 216  #e1; #e2; #c;
 217  nelim e1;
 218  nelim e2;
 219  nelim c;
 220  nnormalize;
 221  napply refl_eq.
 222 nqed.
 223
 224 nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
 225  #e1; #e2; #c;
 226  nelim e1;
 227  nelim e2;
 228  nelim c;
 229  nnormalize;
 230  napply refl_eq.
 231 nqed.
 232
 233 nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
 234  #e1; #e2;
 235  nelim e1;
 236  nelim e2;
 237  nnormalize;
 238  napply refl_eq.
 239 nqed.
 240
 241 nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst … (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
 242  #e1; #e2;
 243  nelim e1;
 244  nelim e2;
 245  nnormalize;
 246  napply refl_eq.
 247 nqed.
 248
 249 nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd … (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
 250  #e1; #e2;
 251  nelim e1;
 252  nelim e2;
 253  nnormalize;
 254  napply refl_eq.
 255 nqed.
 256
 257 nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
 258  #e1; #e2;
 259  nelim e1;
 260  nelim e2;
 261  nnormalize;
 262  napply refl_eq.
 263 nqed.
 264
 265 nlemma associative_plusex_d_d1 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x0 e2) e3) = (plus_ex_d_d x0 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 266 nlemma associative_plusex_d_d2 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x1 e2) e3) = (plus_ex_d_d x1 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 267 nlemma associative_plusex_d_d3 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x2 e2) e3) = (plus_ex_d_d x2 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 268 nlemma associative_plusex_d_d4 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x3 e2) e3) = (plus_ex_d_d x3 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 269 nlemma associative_plusex_d_d5 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x4 e2) e3) = (plus_ex_d_d x4 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 270 nlemma associative_plusex_d_d6 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x5 e2) e3) = (plus_ex_d_d x5 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 271 nlemma associative_plusex_d_d7 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x6 e2) e3) = (plus_ex_d_d x6 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 272 nlemma associative_plusex_d_d8 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x7 e2) e3) = (plus_ex_d_d x7 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 273 nlemma associative_plusex_d_d9 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x8 e2) e3) = (plus_ex_d_d x8 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 274 nlemma associative_plusex_d_d10 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d x9 e2) e3) = (plus_ex_d_d x9 (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 275 nlemma associative_plusex_d_d11 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xA e2) e3) = (plus_ex_d_d xA (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 276 nlemma associative_plusex_d_d12 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xB e2) e3) = (plus_ex_d_d xB (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 277 nlemma associative_plusex_d_d13 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xC e2) e3) = (plus_ex_d_d xC (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 278 nlemma associative_plusex_d_d14 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xD e2) e3) = (plus_ex_d_d xD (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 279 nlemma associative_plusex_d_d15 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xE e2) e3) = (plus_ex_d_d xE (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 280 nlemma associative_plusex_d_d16 : ∀e2,e3.(plus_ex_d_d (plus_ex_d_d xF e2) e3) = (plus_ex_d_d xF (plus_ex_d_d e2 e3)). #e2; #e3; nelim e2; nelim e3; nnormalize; napply refl_eq. nqed.
 281
 282 nlemma associative_plusex_d_d : ∀e1,e2,e3.(plus_ex_d_d (plus_ex_d_d e1 e2) e3) = (plus_ex_d_d e1 (plus_ex_d_d e2 e3)).
 283  #e1; nelim e1;
 284  ##[ ##1: napply associative_plusex_d_d1 ##| ##2: napply associative_plusex_d_d2
 285  ##| ##3: napply associative_plusex_d_d3 ##| ##4: napply associative_plusex_d_d4
 286  ##| ##5: napply associative_plusex_d_d5 ##| ##6: napply associative_plusex_d_d6
 287  ##| ##7: napply associative_plusex_d_d7 ##| ##8: napply associative_plusex_d_d8
 288  ##| ##9: napply associative_plusex_d_d9 ##| ##10: napply associative_plusex_d_d10
 289  ##| ##11: napply associative_plusex_d_d11 ##| ##12: napply associative_plusex_d_d12
 290  ##| ##13: napply associative_plusex_d_d13 ##| ##14: napply associative_plusex_d_d14
 291  ##| ##15: napply associative_plusex_d_d15 ##| ##16: napply associative_plusex_d_d16
 292  ##]
 293 nqed.
 294
 295 nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
 296  #e1; #e2;
 297  nelim e1;
 298  nelim e2;
 299  nnormalize;
 300  napply refl_eq.
 301 nqed.
 302
 303 nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
 304  #e1; #e2;
 305  ncases e1;
 306  ncases e2;
 307  nnormalize;
 308  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
 309  ##| ##*: #H; napply (bool_destruct … H)
 310  ##]
 311 nqed.
 312
 313 nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
 314  #m1; #m2;
 315  ncases m1;
 316  ncases m2;
 317  nnormalize;
 318  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
 319  ##| ##*: #H; napply (exadecim_destruct … H)
 320  ##]
 321 nqed.
 322
 323 nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
 324  #x; #y;
 325  nnormalize;
 326  nelim x;
 327  nelim y;
 328  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 329  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
 330           nnormalize; #H;
 331           napply False_ind;
 332           napply (exadecim_destruct … H)
 333  ##]
 334 nqed.
 335
 336 nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2).
 337  #n1; #n2;
 338  ncases n1;
 339  ncases n2;
 340  nnormalize;
 341  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H)
 342  ##| ##*: #H; #H1; napply (exadecim_destruct … H1)
 343  ##]
 344 nqed.
 345
 346 nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false.
 347  #n1; #n2;
 348  ncases n1;
 349  ncases n2;
 350  nnormalize;
 351  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; nelim (H (refl_eq …))
 352  ##| ##*: #H; napply refl_eq
 353  ##]
 354 nqed.