From 1d8389a897e804825909cc84640e0d5c5f58e543 Mon Sep 17 00:00:00 2001
From: Cosimo Oliboni <??>
Date: Wed, 12 Aug 2009 02:11:23 +0000
Subject: [PATCH]  freescale porting, work in progress

---
 .../contribs/ng_assembly/common/meta_type.ma  | 475 ++++++------------
 .../contribs/ng_assembly/common/theory.ma     | 205 ++++++++
 2 files changed, 354 insertions(+), 326 deletions(-)

diff --git a/helm/software/matita/contribs/ng_assembly/common/meta_type.ma b/helm/software/matita/contribs/ng_assembly/common/meta_type.ma
index 751a4bb56..1ba04df07 100755
--- a/helm/software/matita/contribs/ng_assembly/common/meta_type.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/meta_type.ma
@@ -20,7 +20,7 @@
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "common/string_lemmas.ma".
+include "common/list_utility_lemmas.ma".
 
 nlet rec nmember_list (T:Type) (elem:T) (f:T → T → bool) (l:list T) on l ≝
  match l with
@@ -491,6 +491,46 @@ ndefinition eq_UN ≝
 
  ].
 
+(* costruttore di un sottouniverso:
+   S_EL cioe' uno qualsiasi degli elementi del sottouniverso
+   S_KO cioe' il caso impossibile
+*)
+ninductive S_UN (l:list UN) : Type ≝
+  S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → (∀y.eq_UN x y = true → x = y) → S_UN l
+| S_KO : False → S_UN l. 
+
+ndefinition getelem : ∀l.∀e:S_UN l.UN.
+ #l; #s; nelim s;
+ ##[ ##1: #u; #dim1; #dim2; napply u
+ ##| ##2: #F; nelim F
+ ##]
+nqed.
+
+ndefinition eq_SUN ≝ λl.λx,y:S_UN l.eq_UN (getelem ? x) (getelem ? y).
+
+ndefinition getdim1 : ∀l.∀e:S_UN l.member_list UN (getelem ? e) eq_UN l = true.
+ #l; #s; nelim s;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u; #dim1; #dim2; napply dim1
+ ##]
+nqed.
+
+ndefinition getdim2 : ∀l.∀e:S_UN l.(∀y.eq_UN (getelem ? e) y = true → (getelem ? e) = y).
+ #l; #s; nelim s;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u; #dim1; #dim2; napply dim2
+ ##]
+nqed.
+
+nlemma SUN_destruct_1
+ : ∀l.∀e1,e2.∀dim11,dim21.∀dim12,dim22.S_EL l e1 dim11 dim12 = S_EL l e2 dim21 dim22 → e1 = e2.
+ #l; #e1; #e2; #dim11; #dim21; #dim12; #dim22; #H;
+ nchange with (match S_EL l e2 dim21 dim22 with [ S_EL a _ _ ⇒ e1 = a | S_KO _ ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
 ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true ⇒ P → P  | false ⇒ P ].
  #x; #y; #P; #H;
  nrewrite > H;
@@ -499,6 +539,19 @@ ndefinition UN_destruct : ∀x,y.∀P:Prop.x = y → match eq_UN x y with [ true
  napply (λx.x).
 nqed.
 
+ndefinition SUN_destruct : ∀l.∀x,y:S_UN l.∀P:Prop.x = y → match eq_SUN l x y with [ true ⇒ P → P | false ⇒ P ].
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u2; #dim21; #dim22; #P;
+                   nchange with (? → (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]));
+                   #H; napply (UN_destruct u1 u2);
+                   napply (SUN_destruct_1 l … H)
+          ##]
+ ##]
+nqed.
+
 nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true.
  #e1; #e2; #H;
  nrewrite > H;
@@ -507,225 +560,130 @@ nlemma eq_to_eqUN : ∀e1,e2.e1 = e2 → eq_UN e1 e2 = true.
  napply refl_eq.
 nqed.
 
-nlemma pippo : ∀A,B:Prop.(A → B) → ((¬B) → (¬A)).
- #A; #B; #H; nnormalize;
- #H1; #H2;
- napply (H1 (H H2)).
-nqed.
-
-nlemma pluto1 : ∀x.x = false → x ≠ true.
- #x; nelim x;
- ##[ ##1: #H; napply (bool_destruct … H)
- ##| ##2: #H; nnormalize; #H1; napply (bool_destruct … H1)
- ##]
-nqed.
-
-nlemma pluto2 : ∀x.x = true → x ≠ false.
- #x; nelim x;
- ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
- ##| ##2: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma pluto3 : ∀x.x ≠ false → x = true.
- #x; nelim x;
- ##[ ##1: #H; napply refl_eq
- ##| ##2: nnormalize; #H; nelim (H (refl_eq …))
- ##]
-nqed.
-
-nlemma pluto4 : ∀x.x ≠ true → x = false.
- #x; nelim x;
- ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
- ##| ##2: #H; napply refl_eq
+nlemma eq_to_eqSUN : ∀l.∀x,y:S_UN l.x = y → eq_SUN l x y = true.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u2; #dim21; #dim22;
+                   nchange with (? → eq_UN u1 u2 = true);
+                   #H; napply (eq_to_eqUN u1 u2);
+                   napply (SUN_destruct_1 l … H)
+          ##]
  ##]
 nqed.
 
 nlemma neqUN_to_neq : ∀e1,e2.eq_UN e1 e2 = false → e1 ≠ e2.
  #e1; #e2; #H;
- napply (pippo (e1 = e2) (eq_UN e1 e2 = true) …);
+ napply (not_to_not (e1 = e2) (eq_UN e1 e2 = true) …);
  ##[ ##1: napply (eq_to_eqUN e1 e2)
- ##| ##2: napply (pluto1 … H)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
  ##]
 nqed.
 
-naxiom eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
-
-nlemma neq_to_neqUN : ∀e1,e2.e1 ≠ e2 → eq_UN e1 e2 = false.
- #e1; #e2; #H;
- napply (pluto4 (eq_UN e1 e2));
- napply (pippo (eq_UN e1 e2 = true) (e1 = e2) ? H);
- napply (eqUN_to_eq e1 e2).
-nqed.
-
-nlemma decidable_UN : ∀x,y:UN.decidable (x = y).
- #x; #y; nnormalize;
- napply (or2_elim (eq_UN x y = true) (eq_UN x y = false) ?);
- ##[ ##1: ncases (eq_UN x y);
-          ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
-          ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
+nlemma neqSUN_to_neq : ∀l.∀x,y:S_UN l.eq_SUN l x y = false → x ≠ y.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u2; #dim21; #dim22;
+                        nchange with ((eq_UN u1 u2 = false) → ?);
+                        #H; nnormalize; #H1;
+                        napply (neqUN_to_neq u1 u2 H);
+                        napply (SUN_destruct_1 l … H1)
           ##]
- ##| ##2: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqUN_to_eq … H))
- ##| ##3: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqUN_to_neq … H))
  ##]
 nqed.
 
- nrewrite > (eq_to_eqUN e1 e2 ?);
+naxiom SUN_construct
+ : ∀l.∀u.
+   ∀dim11,dim21:(member_list UN u eq_UN l = true).
+   ∀dim12,dim22:(∀y0.(eq_UN u y0 = true) → (u = y0)).
+   ((S_EL l u dim11 dim12) = (S_EL l u dim21 dim22)).
 
-nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
- #e1; #e2; #H;
- 
-
-nlemma pippo : ∀P.(¬¬¬P) → (¬P).
- #P; nnormalize; #H; #H1;
- napply H; #H2;
- napply (H2 H1).
+nlemma eqgetelem_to_eq : ∀l.∀x,y:S_UN l.(getelem ? x) = (getelem ? y) → x = y.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u2; #dim21; #dim22;
+                   nchange with (u1 = u2 → ?); #H;
+                   nrewrite > H in dim11:(%) dim12:(%) ⊢ %; #dim11; #dim12;
+                   napply (SUN_construct l u2 dim11 dim21 dim12 dim22);
+          ##]
+ ##]
 nqed.
 
-nlemma pippo2 : ∀P.(¬¬P) → P.
- #P; nnormalize; #H;
- napply (or2_elim (¬P) (¬¬¬¬P) ?);
- ##[ ##1: napply (or2_intro2 ?? (prop_to_nnprop ? H))
- ##| ##2: #H1; nelim (H H1)
- ##| ##3: #H1; napply False_ind;
-          napply (H (pippo …));
-          nnormalize; #H2;
-          napply False_ind;
-          napply (pippo ? H1);
-          #H2;
-          napply H;
-          napply False_ind;
-          napply H1; #H2;
-        
- ##[ ##2: #H1;napply (prop_to_nnprop ? H);
- ##| ##1: nnormalize; #H1;
- napply False_ind;
- napply H; #H1;
- napply H;
- napply (or2_elim (¬¬P) (¬¬¬P) ?);
- ##[ ##1: napply (or2_intro1 ?? H);
- 
- napply (absurd (¬¬¬P) P ??);
- ##[ ##2: napply (prop_to_nnprop ? H);
- ##| ##1:
- napply (pippo P);
- nnormalize;
- nnormalize in H:(%);
- #H1;
- #H1;
- napply (absurd ? False H ?);
- nnormalize;
- #H2;
- nnormalize; #H;
- napply False_ind;
- napply H; #H1;
- napply (absurd ? False (prop_to_nnprop (¬P) ?));
- ##[ ##1: nnormalize; #H2; napply (H2 H)
- ##| ##2:
- nnormalize; #H2;
- nnormalize in K:(%);
- # .
+nlemma neq_to_neqgetelem : ∀l.∀x,y:S_UN l.x ≠ y → (getelem ? x) ≠ (getelem ? y).
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u2; #dim21; #dim22; #H;
+                   napply (not_to_not ((getelem l ?) = (getelem l ?))
+                                      ((S_EL l u1 dim11 dim12) = (S_EL l u2 dim21 dim22)) ?);
+                   ##[ ##1: napply H
+                   ##| ##2: napply (eqgetelem_to_eq l …)
+                   ##]
+          ##]
+ ##]
 nqed.
 
-nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
- #e1; #e2;
- napply (or2_elim (eq_UN e1 e2 = false) (e1 ≠ e2) ?);
- ##[ ##3:
- nelim e1;
- nnormalize;
- nchange with (match e2 with [ ? ⇒ true | _ ⇒ false ]);
- nelim e2;
- #H;
- napply (or2_elim (e1 = e2) (e1 ≠ e2) …);
- ##[ ##2:
- 
- ##[ ##1: ncases (eq_UN e1 e2);
-          ##[ ##1: napply (or2_intro1 (true = true) (true = false) (refl_eq …))
-          ##| ##2: napply (or2_intro2 (false = true) (false = false) (refl_eq …))
+nlemma eqSUN_to_eq : ∀l.∀x,y:S_UN l.eq_SUN l x y = true → x = y.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u2; #dim21; #dim22;
+                   nchange with ((eq_UN u1 u2 = true) → ?); #H;
+                   nrewrite > (eqgetelem_to_eq l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22) (dim12 u2 H));
+                   napply refl_eq
           ##]
- ##| ##3: 
-
-
- nnormalize;
- nrewrite > H;
- nelim e2;
- nnormalize;
- napply refl_eq.
+ ##]
 nqed.
 
-ndefinition decidable_UN1 ≝ λx.∀y:UN.decidable (x = y).
- #x;
- nnormalize;
- nelim x;
- ##[ ##1: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); #H; napply (UN_destruct … H)
+nlemma neq_to_neqSUN : ∀l.∀x,y:S_UN l.x ≠ y → eq_SUN l x y = false.
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u2; #dim21; #dim22; #H;
+                   napply neqtrue_to_eqfalse;
+                   napply (not_to_not ?? (eqSUN_to_eq l ??) ?) ;
+                   napply H
+          ##]
  ##]
 nqed.
 
-naxiom decidable_UN : ∀x,y:UN.decidable (x = y).
-
-nlemma neq_to_neqUN : ∀e1,e2.e1 ≠ e2 → eq_UN e1 e2 = false.
- #e1; #e2; #H;
-
-nlemma eqUN_to_eq : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
- #e1; #e2; #H; napply (or2_elim ??? (decidable_UN e1 e2));
- ##[ ##2: #H1;
-
-nlemma pippo : ∀e1,e2:UN.decidable (e1 = e2).
- #e1; #e2; nnormalize;
- nelim e1;
- napply (or2_intro1 (? = ?) (? ≠ ?) …);
- nchange with (match e2 with [ ? ⇒ refl_eq UN ? | _ ⇒ ? ]);
- napply (destruct_UN ? e2 (? = e2) ?);
-
-nlemma pippo : ∀e1,e2.eq_UN e1 e2 = true → e1 = e2.
- #e1; nelim e1; #e2;
-
-
-(* costruttore di un sottouniverso:
-   S_EL cioe' uno qualsiasi degli elementi del sottouniverso
-   S_KO cioe' il caso impossibile
-*)
-ninductive S_UN (l:list UN) : Type ≝
-  S_EL : Πx:UN.((member_list UN x eq_UN l) = true) → 
-               (∀y.x = y → (eq_UN x y = true)) →
-               (∀y.(eq_UN x y = true) → x = y) →
-               (∀y.decidable (x = y)) →
-               (∀y.x ≠ y → (eq_UN x y = false)) →
-               (∀y.(eq_UN x y = false) → x ≠ y) →
-               S_UN l
-| S_KO : False → S_UN l. 
-
-ndefinition SUN_create : Πl.Πe.(member_list UN e eq_UN l = true) → S_UN l.
- #l; #e; #dim; napply (S_EL l e dim …);
- ##[ ##1: #y; #H; nrewrite > H; nelim y; nnormalize; napply refl_eq
- ##| ##2: #y;
-
-(* sottoinsieme degli esadecimali *)
-ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ].
-
-(* getter del testimone di esistenza *)
-ndefinition getelem : ∀l.∀e:S_UN l.UN.
- #l; #s; nelim s;
- ##[ ##1: #u; #H; napply u
- ##| ##2: #H; nelim H
+nlemma decidable_SUN : ∀l.∀x,y:S_UN l.decidable (x = y).
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u2; #dim21; #dim22; nnormalize;
+                   napply (or2_elim … (decidable_bexpr (eq_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22))));
+ ##[ ##1: #H; napply (or2_intro1 (? = ?) (? ≠ ?) (eqSUN_to_eq l … H))
+ ##| ##2: #H; napply (or2_intro2 (? = ?) (? ≠ ?) (neqSUN_to_neq l … H))
  ##]
 nqed.
 
-(* getter della dimostrazione di appartenenza *)
-ndefinition getdim : ∀l.∀e:S_UN l.member_list UN ? eq_UN l = true.
- ##[ ##2: nelim e;
-          ##[ ##1: #u; #H; napply u
-          ##| ##2: #H; nelim H
-          ##]
- ##| ##1: #l; #s; nelim s;
-          ##[ ##1: #u; #m; napply m
-          ##| ##2: #H; nelim H
-          ##]
+nlemma symmetric_eqSUN : ∀l.symmetricT (S_UN l) bool (eq_SUN l).
+ #l; #x; nelim x;
+ ##[ ##2: #F; nelim F
+ ##| ##1: #u1; #dim11; #dim12; #y; nelim y;
+          ##[ ##2: #F; nelim F
+          ##| ##1: #u2; #dim21; #dim22;
+                   napply (or2_elim (? = ?) (? ≠ ?) ? (decidable_SUN l (S_EL l u1 dim11 dim12) (S_EL l u2 dim21 dim22)));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqSUN l … H);
+          napply (symmetric_eq ? (eq_SUN l ??) false);
+          napply (neq_to_neqSUN l … (symmetric_neq … H))
  ##]
 nqed.
 
-(* costruttore universale di una funzione ad un solo argomento: esadecimali → esadecimali *)
+(*
+ndefinition EX_UN ≝ [ ux0; ux1; ux2; ux3; ux4; ux5; ux6; ux7; ux8; ux9; uxA; uxB; uxC; uxD; uxE; uxF ].
+
 ndefinition f1_EX_UN
  : ∀e:S_UN EX_UN.
    ∀f1,f2,f3,f4,f5,f6,f7,f8,f9,f10,f11,f12,f13,f14,f15,f16:S_UN EX_UN.
@@ -743,7 +701,6 @@ ndefinition f1_EX_UN
  ##]
 nqed.
 
-(* esempio: successore esadecimale *)
 ndefinition succ_EX_UN ≝
 λe:S_UN EX_UN.f1_EX_UN
  (S_EL EX_UN ux1 (refl_eq …)) (S_EL EX_UN ux2 (refl_eq …))
@@ -754,138 +711,4 @@ ndefinition succ_EX_UN ≝
  (S_EL EX_UN uxB (refl_eq …)) (S_EL EX_UN uxC (refl_eq …))
  (S_EL EX_UN uxD (refl_eq …)) (S_EL EX_UN uxE (refl_eq …))
  (S_EL EX_UN uxF (refl_eq …)) (S_EL EX_UN ux0 (refl_eq …)).
-
-(* lemmi *)
-nlemma same_UN_1 : ∀l.∀e1,e2.∀dim1,dim2.S_EL l e1 dim1 = S_EL l e2 dim2 → e1 = e2.
- #l; #e1; #e2; #dim1; #dim2; #H;
- nchange with (match S_EL l e2 dim2 with [ S_EL a _ ⇒ e1 = a | S_KO _ ⇒ False ]);
- nrewrite < H;
- nnormalize;
- napply refl_eq.
-nqed.
-
-
-
-ndefinition destruct_SUN
- : ∀l.∀e1,e2:S_UN l.∀P:Prop.
-   e1 = e2 → match eq_UN (getelem ? e1) (getelem ? e2) with [ true ⇒ P → P | false ⇒ P ].
- #l; #e1; nelim e1;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #e2; ncases e2;
-          ##[ ##2: #H; nelim H
-          ##| ##1: #u2; #dim2; #P; #H;
-                   nchange with (match eq_UN u1 u2 with [ true ⇒ P → P | false ⇒ P ]);
-                   napply (destruct_UN u1 u2 P (same_UN_1 l … H))
-          ##]
- ##]
-nqed.
-
-
-
-nlemma eq_to_eqSUN
- : ∀l.∀e1,e2:S_UN l.(getelem ? e1) = (getelem ? e2) → eq_UN (getelem ? e1) (getelem ? e2) = true.
- #l; #e1; nelim e1;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #e2; ncases e2;
-          ##[ ##2: #H; nelim H;
-          ##| ##1: #u2; #dim2; nchange with ((u1 = u2) → (eq_UN u1 u2 = true));
-                   napply (eq_to_eqUN u1 u2);
-          ##]
- ##]
-nqed.
-
-nlet rec scan (T:Type) (e:T) (f:T → T → bool) (l:list T) (n:nat) on l ≝
- match l with
-  [ nil ⇒ None ?
-  | cons h t ⇒ match f e h with
-   [ true ⇒ Some ? n
-   | false ⇒ scan T e f t (S n)
-   ]
-  ].
-
-nlemma pippo : ∀l.∀x,y:S_UN l.x = y → scan ? (getelem ? x) eq_UN l O = scan ? (getelem ? y) eq_UN l O. 
- #l; nelim l;
- ##[ ##1: #x; #y; #H; nnormalize; napply refl_eq
- ##| ##2: #hh; #tt; #H; #x; nelim x;
-          ##[ ##2: #F; nelim F
-          ##| ##1: #u1; #dim1; #y; nelim y;
-                   ##[ ##2: #F; nelim F
-                   ##| ##1: #u2; #dim2; #H1;
-                            nchange with ((scan ? u1 ???) = (scan ? u2 ???));
-                            nrewrite > (same_UN_1 (hh::tt) … H1);
-                            nchange with 
-                            nletin K ≝ (same_UN_1 (hh::tt) … H1);
-                            nchange in K:(%) with (u1 = u2);
-                            nnormalize in K:(%);
-                            nrewrite > (same_UN_1 (hh::tt) … H1) in dim1:(%) dim2:(%) ⊢ %;
-                            nchange with (match eq_UN 
-                   
-                    nchange with (scan ? u1 eq_UN ? O = scan ? u2 eq_UN ? O);
- 
- #x; nelim x;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #y; nelim y;
-     ##[ ##2: #H; nelim H
-     ##| ##1: #u2; #dim2; #H; nchange with (scan ? u1 eq_UN l O = scan ? u2 eq_UN l O);
-              nrewrite > (same_UN_1 l … H);
-              nelim l in x:(%) dim1:(%) y:(%) dim2:(%) H:(%) ⊢ %;
-              ##[ ##1: #x; #dim1; #y; #dim2; #H; nnormalize; napply refl_eq
-              ##| ##2: #uu1; #ll; #H; #y;
-              nnormalize;
-
-nlemma decidable_UN : ∀x,y:UN.decidable (x = y).
- #x; nnormalize; #y;
- napply (Or2_ind);
- 
- 
-  napply (destruct_UN ? y (Or2 ??) ?);
-
-nlemma neq_to_neqUN
- : ∀l.∀e1,e2:S_UN l.(getelem ? e1) ≠ (getelem ? e2) → eq_UN (getelem ? e1) (getelem ? e2) = false.
- #l; #e1; nelim e1;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #e2; ncases e2;
-          ##[ ##2: #H; nelim H;
-          ##| ##1: #u2; #dim2; nchange with ((u1 ≠ u2) → (eq_UN u1 u2 = false));
-                   #H; nrewrite > H;
-                   nelim u2; nnormalize; napply refl_eq
-          ##]
- ##]
-nqed.
-
-                   nelim u1 in dim1:(%) H:(%) ⊢ %; #dim1; #H;
-                   ##[ ##1: nelim u2 in dim2:(%) H:(%) ⊢ %; #dim2; #H;
-                            napply (destruct_UN l (S_EL l uq0 dim1) ?? H);
-                   
-                   ##[ ##1: nelim u2; ##[ ##1:
-                    
-
-ndefinition decidable_UN : ∀l.∀e1,e2:S_UN l.decidable (e1 = e2).
- #l; #e1; ncases e1;
- ##[ ##2: #H; nelim H
- ##| ##1: #u1; #dim1; #e2; ncases e2;
-          ##[ ##2: #H; nelim H
-          ##| ##1: #u2; #dim2; nnormalize;
-                   napply (or2_intro2 (? = ?) (? ≠ ?) ?);
-                   nnormalize;
-                   #H;
-                   nchange with (match S_EL l u1 dim1
-                                  return λx.eq_UN x u2 → Prop
-                                 with
-                                  [ S_EL x _ ⇒ λp:(False
-                                  | S_KO H ⇒ True
-                                  ] (refl_eq ? (eq_UN u1 u2);
-                   nletin K ≝ (same_UN_1 l … H);
-                   nelim u1 in dim1:(%) H:(%) K:(%);
-                   #dim1; #H; #K;
-                   napply (destruct_UN l … H);
-
-
-
-
-
-
-
-
-
-
+*)
diff --git a/helm/software/matita/contribs/ng_assembly/common/theory.ma b/helm/software/matita/contribs/ng_assembly/common/theory.ma
index 7f5f90036..70b12fcc5 100644
--- a/helm/software/matita/contribs/ng_assembly/common/theory.ma
+++ b/helm/software/matita/contribs/ng_assembly/common/theory.ma
@@ -184,6 +184,14 @@ nlemma or2_elim
  napply H.
 nqed.
 
+nlemma symmetric_or2 : ∀P1,P2.Or2 P1 P2 → Or2 P2 P1.
+ #P1; #P2; #H;
+ napply (or2_elim P1 P2 ? H);
+ ##[ ##1: #H1; napply (or2_intro2 P2 P1 H1)
+ ##| ##2: #H1; napply (or2_intro1 P2 P1 H1)
+ ##]
+nqed.
+
 ninductive Or3 (A,B,C:Prop) : Prop ≝
   or3_intro1 : A → (Or3 A B C)
 | or3_intro2 : B → (Or3 A B C)
@@ -196,6 +204,33 @@ nlemma or3_elim
  napply H.
 nqed.
 
+nlemma symmetric_or3_12 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P2 P1 P3.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro2 P2 P1 P3 H1)
+ ##| ##2: #H1; napply (or3_intro1 P2 P1 P3 H1)
+ ##| ##3: #H1; napply (or3_intro3 P2 P1 P3 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or3_13 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P3 P2 P1.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro3 P3 P2 P1 H1)
+ ##| ##2: #H1; napply (or3_intro2 P3 P2 P1 H1)
+ ##| ##3: #H1; napply (or3_intro1 P3 P2 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or3_23 : ∀P1,P2,P3:Prop.Or3 P1 P2 P3 → Or3 P1 P3 P2.
+ #P1; #P2; #P3; #H;
+ napply (or3_elim P1 P2 P3 ? H);
+ ##[ ##1: #H1; napply (or3_intro1 P1 P3 P2 H1)
+ ##| ##2: #H1; napply (or3_intro3 P1 P3 P2 H1)
+ ##| ##3: #H1; napply (or3_intro2 P1 P3 P2 H1)
+ ##]
+nqed.
+
 ninductive Or4 (A,B,C,D:Prop) : Prop ≝
   or4_intro1 : A → (Or4 A B C D)
 | or4_intro2 : B → (Or4 A B C D)
@@ -210,6 +245,66 @@ nlemma or4_elim
  napply H.
 nqed.
 
+nlemma symmetric_or4_12 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P2 P1 P3 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro2 P2 P1 P3 P4 H1)
+ ##| ##2: #H1; napply (or4_intro1 P2 P1 P3 P4 H1)
+ ##| ##3: #H1; napply (or4_intro3 P2 P1 P3 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P2 P1 P3 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_13 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P3 P2 P1 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro3 P3 P2 P1 P4 H1)
+ ##| ##2: #H1; napply (or4_intro2 P3 P2 P1 P4 H1)
+ ##| ##3: #H1; napply (or4_intro1 P3 P2 P1 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P3 P2 P1 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_14 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P4 P2 P3 P1.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro4 P4 P2 P3 P1 H1)
+ ##| ##2: #H1; napply (or4_intro2 P4 P2 P3 P1 H1)
+ ##| ##3: #H1; napply (or4_intro3 P4 P2 P3 P1 H1)
+ ##| ##4: #H1; napply (or4_intro1 P4 P2 P3 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_23 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P3 P2 P4.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P3 P2 P4 H1)
+ ##| ##2: #H1; napply (or4_intro3 P1 P3 P2 P4 H1)
+ ##| ##3: #H1; napply (or4_intro2 P1 P3 P2 P4 H1)
+ ##| ##4: #H1; napply (or4_intro4 P1 P3 P2 P4 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_24 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P4 P3 P2.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P4 P3 P2 H1)
+ ##| ##2: #H1; napply (or4_intro4 P1 P4 P3 P2 H1)
+ ##| ##3: #H1; napply (or4_intro3 P1 P4 P3 P2 H1)
+ ##| ##4: #H1; napply (or4_intro2 P1 P4 P3 P2 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or4_34 : ∀P1,P2,P3,P4:Prop.Or4 P1 P2 P3 P4 → Or4 P1 P2 P4 P3.
+ #P1; #P2; #P3; #P4; #H;
+ napply (or4_elim P1 P2 P3 P4 ? H);
+ ##[ ##1: #H1; napply (or4_intro1 P1 P2 P4 P3 H1)
+ ##| ##2: #H1; napply (or4_intro2 P1 P2 P4 P3 H1)
+ ##| ##3: #H1; napply (or4_intro4 P1 P2 P4 P3 H1)
+ ##| ##4: #H1; napply (or4_intro3 P1 P2 P4 P3 H1)
+ ##]
+nqed.
+
 ninductive Or5 (A,B,C,D,E:Prop) : Prop ≝
   or5_intro1 : A → (Or5 A B C D E)
 | or5_intro2 : B → (Or5 A B C D E)
@@ -225,6 +320,116 @@ nlemma or5_elim
  napply H.
 nqed.
 
+nlemma symmetric_or5_12 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P2 P1 P3 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro2 P2 P1 P3 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro1 P2 P1 P3 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P2 P1 P3 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P2 P1 P3 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P2 P1 P3 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_13 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P3 P2 P1 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro3 P3 P2 P1 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P3 P2 P1 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro1 P3 P2 P1 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P3 P2 P1 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P3 P2 P1 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_14 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P4 P2 P3 P1 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro4 P4 P2 P3 P1 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P4 P2 P3 P1 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P4 P2 P3 P1 P5 H1)
+ ##| ##4: #H1; napply (or5_intro1 P4 P2 P3 P1 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P4 P2 P3 P1 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_15 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P5 P2 P3 P4 P1.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro5 P5 P2 P3 P4 P1 H1)
+ ##| ##2: #H1; napply (or5_intro2 P5 P2 P3 P4 P1 H1)
+ ##| ##3: #H1; napply (or5_intro3 P5 P2 P3 P4 P1 H1)
+ ##| ##4: #H1; napply (or5_intro4 P5 P2 P3 P4 P1 H1)
+ ##| ##5: #H1; napply (or5_intro1 P5 P2 P3 P4 P1 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_23 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P3 P2 P4 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P3 P2 P4 P5 H1)
+ ##| ##2: #H1; napply (or5_intro3 P1 P3 P2 P4 P5 H1)
+ ##| ##3: #H1; napply (or5_intro2 P1 P3 P2 P4 P5 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P3 P2 P4 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P3 P2 P4 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_24 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P4 P3 P2 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P4 P3 P2 P5 H1)
+ ##| ##2: #H1; napply (or5_intro4 P1 P4 P3 P2 P5 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P4 P3 P2 P5 H1)
+ ##| ##4: #H1; napply (or5_intro2 P1 P4 P3 P2 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P4 P3 P2 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_25 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P5 P3 P4 P2.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P5 P3 P4 P2 H1)
+ ##| ##2: #H1; napply (or5_intro5 P1 P5 P3 P4 P2 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P5 P3 P4 P2 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P5 P3 P4 P2 H1)
+ ##| ##5: #H1; napply (or5_intro2 P1 P5 P3 P4 P2 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_34 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P4 P3 P5.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P4 P3 P5 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P4 P3 P5 H1)
+ ##| ##3: #H1; napply (or5_intro4 P1 P2 P4 P3 P5 H1)
+ ##| ##4: #H1; napply (or5_intro3 P1 P2 P4 P3 P5 H1)
+ ##| ##5: #H1; napply (or5_intro5 P1 P2 P4 P3 P5 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_35 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P5 P4 P3.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P5 P4 P3 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P5 P4 P3 H1)
+ ##| ##3: #H1; napply (or5_intro5 P1 P2 P5 P4 P3 H1)
+ ##| ##4: #H1; napply (or5_intro4 P1 P2 P5 P4 P3 H1)
+ ##| ##5: #H1; napply (or5_intro3 P1 P2 P5 P4 P3 H1)
+ ##]
+nqed.
+
+nlemma symmetric_or5_45 : ∀P1,P2,P3,P4,P5:Prop.Or5 P1 P2 P3 P4 P5 → Or5 P1 P2 P3 P5 P4.
+ #P1; #P2; #P3; #P4; #P5; #H;
+ napply (or5_elim P1 P2 P3 P4 P5 ? H);
+ ##[ ##1: #H1; napply (or5_intro1 P1 P2 P3 P5 P4 H1)
+ ##| ##2: #H1; napply (or5_intro2 P1 P2 P3 P5 P4 H1)
+ ##| ##3: #H1; napply (or5_intro3 P1 P2 P3 P5 P4 H1)
+ ##| ##4: #H1; napply (or5_intro5 P1 P2 P3 P5 P4 H1)
+ ##| ##5: #H1; napply (or5_intro4 P1 P2 P3 P5 P4 H1)
+ ##]
+nqed.
+
 ninductive ex (A:Type) (Q:A → Prop) : Prop ≝
  ex_intro: ∀x:A.Q x → ex A Q.
 
-- 
2.39.2