From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 15 Sep 2011 21:43:51 +0000 (+0000)
Subject: unfold on terms completed!
X-Git-Tag: make_still_working~2282
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=64306edf6d64730ab9aa6648ad11d9dfa68775d9;p=helm.git

unfold on terms completed!
---

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma
index 29b99ae41..5a2f86aca 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps.ma
@@ -52,7 +52,7 @@ qed.
 lemma tps_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫ T2 →
                 ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 →
                 L ⊢ T1 [d2, e2] ≫ T2.
-#L #T1 #T #d1 #e1 #H elim H -L T1 T d1 e1
+#L #T1 #T2 #d1 #e1 #H elim H -H L T1 T2 d1 e1
 [ //
 | #L #K #V #W #i #d1 #e1 #Hid1 #Hide1 #HLK #HVW #d2 #e2 #Hd12 #Hde12
   lapply (transitive_le … Hd12 … Hid1) -Hd12 Hid1 #Hid2
@@ -64,7 +64,7 @@ qed.
 
 lemma tps_weak_top: ∀L,T1,T2,d,e.
                     L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 [d, |L| - d] ≫ T2.
-#L #T1 #T #d #e #H elim H -L T1 T d e
+#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
 [ //
 | #L #K #V #W #i #d #e #Hdi #_ #HLK #HVW
   lapply (drop_fwd_drop2_length … HLK) #Hi
@@ -77,14 +77,14 @@ qed.
 
 lemma tps_weak_all: ∀L,T1,T2,d,e.
                     L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 [0, |L|] ≫ T2.
-#L #T1 #T #d #e #HT12
+#L #T1 #T2 #d #e #HT12
 lapply (tps_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
 lapply (tps_weak_top … HT12) //
 qed.
 
 lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. d ≤ i → i ≤ d + e →
                     ∃∃T. L ⊢ T1 [d, i - d] ≫ T & L ⊢ T [i, d + e - i] ≫ T2.
-#L #T1 #T2 #d #e #H elim H -L T1 T2 d e
+#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
 [ /2/
 | #L #K #V #W #i #d #e #Hdi #Hide #HLK #HVW #j #Hdj #Hjde
   elim (lt_or_ge i j)
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
index 58ebb3dd3..c5fca2ca3 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
@@ -17,6 +17,26 @@ include "Basic-2/substitution/tps.ma".
 
 (* PARTIAL SUBSTITUTION ON TERMS ********************************************)
 
+(* Advanced inversion lemmas ************************************************)
+
+fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
+                           ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
+[ //
+| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e;
+  >(le_to_le_to_eq … Hdi ?) /2/ -d #K #V #HLK
+  lapply (drop_mono … HLK0 … HLK) #H destruct
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
+  >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 /2/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
+  >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 … HLK) -IHT12 //
+]
+qed.
+
+lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 →
+                        ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+/2 width=8/ qed.
+
 (* Relocation properties ****************************************************)
 
 (* Basic-1: was: subst1_lift_lt *)
@@ -178,23 +198,3 @@ lapply (tps_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt Hdtde #H
 lapply (tps_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct -U1;
 elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 HLK HTU1 // <minus_plus_m_m /2/
 qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
-                           ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
-#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
-[ //
-| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e;
-  >(le_to_le_to_eq … Hdi ?) /2/ -d #K #V #HLK
-  lapply (drop_mono … HLK0 … HLK) #H destruct
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
-  >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 /2/
-| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
-  >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 … HLK) -IHT12 //
-]
-qed.
-
-lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 →
-                        ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
-/2 width=8/ qed.
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss.ma
index 26b97dcb4..2c90c9f86 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss.ma
@@ -24,3 +24,108 @@ interpretation "partial unfold (term)"
 
 (* Basic properties *********************************************************)
 
+lemma tpss_ind: ∀d,e,L,T1. ∀R: term → Prop. R T1 →
+                (∀T,T2. L ⊢ T1 [d, e] ≫* T → L ⊢ T[d, e] ≫ T2 → R T → R T2) →
+                ∀T2. L ⊢ T1 [d, e] ≫* T2 → R T2.
+#d #e #L #T1 #R #HT1 #IHT1 #T2 #HT12 @(TC_star_ind … HT1 IHT1 … HT12) //
+qed.
+
+lemma tpss_leq_repl_dx: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
+                        ∀L2. L1 [d, e] ≈ L2 → L2 ⊢ T1 [d, e] ≫* T2.
+/3/ qed.
+
+lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ≫* T.
+/2/ qed.
+
+lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ≫* V2 →
+                 ∀I,T1,T2. L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 →
+                 L ⊢ 𝕓{I} V1. T1 [d, e] ≫* 𝕓{I} V2. T2.
+#L #V1 #V2 #d #e #HV12 elim HV12 -HV12 V2
+[ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -HT12 T2
+  [ /3 width=5/
+  | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+  ]
+| #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12
+  lapply (tpss_leq_repl_dx … HT12 (L. 𝕓{I} V) ?) -HT12 /2/ #HT12
+  lapply (IHV … HT12) -IHV HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+]
+qed.
+
+lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e.
+                 L ⊢ V1 [d, e] ≫ * V2 → L ⊢ T1 [d, e] ≫* T2 →
+                 L ⊢ 𝕗{I} V1. T1 [d, e] ≫* 𝕗{I} V2. T2.
+#L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -HV12 V2
+[ #V2 #HV12 #HT12 elim HT12 -HT12 T2
+  [ /3/
+  | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+  ]
+| #V #V2 #_ #HV12 #IHV #HT12
+  lapply (IHV … HT12) -IHV HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+]
+qed.
+
+lemma tpss_weak: ∀L,T1,T2,d1,e1. L ⊢ T1 [d1, e1] ≫* T2 →
+                 ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 →
+                 L ⊢ T1 [d2, e2] ≫* T2.
+#L #T1 #T2 #d1 #e1 #H #d1 #d2 #Hd21 #Hde12 @(tpss_ind … H) -H T2
+[ //
+| #T #T2 #_ #HT12 #IHT
+  lapply (tps_weak … HT12 … Hd21 Hde12) -HT12 Hd21 Hde12 /2/
+]
+qed.
+
+lemma tpss_weak_top: ∀L,T1,T2,d,e.
+                     L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 [d, |L| - d] ≫* T2.
+#L #T1 #T2 #d #e #H @(tpss_ind … H) -H T2
+[ //
+| #T #T2 #_ #HT12 #IHT
+  lapply (tps_weak_top … HT12) -HT12 /2/
+]
+qed.
+
+lemma tpss_weak_all: ∀L,T1,T2,d,e.
+                     L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 [0, |L|] ≫* T2.
+#L #T1 #T2 #d #e #HT12
+lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
+lapply (tpss_weak_top … HT12) //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+(* Note: this can be derived from tpss_inv_atom1 *)
+lemma tpss_inv_sort1: ∀L,T2,k,d,e. L ⊢ ⋆k [d, e] ≫* T2 → T2 = ⋆k.
+#L #T2 #k #d #e #H @(tpss_ind … H) -H T2
+[ //
+| #T #T2 #_ #HT2 #IHT destruct -T
+  >(tps_inv_sort1 … HT2) -HT2 //
+]
+qed.
+
+lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ≫* U2 →
+                      ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & 
+                               L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ≫* T2 &
+                               U2 =  𝕓{I} V2. T2.
+#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -H U2
+[ /2 width=5/
+| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
+  elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
+  lapply (tpss_leq_repl_dx … HT1 (L. 𝕓{I} V2) ?) -HT1 /3 width=5/
+]
+qed.
+
+lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ≫* U2 →
+                      ∃∃V2,T2. L ⊢ V1 [d, e] ≫* V2 & L ⊢ T1 [d, e] ≫* T2 &
+                               U2 =  𝕗{I} V2. T2.
+#d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -H U2
+[ /2 width=5/
+| #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct -U;
+  elim (tps_inv_flat1 … HU2) -HU2 /3 width=5/
+]
+qed.
+
+lemma tpss_inv_refl_O2: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫* T2 → T1 = T2.
+#L #T1 #T2 #d #H @(tpss_ind … H) -H T2
+[ //
+| #T #T2 #_ #HT2 #IHT <(tps_inv_refl_O2 … HT2) -HT2 //
+]
+qed.
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_lift.ma
new file mode 100644
index 000000000..f28ff3896
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_lift.ma
@@ -0,0 +1,131 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "Basic-2/substitution/tps_lift.ma".
+include "Basic-2/unfold/tpss.ma".
+
+(* PARTIAL UNFOLD ON TERMS **************************************************)
+
+(* Advanced properties ******************************************************)
+
+lemma tpss_subst: ∀L,K,V,U1,i,d,e.
+                  d ≤ i → i < d + e →
+                  ↓[0, i] L ≡ K. 𝕓{Abbr} V → K ⊢ V [0, d + e - i - 1] ≫* U1 →
+                  ∀U2. ↑[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ≫* U2.
+#L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -H U1
+[ /3/
+| #U #U1 #_ #HU1 #IHU #U2 #HU12
+  elim (lift_total U 0 (i+1)) #U0 #HU0
+  lapply (IHU … HU0) -IHU #H
+  lapply (drop_fwd_drop2 … HLK) -HLK #HLK
+  lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 HLK HU0 HU12 // normalize #HU02
+  lapply (tps_weak … HU02 d e ? ?) -HU02 [ >arith_i2 // | /2/ | /2/ ]
+]
+qed.
+
+(* Advanced inverion lemmas *************************************************)
+
+lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫* T2 →
+                      T2 = 𝕒{I} ∨
+                      ∃∃K,V1,V2,i. d ≤ i & i < d + e &
+                                   ↓[O, i] L ≡ K. 𝕓{Abbr} V1 &
+                                   K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
+                                   ↑[O, i + 1] V2 ≡ T2 &
+                                   I = LRef i.
+#L #T2 #I #d #e #H @(tpss_ind … H) -H T2
+[ /2/
+| #T #T2 #_ #HT2 *
+  [ #H destruct -T;
+    elim (tps_inv_atom1 … HT2) -HT2 [ /2/ | * /3 width=10/ ]
+  | * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
+    lapply (drop_fwd_drop2 … HLK) #H
+    elim (tps_inv_lift1_up … HT2 … H … HVT ? ? ?) normalize -HT2 H HVT [2,3,4: /2/ ] #V2 <minus_plus #HV2 #HVT2
+    @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2/ (**) (* /4 width=10/ is too slow *)
+  ]
+]
+qed.
+
+lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫* T2 →
+                      T2 = #i ∨
+                      ∃∃K,V1,V2. d ≤ i & i < d + e &
+                                 ↓[O, i] L ≡ K. 𝕓{Abbr} V1 &
+                                 K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
+                                 ↑[O, i + 1] V2 ≡ T2.
+#L #T2 #i #d #e #H
+elim (tpss_inv_atom1 … H) -H /2/
+* #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct -i /3 width=6/
+qed.
+
+lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 →
+                         ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -H T2 //
+#T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
+qed.
+
+(* Relocation properties ****************************************************)
+
+lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
+                    ∀L,U1,d,e. dt + et ≤ d → ↓[d, e] L ≡ K →
+                    ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 →
+                    L ⊢ U1 [dt, et] ≫* U2.
+#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -H T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+  elim (lift_total T d e) #U #HTU
+  lapply (IHT … HTU) -IHT #HU1
+  lapply (tps_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 HLK HTU HTU2 /2/
+]
+qed.
+
+lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
+                    ∀L,U1,d,e. d ≤ dt → ↓[d, e] L ≡ K →
+                    ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 →
+                    L ⊢ U1 [dt + e, et] ≫* U2.
+#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -H T2
+[ #U2 #H >(lift_mono … HTU1 … H) -H //
+| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
+  elim (lift_total T d e) #U #HTU
+  lapply (IHT … HTU) -IHT #HU1
+  lapply (tps_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 HLK HTU HTU2 /2/
+]
+qed.
+
+lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
+                         ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
+                         dt + et ≤ d →
+                         ∃∃T2. K ⊢ T1 [dt, et] ≫* T2 & ↑[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -H U2
+[ /2/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 HLK HTU /3/
+]
+qed.
+
+lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
+                         ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
+                         d + e ≤ dt →
+                         ∃∃T2. K ⊢ T1 [dt - e, et] ≫* T2 & ↑[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -H U2
+[ /2/
+| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
+  elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 HLK HTU /3/
+]
+qed.
+
+lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
+                         L ⊢ U1 [d, e] ≫* U2 → ∀T1. ↑[d, e] T1 ≡ U1 → U1 = U2.
+#L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -H U2 //
+#U #U2 #_ #HU2 #IHU destruct -U1
+<(tps_inv_lift1_eq … HU2 … HTU1) -HU2 HTU1 //
+qed.
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
new file mode 100644
index 000000000..28248cf54
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
@@ -0,0 +1,71 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "Basic-2/substitution/tps_tps.ma".
+include "Basic-2/unfold/tpss_lift.ma".
+
+(* PARTIAL UNFOLD ON TERMS **************************************************)
+
+(* Advanced properties ******************************************************)
+
+lemma tpss_trans_down_strap1: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫* T0 →
+                              ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 → d2 + e2 ≤ d1 →
+                              ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T [d1, e1] ≫* T2.
+/3/ qed.
+
+lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 →
+                     ∀i. d ≤ i → i ≤ d + e →
+                     ∃∃T. L ⊢ T1 [d, i - d] ≫* T & L ⊢ T [i, d + e - i] ≫* T2.
+#L #T1 #T2 #d #e #H #i #Hdi #Hide @(tpss_ind … H) -H T2
+[ /2/
+| #T #T2 #_ #HT12 * #T3 #HT13 #HT3
+  elim (tps_split_up … HT12 … Hdi Hide) -HT12 Hide #T0 #HT0 #HT02
+  elim (tpss_trans_down_strap1 … HT3 … HT0 ?) -T [2: <plus_minus_m_m_comm // ]
+  /3 width=7 by ex2_1_intro, step/ (**) (* just /3 width=7/ is too slow *)
+]
+qed.
+
+lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
+                         ∀K,d,e. ↓[d, e] L ≡ K → ∀T1. ↑[d, e] T1 ≡ U1 →
+                         d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
+                         ∃∃T2. K ⊢ T1 [d, dt + et - (d + e)] ≫* T2 & ↑[d, e] T2 ≡ U2.
+#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
+elim (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
+lapply (tpss_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt Hdtde #HU1
+lapply (tpss_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct -U1;
+elim (tpss_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 HLK HTU1 // <minus_plus_m_m /2/
+qed.
+
+(* Main properties **********************************************************)
+
+theorem tpss_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫* T1 →
+                      ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫* T2 →
+                      ∃∃T. L ⊢ T1 [d2, e2] ≫* T & L ⊢ T2 [d1, e1] ≫* T.
+/3/ qed.
+
+theorem tpss_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ≫* T1 →
+                       ∀L2,T2,d2,e2. L2 ⊢ T0 [d2, e2] ≫* T2 →
+                       (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
+                       ∃∃T. L2 ⊢ T1 [d2, e2] ≫* T & L1 ⊢ T2 [d1, e1] ≫* T.
+/3/ qed.
+
+theorem tpss_trans_eq: ∀L,T1,T,T2,d,e.
+                       L ⊢ T1 [d, e] ≫* T → L ⊢ T [d, e] ≫* T2 →
+                       L ⊢ T1 [d, e] ≫* T2. 
+/2/ qed.
+
+theorem tpss_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ≫* T0 →
+                         ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫* T2 → d2 + e2 ≤ d1 →
+                         ∃∃T. L ⊢ T1 [d2, e2] ≫* T & L ⊢ T [d1, e1] ≫* T2.
+/3/ qed.
diff --git a/matita/matita/contribs/lambda-delta/Ground-2/star.ma b/matita/matita/contribs/lambda-delta/Ground-2/star.ma
index d15768c53..f3cdd97e0 100644
--- a/matita/matita/contribs/lambda-delta/Ground-2/star.ma
+++ b/matita/matita/contribs/lambda-delta/Ground-2/star.ma
@@ -17,32 +17,89 @@ include "Ground-2/xoa_props.ma".
 
 (* PROPERTIES of RELATIONS **************************************************)
 
-definition confluent: ∀A. ∀R: relation A. Prop ≝ λA,R.
-                      ∀a0,a1. R a0 a1 → ∀a2. R a0 a2 →
-                      ∃∃a. R a1 a & R a2 a.
-
-lemma TC_strip: ∀A,R. confluent A R →
-                ∀a0,a1. TC … R a0 a1 → ∀a2. R a0 a2 →
-                ∃∃a. R a1 a & TC … R a2 a.
-#A #R #HR #a0 #a1 #H elim H -H a1
+definition confluent: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
+                      ∀a0,a1. R1 a0 a1 → ∀a2. R2 a0 a2 →
+                      ∃∃a. R2 a1 a & R1 a2 a.
+
+definition transitive: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
+                       ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 →
+                       ∃∃a. R2 a1 a & R1 a a2.
+
+lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 →
+                 ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
+                 ∃∃a. R2 a1 a & TC … R1 a2 a.
+#A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
 [ #a1 #Ha01 #a2 #Ha02
-  elim (HR … Ha01 … Ha02) -HR a0 /3/
+  elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
   elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
-  elim (HR … Ha1 … Ha0) -HR a /4/
+  elim (HR12 … Ha1 … Ha0) -HR12 a /4/
+]
+qed.
+
+lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 →
+                 ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 →
+                 ∃∃a. R1 a2 a & TC … R2 a1 a.
+#A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
+[ #a2 #Ha02 #a1 #Ha01
+  elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
+| #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01
+  elim (IHa0 … Ha01) -IHa0 Ha01 a0 #a0 #Ha0 #Ha21
+  elim (HR12 … Ha0 … Ha2) -HR12 a /4/
 ]
 qed.
 
-lemma TC_confluent: ∀A,R. confluent A R → confluent A (TC … R).
-#A #R #HR #a0 #a1 #H elim H -H a1
+lemma TC_confluent: ∀A,R1,R2.
+                    confluent A R1 R2 → confluent A (TC … R1) (TC … R2).
+#A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
 [ #a1 #Ha01 #a2 #Ha02
-  elim (TC_strip … HR … Ha02 … Ha01) -HR a0 /3/
+  elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 a0 /3/
 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
   elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
-  elim (TC_strip … HR … Ha0 … Ha1) -HR a /4/
+  elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 a /4/
+]
+qed.
+
+lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 →
+                 ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 →
+                 ∃∃a. R2 a1 a & TC … R1 a a2.
+#A #R1 #R2 #HR12 #a1 #a0 #H elim H -H a0
+[ #a0 #Ha10 #a2 #Ha02
+  elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
+| #a #a0 #_ #Ha0 #IHa #a2 #Ha02
+  elim (HR12 … Ha0 … Ha02) -HR12 a0 #a0 #Ha0 #Ha02
+  elim (IHa … Ha0) -a /4/
+]
+qed.
+
+lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 →
+                 ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 →
+                 ∃∃a. R1 a a2 & TC … R2 a1 a.
+#A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
+[ #a2 #Ha02 #a1 #Ha10
+  elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
+| #a #a2 #_ #Ha02 #IHa #a1 #Ha10
+  elim (IHa … Ha10) -a0 #a0 #Ha0 #Ha10
+  elim (HR12 … Ha0 … Ha02) -HR12 a /4/
+]
+qed.
+
+lemma TC_transitive: ∀A,R1,R2.
+                     transitive A R1 R2 → transitive A (TC … R1) (TC … R2).
+#A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
+[ #a0 #Ha10 #a2 #Ha02
+  elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 a0 /3/
+| #a #a0 #_ #Ha0 #IHa #a2 #Ha02
+  elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 a0 #a0 #Ha02 #Ha0
+  elim (IHa … Ha0) -a /4/
 ]
 qed.
 
 lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
 /2/ qed.
 
+lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:A→Prop.
+                   P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
+                   ∀a2. TC … R a1 a2 → P a2.
+#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
+qed.
diff --git a/matita/matita/contribs/lambda-delta/Ground-2/xoa.conf.xml b/matita/matita/contribs/lambda-delta/Ground-2/xoa.conf.xml
index e7f9feef4..f749fe18a 100644
--- a/matita/matita/contribs/lambda-delta/Ground-2/xoa.conf.xml
+++ b/matita/matita/contribs/lambda-delta/Ground-2/xoa.conf.xml
@@ -24,6 +24,7 @@
     <key name="ex">4 4</key>
     <key name="ex">5 3</key>
     <key name="ex">5 4</key>
+    <key name="ex">6 4</key>
     <key name="ex">6 6</key>
     <key name="ex">7 6</key>
     <key name="or">3</key>
diff --git a/matita/matita/contribs/lambda-delta/Ground-2/xoa.ma b/matita/matita/contribs/lambda-delta/Ground-2/xoa.ma
index a9deb0fa1..2b7af4503 100644
--- a/matita/matita/contribs/lambda-delta/Ground-2/xoa.ma
+++ b/matita/matita/contribs/lambda-delta/Ground-2/xoa.ma
@@ -96,6 +96,14 @@ inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop)
 
 interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
 
+(* multiple existental quantifier (6, 4) *)
+
+inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝
+   | ex6_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 → P5 x0 x1 x2 x3 → ex6_4 ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (6, 4)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_4 ? ? ? ? P0 P1 P2 P3 P4 P5).
+
 (* multiple existental quantifier (6, 6) *)
 
 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 ≝
diff --git a/matita/matita/contribs/lambda-delta/Ground-2/xoa_notation.ma b/matita/matita/contribs/lambda-delta/Ground-2/xoa_notation.ma
index 5f747314c..47e3268b4 100644
--- a/matita/matita/contribs/lambda-delta/Ground-2/xoa_notation.ma
+++ b/matita/matita/contribs/lambda-delta/Ground-2/xoa_notation.ma
@@ -114,6 +114,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }.
 
+(* multiple existental quantifier (6, 4) *)
+
+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 break & term 19 P5)"
+ 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) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) }.
+
+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 break & term 19 P5)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) }.
+
 (* multiple existental quantifier (6, 6) *)
 
 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)"
diff --git a/matita/matita/contribs/lambda-delta/replace.sh b/matita/matita/contribs/lambda-delta/replace.sh
new file mode 100644
index 000000000..6caaacdb8
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/replace.sh
@@ -0,0 +1,8 @@
+#!/bin/sh
+for V in `cat Make`; do
+   echo ${V}; sed "s/$1/$2/g" ${V} > ${V}.new
+   if diff ${V} ${V}.new > /dev/null; 
+      then rm -f ${V}.new; else mv -f ${V}.new ${V}; fi
+done
+
+unset V