- the confluence of context-senstitive parallel reduction (cpr) is closed!

[helm.git] / matita / matita / contribs / lambda-delta / Basic-2 / unfold / tpss_tpss.ma

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
index 28248cf5417f7ccdedb63869c20940c3ceca8c8a..a8492845333c75d7db27c49e501e832f53d1ee8b 100644 (file)
--- a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
@@ -19,9 +19,31 @@ include "Basic-2/unfold/tpss_lift.ma".
 
 (* 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.
+lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 → L ⊢ T1 [d, 1] ≫ T2.
+#L #T1 #T2 #d #H @(tpss_ind … H) -H T2 //
+#T #T2 #_ #HT2 #IHT1
+lapply (tps_trans_ge … IHT1 … HT2 ?) //
+qed.
+
+lemma tpss_strip_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.
+
+lemma tpss_strip_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.
+
+lemma tpss_strap1_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.
+
+lemma tpss_strap2_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.
 
 lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 →
@@ -31,7 +53,7 @@ lemma tpss_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* 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 // ]
+  elim (tpss_strap1_down … 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.