helm/software/matita/contribs/ng_assembly/freescale/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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/bool_lemmas.ma".
  28 include "freescale/exadecim.ma".
  29
  30 (* *********** *)
  31 (* ESADECIMALI *)
  32 (* *********** *)
  33
  34 ndefinition exadecim_destruct1 : Πe2.ΠP:Prop.ΠH:x0 = e2.match e2 with [ x0 ⇒ P → P | _ ⇒ P ].
  35  #e2; #P; ncases e2; nnormalize; #H;
  36  ##[ ##1: napply (λx:P.x)
  37  ##| ##*: napply (False_ind ??);
  38           nchange with (match x0 with [ x0 ⇒ False | _ ⇒ True ]);
  39           nrewrite > H; nnormalize; napply I
  40  ##]
  41 nqed.
  42
  43 ndefinition exadecim_destruct2 : Πe2.ΠP:Prop.ΠH:x1 = e2.match e2 with [ x1 ⇒ P → P | _ ⇒ P ].
  44  #e2; #P; ncases e2; nnormalize; #H;
  45  ##[ ##2: napply (λx:P.x)
  46  ##| ##*: napply (False_ind ??);
  47           nchange with (match x1 with [ x1 ⇒ False | _ ⇒ True ]);
  48           nrewrite > H; nnormalize; napply I
  49  ##]
  50 nqed.
  51
  52 ndefinition exadecim_destruct3 : Πe2.ΠP:Prop.ΠH:x2 = e2.match e2 with [ x2 ⇒ P → P | _ ⇒ P ].
  53  #e2; #P; ncases e2; nnormalize; #H;
  54  ##[ ##3: napply (λx:P.x)
  55  ##| ##*: napply (False_ind ??);
  56           nchange with (match x2 with [ x2 ⇒ False | _ ⇒ True ]);
  57           nrewrite > H; nnormalize; napply I
  58  ##]
  59 nqed.
  60
  61 ndefinition exadecim_destruct4 : Πe2.ΠP:Prop.ΠH:x3 = e2.match e2 with [ x3 ⇒ P → P | _ ⇒ P ].
  62  #e2; #P; ncases e2; nnormalize; #H;
  63  ##[ ##4: napply (λx:P.x)
  64  ##| ##*: napply (False_ind ??);
  65           nchange with (match x3 with [ x3 ⇒ False | _ ⇒ True ]);
  66           nrewrite > H; nnormalize; napply I
  67  ##]
  68 nqed.
  69
  70 ndefinition exadecim_destruct5 : Πe2.ΠP:Prop.ΠH:x4 = e2.match e2 with [ x4 ⇒ P → P | _ ⇒ P ].
  71  #e2; #P; ncases e2; nnormalize; #H;
  72  ##[ ##5: napply (λx:P.x)
  73  ##| ##*: napply (False_ind ??);
  74           nchange with (match x4 with [ x4 ⇒ False | _ ⇒ True ]);
  75           nrewrite > H; nnormalize; napply I
  76  ##]
  77 nqed.
  78
  79 ndefinition exadecim_destruct6 : Πe2.ΠP:Prop.ΠH:x5 = e2.match e2 with [ x5 ⇒ P → P | _ ⇒ P ].
  80  #e2; #P; ncases e2; nnormalize; #H;
  81  ##[ ##6: napply (λx:P.x)
  82  ##| ##*: napply (False_ind ??);
  83           nchange with (match x5 with [ x5 ⇒ False | _ ⇒ True ]);
  84           nrewrite > H; nnormalize; napply I
  85  ##]
  86 nqed.
  87
  88 ndefinition exadecim_destruct7 : Πe2.ΠP:Prop.ΠH:x6 = e2.match e2 with [ x6 ⇒ P → P | _ ⇒ P ].
  89  #e2; #P; ncases e2; nnormalize; #H;
  90  ##[ ##7: napply (λx:P.x)
  91  ##| ##*: napply (False_ind ??);
  92           nchange with (match x6 with [ x6 ⇒ False | _ ⇒ True ]);
  93           nrewrite > H; nnormalize; napply I
  94  ##]
  95 nqed.
  96
  97 ndefinition exadecim_destruct8 : Πe2.ΠP:Prop.ΠH:x7 = e2.match e2 with [ x7 ⇒ P → P | _ ⇒ P ].
  98  #e2; #P; ncases e2; nnormalize; #H;
  99  ##[ ##8: napply (λx:P.x)
 100  ##| ##*: napply (False_ind ??);
 101           nchange with (match x7 with [ x7 ⇒ False | _ ⇒ True ]);
 102           nrewrite > H; nnormalize; napply I
 103  ##]
 104 nqed.
 105
 106 ndefinition exadecim_destruct9 : Πe2.ΠP:Prop.ΠH:x8 = e2.match e2 with [ x8 ⇒ P → P | _ ⇒ P ].
 107  #e2; #P; ncases e2; nnormalize; #H;
 108  ##[ ##9: napply (λx:P.x)
 109  ##| ##*: napply (False_ind ??);
 110           nchange with (match x8 with [ x8 ⇒ False | _ ⇒ True ]);
 111           nrewrite > H; nnormalize; napply I
 112  ##]
 113 nqed.
 114
 115 ndefinition exadecim_destruct10 : Πe2.ΠP:Prop.ΠH:x9 = e2.match e2 with [ x9 ⇒ P → P | _ ⇒ P ].
 116  #e2; #P; ncases e2; nnormalize; #H;
 117  ##[ ##10: napply (λx:P.x)
 118  ##| ##*: napply (False_ind ??);
 119           nchange with (match x9 with [ x9 ⇒ False | _ ⇒ True ]);
 120           nrewrite > H; nnormalize; napply I
 121  ##]
 122 nqed.
 123
 124 ndefinition exadecim_destruct11 : Πe2.ΠP:Prop.ΠH:xA = e2.match e2 with [ xA ⇒ P → P | _ ⇒ P ].
 125  #e2; #P; ncases e2; nnormalize; #H;
 126  ##[ ##11: napply (λx:P.x)
 127  ##| ##*: napply (False_ind ??);
 128           nchange with (match xA with [ xA ⇒ False | _ ⇒ True ]);
 129           nrewrite > H; nnormalize; napply I
 130  ##]
 131 nqed.
 132
 133 ndefinition exadecim_destruct12 : Πe2.ΠP:Prop.ΠH:xB = e2.match e2 with [ xB ⇒ P → P | _ ⇒ P ].
 134  #e2; #P; ncases e2; nnormalize; #H;
 135  ##[ ##12: napply (λx:P.x)
 136  ##| ##*: napply (False_ind ??);
 137           nchange with (match xB with [ xB ⇒ False | _ ⇒ True ]);
 138           nrewrite > H; nnormalize; napply I
 139  ##]
 140 nqed.
 141
 142 ndefinition exadecim_destruct13 : Πe2.ΠP:Prop.ΠH:xC = e2.match e2 with [ xC ⇒ P → P | _ ⇒ P ].
 143  #e2; #P; ncases e2; nnormalize; #H;
 144  ##[ ##13: napply (λx:P.x)
 145  ##| ##*: napply (False_ind ??);
 146           nchange with (match xC with [ xC ⇒ False | _ ⇒ True ]);
 147           nrewrite > H; nnormalize; napply I
 148  ##]
 149 nqed.
 150
 151 ndefinition exadecim_destruct14 : Πe2.ΠP:Prop.ΠH:xD = e2.match e2 with [ xD ⇒ P → P | _ ⇒ P ].
 152  #e2; #P; ncases e2; nnormalize; #H;
 153  ##[ ##14: napply (λx:P.x)
 154  ##| ##*: napply (False_ind ??);
 155           nchange with (match xD with [ xD ⇒ False | _ ⇒ True ]);
 156           nrewrite > H; nnormalize; napply I
 157  ##]
 158 nqed.
 159
 160 ndefinition exadecim_destruct15 : Πe2.ΠP:Prop.ΠH:xE = e2.match e2 with [ xE ⇒ P → P | _ ⇒ P ].
 161  #e2; #P; ncases e2; nnormalize; #H;
 162  ##[ ##15: napply (λx:P.x)
 163  ##| ##*: napply (False_ind ??);
 164           nchange with (match xE with [ xE ⇒ False | _ ⇒ True ]);
 165           nrewrite > H; nnormalize; napply I
 166  ##]
 167 nqed.
 168
 169 ndefinition exadecim_destruct16 : Πe2.ΠP:Prop.ΠH:xF = e2.match e2 with [ xF ⇒ P → P | _ ⇒ P ].
 170  #e2; #P; ncases e2; nnormalize; #H;
 171  ##[ ##16: napply (λx:P.x)
 172  ##| ##*: napply (False_ind ??);
 173           nchange with (match xF with [ xF ⇒ False | _ ⇒ True ]);
 174           nrewrite > H; nnormalize; napply I
 175  ##]
 176 nqed.
 177
 178 ndefinition exadecim_destruct_aux ≝
 179 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
 180  match e1 with
 181   [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ]
 182   | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
 183   | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ]
 184   | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
 185   | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ]
 186   | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
 187   | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ]
 188   | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
 189   | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ]
 190   | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
 191   | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ]
 192   | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
 193   | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ]
 194   | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
 195   | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ]
 196   | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
 197   ].
 198
 199 ndefinition exadecim_destruct : exadecim_destruct_aux.
 200  #e1; ncases e1;
 201  ##[ ##1: napply exadecim_destruct1
 202  ##| ##2: napply exadecim_destruct2
 203  ##| ##3: napply exadecim_destruct3
 204  ##| ##4: napply exadecim_destruct4
 205  ##| ##5: napply exadecim_destruct5
 206  ##| ##6: napply exadecim_destruct6
 207  ##| ##7: napply exadecim_destruct7
 208  ##| ##8: napply exadecim_destruct8
 209  ##| ##9: napply exadecim_destruct9
 210  ##| ##10: napply exadecim_destruct10
 211  ##| ##11: napply exadecim_destruct11
 212  ##| ##12: napply exadecim_destruct12
 213  ##| ##13: napply exadecim_destruct13
 214  ##| ##14: napply exadecim_destruct14
 215  ##| ##15: napply exadecim_destruct15
 216  ##| ##16: napply exadecim_destruct16
 217  ##]
 218 nqed.
 219
 220 nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
 221  #e1; #e2;
 222  nelim e1;
 223  nelim e2;
 224  nnormalize;
 225  napply (refl_eq ??).
 226 nqed.
 227
 228 nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
 229  #e1; #e2;
 230  nelim e1;
 231  nelim e2;
 232  nnormalize;
 233  napply (refl_eq ??).
 234 nqed.
 235
 236 nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
 237  #e1; #e2; #e3;
 238  nelim e1;
 239  ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 240  ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 241  ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 242  ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 243  ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 244  ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 245  ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 246  ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 247  ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 248  ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 249  ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 250  ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 251  ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 252  ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 253  ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 254  ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 255  ##]
 256 nqed.
 257
 258 nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
 259  #e1; #e2;
 260  nelim e1;
 261  nelim e2;
 262  nnormalize;
 263  napply (refl_eq ??).
 264 nqed.
 265
 266 nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
 267  #e1; #e2; #e3;
 268  nelim e1;
 269  ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 270  ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 271  ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 272  ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 273  ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 274  ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 275  ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 276  ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 277  ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 278  ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 279  ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 280  ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 281  ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 282  ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 283  ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 284  ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 285  ##]
 286 nqed.
 287
 288 nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
 289  #e1; #e2;
 290  nelim e1;
 291  nelim e2;
 292  nnormalize;
 293  napply (refl_eq ??).
 294 nqed.
 295
 296 nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
 297  #e1; #e2; #e3;
 298  nelim e1;
 299  ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 300  ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 301  ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 302  ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 303  ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 304  ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 305  ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 306  ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 307  ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 308  ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 309  ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 310  ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 311  ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 312  ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 313  ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 314  ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 315  ##]
 316 nqed.
 317
 318 nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c.
 319  #e1; #e2; #c;
 320  nelim e1;
 321  nelim e2;
 322  nelim c;
 323  nnormalize;
 324  napply (refl_eq ??).
 325 nqed.
 326
 327 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.
 328  #e1; #e2; #c;
 329  nelim e1;
 330  nelim e2;
 331  nelim c;
 332  nnormalize;
 333  napply (refl_eq ??).
 334 nqed.
 335
 336 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.
 337  #e1; #e2; #c;
 338  nelim e1;
 339  nelim e2;
 340  nelim c;
 341  nnormalize;
 342  napply (refl_eq ??).
 343 nqed.
 344
 345 nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
 346  #e1; #e2;
 347  nelim e1;
 348  nelim e2;
 349  nnormalize;
 350  napply (refl_eq ??).
 351 nqed.
 352
 353 nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst ?? (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
 354  #e1; #e2;
 355  nelim e1;
 356  nelim e2;
 357  nnormalize;
 358  napply (refl_eq ??).
 359 nqed.
 360
 361 nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd ?? (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
 362  #e1; #e2;
 363  nelim e1;
 364  nelim e2;
 365  nnormalize;
 366  napply (refl_eq ??).
 367 nqed.
 368
 369 nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
 370  #e1; #e2; #c;
 371  nelim e1;
 372  nelim e2;
 373  nelim c;
 374  nnormalize;
 375  napply (refl_eq ??).
 376 nqed.
 377
 378 nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
 379  #e1; #e2; #c;
 380  nelim e1;
 381  nelim e2;
 382  nelim c;
 383  nnormalize;
 384  napply (refl_eq ??).
 385 nqed.
 386
 387 nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
 388  #e1; #e2;
 389  nelim e1;
 390  nelim e2;
 391  nnormalize;
 392  napply (refl_eq ??).
 393 nqed.
 394
 395 nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst ?? (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
 396  #e1; #e2;
 397  nelim e1;
 398  nelim e2;
 399  nnormalize;
 400  napply (refl_eq ??).
 401 nqed.
 402
 403 nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd ?? (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
 404  #e1; #e2;
 405  nelim e1;
 406  nelim e2;
 407  nnormalize;
 408  napply (refl_eq ??).
 409 nqed.
 410
 411 nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
 412  #e1; #e2;
 413  nelim e1;
 414  nelim e2;
 415  nnormalize;
 416  napply (refl_eq ??).
 417 nqed.
 418
 419 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)).
 420  #e1; #e2; #e3;
 421  nelim e1;
 422  ##[ ##1: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 423  ##| ##2: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 424  ##| ##3: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 425  ##| ##4: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 426  ##| ##5: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 427  ##| ##6: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 428  ##| ##7: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 429  ##| ##8: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 430  ##| ##9: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 431  ##| ##10: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 432  ##| ##11: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 433  ##| ##12: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 434  ##| ##13: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 435  ##| ##14: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 436  ##| ##15: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 437  ##| ##16: nelim e2; nelim e3; nnormalize; napply (refl_eq ??)
 438  ##]
 439 nqed.
 440
 441 nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
 442  #e1; #e2;
 443  nelim e1;
 444  nelim e2;
 445  nnormalize;
 446  napply (refl_eq ??).
 447 nqed.
 448
 449 nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
 450  #e1; #e2;
 451  ncases e1;
 452  ncases e2;
 453  nnormalize;
 454  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
 455  ##| ##*: #H; napply (bool_destruct ??? H)
 456  ##]
 457 nqed.
 458
 459 nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
 460  #m1; #m2;
 461  ncases m1;
 462  ncases m2;
 463  nnormalize;
 464  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (refl_eq ??)
 465  ##| ##*: #H; napply (exadecim_destruct ??? H)
 466  ##]
 467 nqed.