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_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
  31  #e2; #P; ncases e2; nnormalize; #H;
  32  ##[ ##1: napply (λx:P.x)
  33  ##| ##*: napply False_ind;
  34           nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
  35           nrewrite > H; nnormalize; napply I
  36  ##]
  37 nqed.
  38
  39 ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
  40  #e2; #P; ncases e2; nnormalize; #H;
  41  ##[ ##2: napply (λx:P.x)
  42  ##| ##*: napply False_ind;
  43           nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
  44           nrewrite > H; nnormalize; napply I
  45  ##]
  46 nqed.
  47
  48 ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
  49  #e2; #P; ncases e2; nnormalize; #H;
  50  ##[ ##3: napply (λx:P.x)
  51  ##| ##*: napply False_ind;
  52           nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
  53           nrewrite > H; nnormalize; napply I
  54  ##]
  55 nqed.
  56
  57 ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
  58  #e2; #P; ncases e2; nnormalize; #H;
  59  ##[ ##4: napply (λx:P.x)
  60  ##| ##*: napply False_ind;
  61           nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
  62           nrewrite > H; nnormalize; napply I
  63  ##]
  64 nqed.
  65
  66 ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
  67  #e2; #P; ncases e2; nnormalize; #H;
  68  ##[ ##5: napply (λx:P.x)
  69  ##| ##*: napply False_ind;
  70           nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
  71           nrewrite > H; nnormalize; napply I
  72  ##]
  73 nqed.
  74
  75 ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
  76  #e2; #P; ncases e2; nnormalize; #H;
  77  ##[ ##6: napply (λx:P.x)
  78  ##| ##*: napply False_ind;
  79           nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
  80           nrewrite > H; nnormalize; napply I
  81  ##]
  82 nqed.
  83
  84 ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
  85  #e2; #P; ncases e2; nnormalize; #H;
  86  ##[ ##7: napply (λx:P.x)
  87  ##| ##*: napply False_ind;
  88           nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
  89           nrewrite > H; nnormalize; napply I
  90  ##]
  91 nqed.
  92
  93 ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
  94  #e2; #P; ncases e2; nnormalize; #H;
  95  ##[ ##8: napply (λx:P.x)
  96  ##| ##*: napply False_ind;
  97           nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
  98           nrewrite > H; nnormalize; napply I
  99  ##]
 100 nqed.
 101
 102 ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
 103  #e2; #P; ncases e2; nnormalize; #H;
 104  ##[ ##9: napply (λx:P.x)
 105  ##| ##*: napply False_ind;
 106           nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
 107           nrewrite > H; nnormalize; napply I
 108  ##]
 109 nqed.
 110
 111 ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
 112  #e2; #P; ncases e2; nnormalize; #H;
 113  ##[ ##10: napply (λx:P.x)
 114  ##| ##*: napply False_ind;
 115           nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
 116           nrewrite > H; nnormalize; napply I
 117  ##]
 118 nqed.
 119
 120 ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
 121  #e2; #P; ncases e2; nnormalize; #H;
 122  ##[ ##11: napply (λx:P.x)
 123  ##| ##*: napply False_ind;
 124           nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
 125           nrewrite > H; nnormalize; napply I
 126  ##]
 127 nqed.
 128
 129 ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
 130  #e2; #P; ncases e2; nnormalize; #H;
 131  ##[ ##12: napply (λx:P.x)
 132  ##| ##*: napply False_ind;
 133           nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
 134           nrewrite > H; nnormalize; napply I
 135  ##]
 136 nqed.
 137
 138 ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
 139  #e2; #P; ncases e2; nnormalize; #H;
 140  ##[ ##13: napply (λx:P.x)
 141  ##| ##*: napply False_ind;
 142           nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
 143           nrewrite > H; nnormalize; napply I
 144  ##]
 145 nqed.
 146
 147 ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
 148  #e2; #P; ncases e2; nnormalize; #H;
 149  ##[ ##14: napply (λx:P.x)
 150  ##| ##*: napply False_ind;
 151           nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
 152           nrewrite > H; nnormalize; napply I
 153  ##]
 154 nqed.
 155
 156 ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
 157  #e2; #P; ncases e2; nnormalize; #H;
 158  ##[ ##15: napply (λx:P.x)
 159  ##| ##*: napply False_ind;
 160           nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
 161           nrewrite > H; nnormalize; napply I
 162  ##]
 163 nqed.
 164
 165 ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
 166  #e2; #P; ncases e2; nnormalize; #H;
 167  ##[ ##16: napply (λx:P.x)
 168  ##| ##*: napply False_ind;
 169           nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
 170           nrewrite > H; nnormalize; napply I
 171  ##]
 172 nqed.
 173
 174 ndefinition exadecim_destruct_aux ≝
 175 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
 176  match e1 with
 177   [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
 178   | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
 179   | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
 180   | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
 181   | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
 182   | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
 183   | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
 184   | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
 185   ].
 186
 187 ndefinition exadecim_destruct : exadecim_destruct_aux.
 188  #e1; ncases e1;
 189  ##[ ##1: napply exadecim_destruct1 ##| ##2: napply exadecim_destruct2
 190  ##| ##3: napply exadecim_destruct3 ##| ##4: napply exadecim_destruct4
 191  ##| ##5: napply exadecim_destruct5 ##| ##6: napply exadecim_destruct6
 192  ##| ##7: napply exadecim_destruct7 ##| ##8: napply exadecim_destruct8
 193  ##| ##9: napply exadecim_destruct9 ##| ##10: napply exadecim_destruct10
 194  ##| ##11: napply exadecim_destruct11 ##| ##12: napply exadecim_destruct12
 195  ##| ##13: napply exadecim_destruct13 ##| ##14: napply exadecim_destruct14
 196  ##| ##15: napply exadecim_destruct15 ##| ##16: napply exadecim_destruct16
 197  ##]
 198 nqed.
 199
 200 nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
 201  #e1; #e2;
 202  nelim e1;
 203  nelim e2;
 204  nnormalize;
 205  napply refl_eq.
 206 nqed.
 207
 208 nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
 209  #e1; #e2;
 210  nelim e1;
 211  nelim e2;
 212  nnormalize;
 213  napply refl_eq.
 214 nqed.
 215
 216 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.
 217 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.
 218 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.
 219 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.
 220 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.
 221 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.
 222 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.
 223 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.
 224 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.
 225 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.
 226 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.
 227 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.
 228 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.
 229 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.
 230 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.
 231 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.
 232
 233 nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
 234  #e1; nelim e1;
 235  ##[ ##1: napply  associative_andex1 ##| ##2: napply  associative_andex2
 236  ##| ##3: napply  associative_andex3 ##| ##4: napply  associative_andex4
 237  ##| ##5: napply  associative_andex5 ##| ##6: napply  associative_andex6
 238  ##| ##7: napply  associative_andex7 ##| ##8: napply  associative_andex8
 239  ##| ##9: napply  associative_andex9 ##| ##10: napply  associative_andex10
 240  ##| ##11: napply  associative_andex11 ##| ##12: napply  associative_andex12
 241  ##| ##13: napply  associative_andex13 ##| ##14: napply  associative_andex14
 242  ##| ##15: napply  associative_andex15 ##| ##16: napply  associative_andex16
 243  ##]
 244 nqed.
 245
 246 nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
 247  #e1; #e2;
 248  nelim e1;
 249  nelim e2;
 250  nnormalize;
 251  napply refl_eq.
 252 nqed.
 253
 254 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.
 255 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.
 256 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.
 257 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.
 258 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.
 259 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.
 260 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.
 261 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.
 262 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.
 263 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.
 264 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.
 265 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.
 266 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.
 267 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.
 268 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.
 269 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.
 270
 271 nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
 272  #e1; nelim e1;
 273  ##[ ##1: napply associative_orex1 ##| ##2: napply associative_orex2
 274  ##| ##3: napply associative_orex3 ##| ##4: napply associative_orex4
 275  ##| ##5: napply associative_orex5 ##| ##6: napply associative_orex6
 276  ##| ##7: napply associative_orex7 ##| ##8: napply associative_orex8
 277  ##| ##9: napply associative_orex9 ##| ##10: napply associative_orex10
 278  ##| ##11: napply associative_orex11 ##| ##12: napply associative_orex12
 279  ##| ##13: napply associative_orex13 ##| ##14: napply associative_orex14
 280  ##| ##15: napply associative_orex15 ##| ##16: napply associative_orex16
 281  ##]
 282 nqed.
 283
 284 nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
 285  #e1; #e2;
 286  nelim e1;
 287  nelim e2;
 288  nnormalize;
 289  napply refl_eq.
 290 nqed.
 291
 292 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.
 293 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.
 294 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.
 295 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.
 296 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.
 297 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.
 298 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.
 299 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.
 300 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.
 301 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.
 302 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.
 303 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.
 304 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.
 305 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.
 306 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.
 307 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.
 308
 309 nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
 310  #e1; nelim e1;
 311  ##[ ##1: napply associative_xorex1 ##| ##2: napply associative_xorex2
 312  ##| ##3: napply associative_xorex3 ##| ##4: napply associative_xorex4
 313  ##| ##5: napply associative_xorex5 ##| ##6: napply associative_xorex6
 314  ##| ##7: napply associative_xorex7 ##| ##8: napply associative_xorex8
 315  ##| ##9: napply associative_xorex9 ##| ##10: napply associative_xorex10
 316  ##| ##11: napply associative_xorex11 ##| ##12: napply associative_xorex12
 317  ##| ##13: napply associative_xorex13 ##| ##14: napply associative_xorex14
 318  ##| ##15: napply associative_xorex15 ##| ##16: napply associative_xorex16
 319  ##]
 320 nqed.
 321
 322 nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c.
 323  #e1; #e2; #c;
 324  nelim e1;
 325  nelim e2;
 326  nelim c;
 327  nnormalize;
 328  napply refl_eq.
 329 nqed.
 330
 331 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.
 332  #e1; #e2; #c;
 333  nelim e1;
 334  nelim e2;
 335  nelim c;
 336  nnormalize;
 337  napply refl_eq.
 338 nqed.
 339
 340 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.
 341  #e1; #e2; #c;
 342  nelim e1;
 343  nelim e2;
 344  nelim c;
 345  nnormalize;
 346  napply refl_eq.
 347 nqed.
 348
 349 nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
 350  #e1; #e2;
 351  nelim e1;
 352  nelim e2;
 353  nnormalize;
 354  napply refl_eq.
 355 nqed.
 356
 357 nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
 358  #e1; #e2;
 359  nelim e1;
 360  nelim e2;
 361  nnormalize;
 362  napply refl_eq.
 363 nqed.
 364
 365 nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
 366  #e1; #e2;
 367  nelim e1;
 368  nelim e2;
 369  nnormalize;
 370  napply refl_eq.
 371 nqed.
 372
 373 nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
 374  #e1; #e2; #c;
 375  nelim e1;
 376  nelim e2;
 377  nelim c;
 378  nnormalize;
 379  napply refl_eq.
 380 nqed.
 381
 382 nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
 383  #e1; #e2; #c;
 384  nelim e1;
 385  nelim e2;
 386  nelim c;
 387  nnormalize;
 388  napply refl_eq.
 389 nqed.
 390
 391 nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
 392  #e1; #e2;
 393  nelim e1;
 394  nelim e2;
 395  nnormalize;
 396  napply refl_eq.
 397 nqed.
 398
 399 nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst … (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
 400  #e1; #e2;
 401  nelim e1;
 402  nelim e2;
 403  nnormalize;
 404  napply refl_eq.
 405 nqed.
 406
 407 nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd … (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
 408  #e1; #e2;
 409  nelim e1;
 410  nelim e2;
 411  nnormalize;
 412  napply refl_eq.
 413 nqed.
 414
 415 nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
 416  #e1; #e2;
 417  nelim e1;
 418  nelim e2;
 419  nnormalize;
 420  napply refl_eq.
 421 nqed.
 422
 423 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.
 424 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.
 425 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.
 426 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.
 427 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.
 428 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.
 429 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.
 430 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.
 431 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.
 432 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.
 433 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.
 434 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.
 435 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.
 436 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.
 437 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.
 438 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.
 439
 440 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)).
 441  #e1; nelim e1;
 442  ##[ ##1: napply associative_plusex_d_d1 ##| ##2: napply associative_plusex_d_d2
 443  ##| ##3: napply associative_plusex_d_d3 ##| ##4: napply associative_plusex_d_d4
 444  ##| ##5: napply associative_plusex_d_d5 ##| ##6: napply associative_plusex_d_d6
 445  ##| ##7: napply associative_plusex_d_d7 ##| ##8: napply associative_plusex_d_d8
 446  ##| ##9: napply associative_plusex_d_d9 ##| ##10: napply associative_plusex_d_d10
 447  ##| ##11: napply associative_plusex_d_d11 ##| ##12: napply associative_plusex_d_d12
 448  ##| ##13: napply associative_plusex_d_d13 ##| ##14: napply associative_plusex_d_d14
 449  ##| ##15: napply associative_plusex_d_d15 ##| ##16: napply associative_plusex_d_d16
 450  ##]
 451 nqed.
 452
 453 nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
 454  #e1; #e2;
 455  nelim e1;
 456  nelim e2;
 457  nnormalize;
 458  napply refl_eq.
 459 nqed.
 460
 461 nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
 462  #e1; #e2;
 463  ncases e1;
 464  ncases e2;
 465  nnormalize;
 466  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
 467  ##| ##*: #H; napply (bool_destruct … H)
 468  ##]
 469 nqed.
 470
 471 nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
 472  #m1; #m2;
 473  ncases m1;
 474  ncases m2;
 475  nnormalize;
 476  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
 477  ##| ##*: #H; napply (exadecim_destruct … H)
 478  ##]
 479 nqed.
 480
 481 nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
 482  #x; #y;
 483  nnormalize;
 484  nelim x;
 485  nelim y;
 486  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
 487  ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (exadecim_destruct … H)
 488  ##]
 489 nqed.
 490
 491 nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2).
 492  #n1; #n2;
 493  ncases n1;
 494  ncases n2;
 495  nnormalize;
 496  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H)
 497  ##| ##*: #H; #H1; napply (exadecim_destruct … H1)
 498  ##]
 499 nqed.
 500
 501 nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false.
 502  #n1; #n2;
 503  ncases n1;
 504  ncases n2;
 505  nnormalize;
 506  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; nelim (H (refl_eq …))
 507  ##| ##*: #H; napply refl_eq
 508  ##]
 509 nqed.