X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Fnum%2Fexadecim_lemmas.ma;h=1d984ebfb6917b6a8b67d59e9b350041f180fb2f;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=2ccd1e3c10e41af7f722aa8599ceae85bcd5f8d7;hpb=601baed778a190b580982b588ebe49ba3f762b30;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
index 2ccd1e3c1..1d984ebfb 100755
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -27,6 +27,7 @@ include "num/bool_lemmas.ma".
 (* ESADECIMALI *)
 (* *********** *)
 
+(*
 ndefinition exadecim_destruct_aux ≝
 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
  match eq_ex e1 e2 with [ true ⇒ P → P | false ⇒ P ].
@@ -38,317 +39,55 @@ ndefinition exadecim_destruct : exadecim_destruct_aux.
  nnormalize;
  napply (λx.x).
 nqed.
+*)
 
-nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
- #e1; #e2;
- nelim e1;
- nelim e2;
+nlemma eq_to_eqex : ∀n1,n2.n1 = n2 → eq_ex n1 n2 = true.
+ #n1; #n2; #H;
+ nrewrite > H;
+ nelim n2;
  nnormalize;
  napply refl_eq.
 nqed.
 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-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. 
-
-nlemma associative_andex : ∀e1,e2,e3.(and_ex (and_ex e1 e2) e3) = (and_ex e1 (and_ex e2 e3)).
- #e1; nelim e1;
- ##[ ##1: napply  associative_andex1 ##| ##2: napply  associative_andex2
- ##| ##3: napply  associative_andex3 ##| ##4: napply  associative_andex4
- ##| ##5: napply  associative_andex5 ##| ##6: napply  associative_andex6
- ##| ##7: napply  associative_andex7 ##| ##8: napply  associative_andex8
- ##| ##9: napply  associative_andex9 ##| ##10: napply  associative_andex10
- ##| ##11: napply  associative_andex11 ##| ##12: napply  associative_andex12
- ##| ##13: napply  associative_andex13 ##| ##14: napply  associative_andex14
- ##| ##15: napply  associative_andex15 ##| ##16: napply  associative_andex16
+nlemma neqex_to_neq : ∀n1,n2.eq_ex n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_ex n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqex n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
  ##]
 nqed.
 
-nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-
-nlemma associative_orex : ∀e1,e2,e3.(or_ex (or_ex e1 e2) e3) = (or_ex e1 (or_ex e2 e3)).
- #e1; nelim e1;
- ##[ ##1: napply associative_orex1 ##| ##2: napply associative_orex2
- ##| ##3: napply associative_orex3 ##| ##4: napply associative_orex4
- ##| ##5: napply associative_orex5 ##| ##6: napply associative_orex6
- ##| ##7: napply associative_orex7 ##| ##8: napply associative_orex8
- ##| ##9: napply associative_orex9 ##| ##10: napply associative_orex10
- ##| ##11: napply associative_orex11 ##| ##12: napply associative_orex12
- ##| ##13: napply associative_orex13 ##| ##14: napply associative_orex14
- ##| ##15: napply associative_orex15 ##| ##16: napply associative_orex16
- ##]
-nqed.
-
-nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-
-nlemma associative_xorex : ∀e1,e2,e3.(xor_ex (xor_ex e1 e2) e3) = (xor_ex e1 (xor_ex e2 e3)).
- #e1; nelim e1;
- ##[ ##1: napply associative_xorex1 ##| ##2: napply associative_xorex2
- ##| ##3: napply associative_xorex3 ##| ##4: napply associative_xorex4
- ##| ##5: napply associative_xorex5 ##| ##6: napply associative_xorex6
- ##| ##7: napply associative_xorex7 ##| ##8: napply associative_xorex8
- ##| ##9: napply associative_xorex9 ##| ##10: napply associative_xorex10
- ##| ##11: napply associative_xorex11 ##| ##12: napply associative_xorex12
- ##| ##13: napply associative_xorex13 ##| ##14: napply associative_xorex14
- ##| ##15: napply associative_xorex15 ##| ##16: napply associative_xorex16
- ##]
-nqed.
-
-nlemma symmetric_plusex_dc_dc : ∀e1,e2,c.plus_ex_dc_dc e1 e2 c = plus_ex_dc_dc e2 e1 c.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-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.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-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.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_dc_dc_to_d_dc : ∀e1,e2.plus_ex_dc_dc e1 e2 false = plus_ex_d_dc e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_dc_dc_to_d_d : ∀e1,e2.fst … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_d e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_dc_dc_to_d_c : ∀e1,e2.snd … (plus_ex_dc_dc e1 e2 false) = plus_ex_d_c e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_plusex_dc_d : ∀e1,e2,c.plus_ex_dc_d e1 e2 c = plus_ex_dc_d e2 e1 c.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_plusex_dc_c : ∀e1,e2,c.plus_ex_dc_c e1 e2 c = plus_ex_dc_c e2 e1 c.
- #e1; #e2; #c;
- nelim e1;
- nelim e2;
- nelim c;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_plusex_d_dc : ∀e1,e2.plus_ex_d_dc e1 e2 = plus_ex_d_dc e2 e1.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_d_dc_to_d_d : ∀e1,e2.fst … (plus_ex_d_dc e1 e2) = plus_ex_d_d e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma plusex_d_dc_to_d_c : ∀e1,e2.snd … (plus_ex_d_dc e1 e2) = plus_ex_d_c e1 e2.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-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.
-
-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)).
- #e1; nelim e1;
- ##[ ##1: napply associative_plusex_d_d1 ##| ##2: napply associative_plusex_d_d2
- ##| ##3: napply associative_plusex_d_d3 ##| ##4: napply associative_plusex_d_d4
- ##| ##5: napply associative_plusex_d_d5 ##| ##6: napply associative_plusex_d_d6
- ##| ##7: napply associative_plusex_d_d7 ##| ##8: napply associative_plusex_d_d8
- ##| ##9: napply associative_plusex_d_d9 ##| ##10: napply associative_plusex_d_d10
- ##| ##11: napply associative_plusex_d_d11 ##| ##12: napply associative_plusex_d_d12
- ##| ##13: napply associative_plusex_d_d13 ##| ##14: napply associative_plusex_d_d14
- ##| ##15: napply associative_plusex_d_d15 ##| ##16: napply associative_plusex_d_d16
- ##]
-nqed.
-
-nlemma symmetric_plusex_d_c : ∀e1,e2.plus_ex_d_c e1 e2 = plus_ex_d_c e2 e1.
- #e1; #e2;
- nelim e1;
- nelim e2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma eqex_to_eq : ∀e1,e2:exadecim.(eq_ex e1 e2 = true) → (e1 = e2).
- #e1; #e2;
- ncases e1;
- ncases e2;
+nlemma eqex_to_eq : ∀n1,n2.eq_ex n1 n2 = true → n1 = n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
  nnormalize;
  ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
  ##]
 nqed.
 
-nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
- #m1; #m2;
- ncases m1;
- ncases m2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply refl_eq
- ##| ##*: #H; napply (exadecim_destruct … H)
- ##]
+nlemma neq_to_neqex : ∀n1,n2.n1 ≠ n2 → eq_ex n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_ex n1 n2));
+ napply (not_to_not (eq_ex n1 n2 = true) (n1 = n2) ? H);
+ napply (eqex_to_eq n1 n2).
 nqed.
 
 nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
- #x; #y;
- nnormalize;
- nelim x;
- nelim y;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …);
-          nnormalize; #H;
-          napply False_ind;
-          napply (exadecim_destruct … H)
- ##]
-nqed.
-
-nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2).
- #n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H)
- ##| ##*: #H; #H1; napply (exadecim_destruct … H1)
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_ex x y = true) (eq_ex x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqex_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqex_to_neq … H))
  ##]
 nqed.
 
-nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false.
+nlemma symmetric_eqex : symmetricT exadecim bool eq_ex.
  #n1; #n2;
- ncases n1;
- ncases n2;
- nnormalize;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; nelim (H (refl_eq …))
- ##| ##*: #H; napply refl_eq
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_ex n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqex n1 n2 H);
+          napply (symmetric_eq ? (eq_ex n2 n1) false);
+          napply (neq_to_neqex n2 n1 (symmetric_neq ? n1 n2 H))
  ##]
 nqed.