From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 26 Jul 2011 19:47:31 +0000 (+0000)
Subject: tpr: more inversion lemmas and a main property stated
X-Git-Tag: make_still_working~2349
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4c4b73b9ccf2e93901d0352599623c851781b74b;p=helm.git

tpr: more inversion lemmas and a main property stated
---

diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
index 498fbb744..a8aac61df 100644
--- a/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
+++ b/matita/matita/lib/lambda-delta/reduction/tpr_defs.ma
@@ -127,6 +127,18 @@ lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 →
                      ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
 /2/ qed.
 
+lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
+                     ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕓{I} V2. T2
+                      | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+                                   ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
+                                   U2 = 𝕚{Abbr} V2. T & I = Abbr
+                      | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
+#V1 #T1 #U2 * #H
+[ elim (tpr_inv_abbr1 … H) -H * /3 width=7/
+| /3/
+]
+qed.
+
 lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 →
                          ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
                                                 U2 = 𝕚{Appl} V2. T2
@@ -184,6 +196,24 @@ lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕚{Cast} V1. T1 ⇒ U2 →
                      ∨ T1 ⇒ U2.
 /2/ qed.
 
+lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
+                     ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
+                                            U2 = 𝕗{I} V2. T2
+                      | ∃∃V2,W,T1,T2.       V1 ⇒ V2 & T1 ⇒ T2 &
+                                            U0 = 𝕚{Abst} W. T1 &
+                                            U2 = 𝕓{Abbr} V2. T2 & I = Appl
+                      | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
+                                            ↑[0,1] V2 ≡ V &
+                                            U0 = 𝕚{Abbr} W1. T1 &
+                                            U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2 &
+                                            I = Appl
+                      |                     (U0 ⇒ U2 ∧ I = Cast).
+#V1 #U0 #U2 * #H
+[ elim (tpr_inv_appl1 … H) -H * /3 width=12/
+| elim (tpr_inv_cast1 … H) -H [1: *] /3 width=5/
+]
+qed.
+
 lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
                          ∨∨           T1 = #i
                           | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_ps.ma b/matita/matita/lib/lambda-delta/reduction/tpr_ps.ma
new file mode 100644
index 000000000..dc4a1098c
--- /dev/null
+++ b/matita/matita/lib/lambda-delta/reduction/tpr_ps.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "lambda-delta/reduction/lpr_defs.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+axiom tpr_ps_lpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
+                  ∀d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
+                  ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫ U2.
+
+lemma tpr_ps_bind: ∀I,V1,V2,T1,T2,U1. V1 ⇒ V2 → T1 ⇒ T2 →
+                   ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ≫ U1 →
+                   ∃∃U2. U1 ⇒ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ U2.
+/3 width=5/ qed.
diff --git a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
index da8a55071..6e632f72d 100644
--- a/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
+++ b/matita/matita/lib/lambda-delta/reduction/tpr_tpr.ma
@@ -9,111 +9,156 @@
      \ /
       V_______________________________________________________________ *)
 
+include "lambda-delta/substitution/lift_fun.ma".
 include "lambda-delta/substitution/lift_weight.ma".
 include "lambda-delta/reduction/tpr_main.ma".
+include "lambda-delta/reduction/tpr_ps.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 
 (* Confluence lemmas ********************************************************)
 
-lemma tpr_conf_sort_sort: ∀k1. ∃∃T0. ⋆k1 ⇒ T0 & ⋆k1 ⇒ T0.
+lemma tpr_conf_sort_sort: ∀k. ∃∃X. ⋆k ⇒ X & ⋆k ⇒ X.
 /2/ qed.
 
-lemma tpr_conf_lref_lref: ∀i1. ∃∃T0. #i1 ⇒ T0 & #i1 ⇒ T0.
+lemma tpr_conf_lref_lref: ∀i. ∃∃X. #i ⇒ X & #i ⇒ X.
 /2/ qed.
 
 lemma tpr_conf_bind_bind:
-   ∀I1,V11,V12,T11,T12,V22,T22. (
-      ∀T1. #T1 < #V11 + #T11 + 1 →
-      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
-      ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+   ∀I,V0,V1,T0,T1,V2,T2. (
+      ∀X0:term. #X0 < #V0 + #T0 + 1 →
+      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+      ∃∃X. X1 ⇒ X & X2 ⇒ X
+   ) →
+   V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
+   ∃∃X. 𝕓{I} V1. T1 ⇒ X & 𝕓{I} V2. T2 ⇒ X.
+#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
+elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
+qed.
+
+lemma tpr_conf_bind_delta:
+   ∀V0,V1,T0,T1,V2,T2,T. (
+      ∀X0:term. #X0 < #V0 + #T0 + 1 →
+      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+      ∃∃X. X1 ⇒ X & X2 ⇒ X
    ) →
-   V11 ⇒ V12 → T11 ⇒ T12 →
-   V11 ⇒ V22 → T11 ⇒ T22 →
-   ∃∃T0. 𝕓{I1} V12. T12 ⇒ T0 & 𝕓{I1} V22. T22 ⇒ T0.
-#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
-elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
-elim (IH … HT1 … HT2) -HT1 HT2 IH /3 width=5/
+   V0 ⇒ V1 → V0 ⇒ V2 →
+   T0 ⇒ T1 → T0 ⇒ T2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [O,1] ≫ T →
+   ∃∃X. 𝕓{Abbr} V1. T1 ⇒ X & 𝕓{Abbr} V2. T ⇒ X.
+#V0 #V1 #T0 #T1 #V2 #T2 #T #IH #HV01 #HV02 #HT01 #HT02 #HT2
+elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 HT02 IH // -V0 T0 #T0 #HT10 #HT20
+elim (tpr_ps_bind … HV2 HT20 … HT2) -HT20 HT2 /3 width=5/
 qed.
 
 lemma tpr_conf_bind_zeta:
-   ∀V11,V12,T11,T12,T22,T20. (
-      ∀T1. #T1 < #V11 + #T11 +1 →
-      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
-      ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+   ∀X2,V0,V1,T0,T1,T. (
+      ∀X0:term. #X0 < #V0 + #T0 +1 →
+      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+      ∃∃X. X1 ⇒ X & X2 ⇒ X
    ) →
-   V11 ⇒ V12 → T22 ⇒ T20 → T11 ⇒ T12 → ↑[O, 1] T22 ≡ T11 →
-   ∃∃T0. 𝕓{Abbr} V12. T12 ⇒ T0 & T20 ⇒ T0.
-#V11 #V12 #T11 #T12 #T22 #T20 #IH #HV112 #HT202 #HT112 #HT
-elim (tpr_inv_lift … HT112 … HT) -HT112 #T #HT12 #HT22
-lapply (tw_lift … HT) -HT #HT
-elim (IH … HT202 … HT22) -HT202 HT22 IH /3/
+   V0 ⇒ V1 → T0 ⇒ T1 → T ⇒ X2 → ↑[O, 1] T ≡ T0 →
+   ∃∃X. 𝕓{Abbr} V1. T1 ⇒ X & X2 ⇒ X.
+#X2 #V0 #V1 #T0 #T1 #T #IH #HV01 #HT01 #HTX2 #HT0
+elim (tpr_inv_lift … HT01 … HT0) -HT01 #U #HUT1 #HTU
+lapply (tw_lift … HT0) -HT0 #HT0
+elim (IH … HTX2 … HTU) -HTX2 HTU IH /3/
 qed.
 
 lemma tpr_conf_flat_flat:
-   ∀I1,V11,V12,T11,T12,V22,T22. (
-      ∀T1. #T1 < #V11 + #T11 + 1 →
-      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
-      ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+   ∀I,V0,V1,T0,T1,V2,T2. (
+      ∀X0:term. #X0 < #V0 + #T0 + 1 →
+      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+      ∃∃X. X1 ⇒ X & X2 ⇒ X
    ) →
-   V11 ⇒ V12 → T11 ⇒ T12 →
-   V11 ⇒ V22 → T11 ⇒ T22 →
-   ∃∃T0. 𝕗{I1} V12. T12 ⇒ T0 & 𝕗{I1} V22. T22 ⇒ T0.
-#I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
-elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
-elim (IH … HT1 … HT2) -HT1 HT2 /3 width=5/
+   V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
+   ∃∃T0. 𝕗{I} V1. T1 ⇒ T0 & 𝕗{I} V2. T2 ⇒ T0.
+#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
+elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/
 qed.
 
 lemma tpr_conf_flat_beta:
-   ∀V11,V12,T12,V22,W2,T21,T22. (
-      ∀T1. #T1 < #V11 + (#W2 + #T21 + 1) + 1 →
-      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
-      ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+   ∀V0,V1,T1,V2,W0,U0,T2. (
+      ∀X0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 →
+      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+      ∃∃X. X1 ⇒ X & X2 ⇒ X
    ) →
-   V11 ⇒ V12 → V11 ⇒ V22 →
-   T21 ⇒ T22 → 𝕓{Abst} W2. T21 ⇒ T12 →
-   ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} V22. T22 ⇒ T0.
-#V11 #V12 #T12 #V22 #W2 #T21 #T22 #IH #HV1 #HV2 #HT1 #HT2
-elim (tpr_inv_abst1 … HT2) -HT2 #W1 #T1 #HW21 #HT21 #H destruct -T12;
-elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV12 #HV22
-elim (IH … HT21 … HT1) -HT21 HT1 IH /3 width=5/
+   V0 ⇒ V1 → V0 ⇒ V2 →
+   U0 ⇒ T2 → 𝕓{Abst} W0. U0 ⇒ T1 →
+   ∃∃X. 𝕗{Appl} V1. T1 ⇒ X & 𝕓{Abbr} V2. T2 ⇒ X.
+#V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
+elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct -T1;
+elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
+elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/
 qed.
-(*
+
 lemma tpr_conf_flat_theta:
-   ∀V11,V12,T12,V2,V22,W21,W22,T21,T22. (
-      ∀T1. #T1 < #V11 + (#W21 + #T21 + 1) + 1 →
-      ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
-      ∃∃T0. T3 ⇒ T0 & T4 ⇒T0
+   ∀V0,V1,T1,V2,V,W0,W2,U0,U2. (
+      ∀X0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 →
+      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+      ∃∃X. X1 ⇒ X & X2 ⇒ X
    ) →
-   V11 ⇒ V12 → V11 ⇒ V22 → ↑[O,1] V22 ≡ V2 →
-   W21 ⇒ W22 → T21 ⇒ T22 →  𝕓{Abbr} W21. T21 ⇒ T12 →
-   ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} W22. 𝕗{Appl} V2. T22 ⇒T0.
-*)
-
+   V0 ⇒ V1 → V0 ⇒ V2 → ↑[O,1] V2 ≡ V →
+   W0 ⇒ W2 → U0 ⇒ U2 →  𝕓{Abbr} W0. U0 ⇒ T1 →
+   ∃∃X. 𝕗{Appl} V1. T1 ⇒ X & 𝕓{Abbr} W2. 𝕗{Appl} V. U2 ⇒ X.
+#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H 
+elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2
+elim (lift_total VV 0 1) #VVV #HVV
+lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
+elim (tpr_inv_abbr1 … H) -H *
+(* case 1: bind *)
+[ -HV2 HVV2 #WW #UU #HWW0 #HUU0 #H destruct -T1;
+  elim (IH … HW02 … HWW0) -HW02 HWW0 // #W #HW2 #HWW
+  elim (IH … HU02 … HUU0) -HU02 HUU0 IH // #U #HU2 #HUU
+  @ex2_1_intro
+  [2: @tpr_theta [5: @HVV1 |6: @HVV |7:// by {}; (*@HWW*) |8: @HUU |1,2,3,4:skip ]
+  |3: @tpr_bind [ @HW2 | @tpr_flat [ @HVVV | @HU2 ] ]
+  | skip 
 (* Confluence ***************************************************************)
-(*
+
 lemma tpr_conf_aux:
-   ∀T. (
-      ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
-      ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
+   ∀Y0:term. (
+      ∀X0:term. #X0 < #Y0 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+      ∃∃X. X1 ⇒ X & X2 ⇒ X
          ) →
-   ∀U1,T1,T2. U1 ⇒ T1 → U1 ⇒ T2 → U1 = T →
-   ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
-#T #IH  #U1 #T1 #T2 * -U1 T1
-[ #k1 #H1 #H2 destruct -T;
+   ∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 →
+   ∃∃X. X1 ⇒ X & X2 ⇒ X.
+#Y0 #IH #X0 #X1 #X2 * -X0 X1
+[ #k1 #H1 #H2 destruct -Y0;
   lapply (tpr_inv_sort1 … H1) -H1
-(* case 1: sort, sort *) 
-  #H1 destruct -T2 //
-| #i1 #H1 #H2 destruct -T;
+(* case 1: sort, sort *)
+  #H1 destruct -X2 //
+| #i1 #H1 #H2 destruct -Y0;
   lapply (tpr_inv_lref1 … H1) -H1
-(* case 2: lref, lref *) 
-  #H1 destruct -T2 //
-| #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 #H1 #H2 destruct -T;
-  lapply (tpr_inv_bind1 … H1) -H1
-  [ 
-
-theorem tpr_conf: ∀T,T1,T2. T ⇒ T1 → T ⇒ T2 →
-                 ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
+(* case 2: lref, lref *)
+  #H1 destruct -X2 //
+| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+  elim (tpr_inv_bind1 … H1) -H1 *
+(* case 3: bind, bind *)
+  [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+    @tpr_conf_bind_bind /2 width=7/ (**) (* /3 width=7/ is too slow *)
+(* case 4: bind, delta *)
+  | #V2 #T2 #T #HV02 #HT02 #HT2 #H1 #H2 destruct -X2 I
+    @tpr_conf_bind_delta /2 width=9/ (**) (* /3 width=9/ is too slow *)
+(* case 5: bind, zeta *)
+  | #T #HT0 #HTX2 #H destruct -I
+    @tpr_conf_bind_zeta /2 width=8/ (**) (* /3 width=8/ is too slow *)
+  ]
+| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
+  elim (tpr_inv_flat1 … H1) -H1 *
+(* case 6: flat, flat *)
+  [ #V2 #T2 #HV02 #HT02 #H destruct -X2
+    @tpr_conf_flat_flat /2 width=7/ (**) (* /3 width=7/ is too slow *)
+(* case 7: flat, beta *)
+  | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I
+    @tpr_conf_flat_beta /2 width=8/ (**) (* /3 width=8/ is too slow *)
+(* case 8: flat, theta *)
+  | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I  
+    //
+theorem tpr_conf: ∀T0,T1,T2. T0 ⇒ T1 → T0 ⇒ T2 →
+                  ∃∃T. T1 ⇒ T & T2 ⇒ T.
 #T @(tw_wf_ind … T) -T /3 width=6/
 qed.
 *)
@@ -218,3 +263,12 @@ lemma tpr_conf_flat_theta:
    W21 ⇒ W22 → T21 ⇒ T22 →  𝕓{Abbr} W21. T21 ⇒ T12 →
    ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} W22. 𝕗{Appl} V2. T22 ⇒T0.
 
+lemma tpr_conf_bind_delta:
+   ∀V0,V1,T0,T1,V2,T2,T. (
+      ∀X. #X < #V0 + #T0 + 1 →
+      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+      ∃∃X. X1 ⇒ X & X2⇒X
+   ) →
+   V0 ⇒ V1 → V0 ⇒ V2 →
+   T0 ⇒ T1 → T0 ⇒ T2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [O,1] ≫ T →
+   ∃∃X. 𝕓{Abbr} V1. T1 ⇒ X & 𝕓{Abbr} V2. T ⇒ X.
\ No newline at end of file
diff --git a/matita/matita/lib/lambda-delta/xoa_defs.ma b/matita/matita/lib/lambda-delta/xoa_defs.ma
index af9ba3708..9dbf226f4 100644
--- a/matita/matita/lib/lambda-delta/xoa_defs.ma
+++ b/matita/matita/lib/lambda-delta/xoa_defs.ma
@@ -28,6 +28,12 @@ inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
 
+inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
+   | ex3_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3_1 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2).
+
 inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
    | ex3_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → ex3_2 ? ? ? ? ?
 .
@@ -52,12 +58,30 @@ inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : P
 
 interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3).
 
+inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→Prop) : Prop ≝
+   | ex5_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → ex5_3 ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 3)" 'Ex P0 P1 P2 P3 P4 = (ex5_3 ? ? ? P0 P1 P2 P3 P4).
+
+inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop) : Prop ≝
+   | ex5_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → ex5_4 ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
+
 inductive ex6_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝
    | ex6_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → ex6_6 ? ? ? ? ? ? ? ? ? ? ? ?
 .
 
 interpretation "multiple existental quantifier (6, 6)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
 
+inductive ex7_6 (A0,A1,A2,A3,A4,A5:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→Prop) : Prop ≝
+   | ex7_6_intro: ∀x0,x1,x2,x3,x4,x5. P0 x0 x1 x2 x3 x4 x5 → P1 x0 x1 x2 x3 x4 x5 → P2 x0 x1 x2 x3 x4 x5 → P3 x0 x1 x2 x3 x4 x5 → P4 x0 x1 x2 x3 x4 x5 → P5 x0 x1 x2 x3 x4 x5 → P6 x0 x1 x2 x3 x4 x5 → ex7_6 ? ? ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 6)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_6 ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
 inductive or3 (P0,P1,P2:Prop) : Prop ≝
    | or3_intro0: P0 → or3 ? ? ?
    | or3_intro1: P1 → or3 ? ? ?
@@ -66,3 +90,12 @@ inductive or3 (P0,P1,P2:Prop) : Prop ≝
 
 interpretation "multiple disjunction connective (3)" 'Or P0 P1 P2 = (or3 P0 P1 P2).
 
+inductive or4 (P0,P1,P2,P3:Prop) : Prop ≝
+   | or4_intro0: P0 → or4 ? ? ? ?
+   | or4_intro1: P1 → or4 ? ? ? ?
+   | or4_intro2: P2 → or4 ? ? ? ?
+   | or4_intro3: P3 → or4 ? ? ? ?
+.
+
+interpretation "multiple disjunction connective (4)" 'Or P0 P1 P2 P3 = (or4 P0 P1 P2 P3).
+
diff --git a/matita/matita/lib/lambda-delta/xoa_notation.ma b/matita/matita/lib/lambda-delta/xoa_notation.ma
index 18b3c0293..e37c37eb1 100644
--- a/matita/matita/lib/lambda-delta/xoa_notation.ma
+++ b/matita/matita/lib/lambda-delta/xoa_notation.ma
@@ -22,6 +22,10 @@ notation "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0},${ident x1}.$P0) (λ${ident x0},${ident x1}.$P1) }.
 
+notation "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }.
+
 notation "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0},${ident x1}.$P0) (λ${ident x0},${ident x1}.$P1) (λ${ident x0},${ident x1}.$P2) }.
@@ -38,11 +42,27 @@ notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P3) }.
 
+notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0},${ident x1},${ident x2}.$P0) (λ${ident x0},${ident x1},${ident x2}.$P1) (λ${ident x0},${ident x1},${ident x2}.$P2) (λ${ident x0},${ident x1},${ident x2}.$P3) (λ${ident x0},${ident x1},${ident x2}.$P4) }.
+
+notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P3) (λ${ident x0},${ident x1},${ident x2},${ident x3}.$P4) }.
+
 notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P3) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P4) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P5) }.
 
-notation "hvbox(∨∨ term 19 P0 break | term 19 P1 break | term 19 P2)"
+notation "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)"
  non associative with precedence 20
+ for @{ 'Ex (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P0) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P1) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P2) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P3) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P4) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P5) (λ${ident x0},${ident x1},${ident x2},${ident x3},${ident x4},${ident x5}.$P6) }.
+
+notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)"
+ non associative with precedence 30
  for @{ 'Or $P0 $P1 $P2 }.
 
+notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2 break | term 29 P3)"
+ non associative with precedence 30
+ for @{ 'Or $P0 $P1 $P2 $P3 }.
+