freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / exadecim_lemmas.ma

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 47847434eb909921c312e8f7c383433cfa530972..cbb03f412583c669396c5bded4a70b8494c7b47d 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
@@ -174,42 +174,26 @@ nqed.
 ndefinition exadecim_destruct_aux ≝
 Πe1,e2.ΠP:Prop.ΠH:e1 = e2.
  match e1 with
-  [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ]
-  | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
-  | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ]
-  | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
-  | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ]
-  | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
-  | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ]
-  | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
-  | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ]
-  | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
-  | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ]
-  | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
-  | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ]
-  | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
-  | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ]
-  | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
+  [ x0 ⇒ match e2 with [ x0 ⇒ P → P | _ ⇒ P ] | x1 ⇒ match e2 with [ x1 ⇒ P → P | _ ⇒ P ]
+  | x2 ⇒ match e2 with [ x2 ⇒ P → P | _ ⇒ P ] | x3 ⇒ match e2 with [ x3 ⇒ P → P | _ ⇒ P ]
+  | x4 ⇒ match e2 with [ x4 ⇒ P → P | _ ⇒ P ] | x5 ⇒ match e2 with [ x5 ⇒ P → P | _ ⇒ P ]
+  | x6 ⇒ match e2 with [ x6 ⇒ P → P | _ ⇒ P ] | x7 ⇒ match e2 with [ x7 ⇒ P → P | _ ⇒ P ]
+  | x8 ⇒ match e2 with [ x8 ⇒ P → P | _ ⇒ P ] | x9 ⇒ match e2 with [ x9 ⇒ P → P | _ ⇒ P ]
+  | xA ⇒ match e2 with [ xA ⇒ P → P | _ ⇒ P ] | xB ⇒ match e2 with [ xB ⇒ P → P | _ ⇒ P ]
+  | xC ⇒ match e2 with [ xC ⇒ P → P | _ ⇒ P ] | xD ⇒ match e2 with [ xD ⇒ P → P | _ ⇒ P ]
+  | xE ⇒ match e2 with [ xE ⇒ P → P | _ ⇒ P ] | xF ⇒ match e2 with [ xF ⇒ P → P | _ ⇒ P ]
   ].
 
 ndefinition exadecim_destruct : exadecim_destruct_aux.
  #e1; ncases e1;
- ##[ ##1: napply exadecim_destruct1
- ##| ##2: napply exadecim_destruct2
- ##| ##3: napply exadecim_destruct3
- ##| ##4: napply exadecim_destruct4
- ##| ##5: napply exadecim_destruct5
- ##| ##6: napply exadecim_destruct6
- ##| ##7: napply exadecim_destruct7
- ##| ##8: napply exadecim_destruct8
- ##| ##9: napply exadecim_destruct9
- ##| ##10: napply exadecim_destruct10
- ##| ##11: napply exadecim_destruct11
- ##| ##12: napply exadecim_destruct12
- ##| ##13: napply exadecim_destruct13
- ##| ##14: napply exadecim_destruct14
- ##| ##15: napply exadecim_destruct15
- ##| ##16: napply exadecim_destruct16
+ ##[ ##1: napply exadecim_destruct1 ##| ##2: napply exadecim_destruct2
+ ##| ##3: napply exadecim_destruct3 ##| ##4: napply exadecim_destruct4
+ ##| ##5: napply exadecim_destruct5 ##| ##6: napply exadecim_destruct6
+ ##| ##7: napply exadecim_destruct7 ##| ##8: napply exadecim_destruct8
+ ##| ##9: napply exadecim_destruct9 ##| ##10: napply exadecim_destruct10
+ ##| ##11: napply exadecim_destruct11 ##| ##12: napply exadecim_destruct12
+ ##| ##13: napply exadecim_destruct13 ##| ##14: napply exadecim_destruct14
+ ##| ##15: napply exadecim_destruct15 ##| ##16: napply exadecim_destruct16
  ##]
 nqed.
 
@@ -229,25 +213,33 @@ nlemma symmetric_andex : symmetricT exadecim exadecim and_ex.
  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; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ #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
  ##]
 nqed.
 
@@ -259,25 +251,33 @@ nlemma symmetric_orex : symmetricT exadecim exadecim or_ex.
  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; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ #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.
 
@@ -289,25 +289,33 @@ nlemma symmetric_xorex : symmetricT exadecim exadecim xor_ex.
  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; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ #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.
 
@@ -412,25 +420,33 @@ nlemma symmetric_plusex_d_d : ∀e1,e2.plus_ex_d_d e1 e2 = plus_ex_d_d e2 e1.
  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; #e2; #e3;
- nelim e1;
- ##[ ##1: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##2: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##3: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##4: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##5: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##6: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##7: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##8: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##9: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##10: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##11: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##12: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##13: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##14: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##15: nelim e2; nelim e3; nnormalize; napply refl_eq
- ##| ##16: nelim e2; nelim e3; nnormalize; napply refl_eq
+ #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.
 
@@ -467,8 +483,8 @@ nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
  nnormalize;
  nelim x;
  nelim y;
- ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (exadecim_destruct … H)
+ ##[ ##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.