From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 18 Oct 2012 14:57:26 +0000 (+0000)
Subject: - some confluence results for focalized reduction and computation
X-Git-Tag: make_still_working~1491
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c09a0b1f8801e40612eef429b82fc6dbae01b85;p=helm.git

- some confluence results for focalized reduction and computation
- more notation to be used later on ....
---

diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index 178f0d0a8..d64855d0d 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -168,8 +168,6 @@ pc3/props pc3_eta
 
 pr0/fwd pr0_gen_void
 pr0/dec nf0_dec
-pr0/subst1 pr0_subst1_back
-pr0/subst1 pr0_subst1_fwd
 
 pr1/props pr1_eta
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma
new file mode 100644
index 000000000..bf429672a
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reducibility/fpr.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+definition fprs: bi_relation lenv term ≝ bi_TC … fpr.
+
+interpretation "context-free parallel computation (closure)"
+   'FocalizedPRedStar L1 T1 L2 T2 = (fprs L1 T1 L2 T2).
+
+(* Basic properties *********************************************************)
+
+lemma fprs_refl: bi_reflexive … fprs.
+/2 width=1/ qed.
+
+lemma fprs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ →
+                   ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+/2 width=4/ qed.
+
+lemma fprs_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ →
+                   ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
+/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_aaa.ma
new file mode 100644
index 000000000..b76637ff7
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_aaa.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 "basic_2/reducibility/cfpr_aaa.ma".
+include "basic_2/computation/fprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_fprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A →
+                     ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A.
+#L1 #T1 #A #HT1 #L2 #T2 #HLT12
+@(bi_TC_Conf3 … HT1 ?? HLT12) /2 width=4/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_fprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_fprs.ma
new file mode 100644
index 000000000..e0c1b3058
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/fprs_fprs.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reducibility/fpr_fpr.ma".
+include "basic_2/computation/fprs.ma".
+
+(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma fprs_strip: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ➡ ⦃L1, T1⦄ →
+                  ∀L2,T2. ⦃L0, T0⦄ ➡* ⦃L2, T2⦄ →
+                  ∃∃L,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ & ⦃L2, T2⦄ ➡ ⦃L, T⦄.
+#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8
+/2 width=4/ qed.
+
+(* Main propertis ***********************************************************)
+
+theorem fprs_conf: bi_confluent … fprs.
+/2 width=4/ qed.
+
+theorem fprs_trans: bi_transitive … fprs.
+/2 width=4/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma
index a1337787c..5c6cd31cb 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/lfprs_aaa.ma
@@ -23,9 +23,3 @@ lemma aaa_lfprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡* ⦃L2
 #L1 #T #A #HT #L2 #HL12
 @(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3/
 qed.
-(*
-(* Note: this should be rephrased in terms of fprs *)
-lemma aaa_lfprs_cprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A → ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ →
-                           ∀T2. L2 ⊢ T1 ➡* T2 → L2 ⊢ T2 ⁝ A.
-/3 width=3/ qed.
-*)
diff --git a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
index 810083108..7012ec11e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_delift.ma
@@ -19,53 +19,6 @@ include "basic_2/equivalence/cpcs_cpcs.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
 
-(* Advanced inversion lemmas ************************************************)
-(* does not holds
-axiom cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → (
-                           ∃∃V2,T2.    L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
-                                       L ⊢ U2 ➡* ⓐV2. T2
-                           ) ∨
-                           ∃∃a,V2,W,T. L ⊢ V1 ➡* V2 &
-                                       L ⊢ T1 ➡* ⓛ{a}W. T & L ⊢ ⓓ{a}V2. T ⬌* U2.
-#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
-#U #U2 #_ #HU2 * *
-[ #V0 #T0 #HV10 #HT10 #HUT0
-  elim (cprs_strip … HUT0 … HU2) -U #U #H #HU2
-  elim (cpr_inv_appl1 … H) -H *
-  [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
-  | #b #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
-    lapply (cprs_strap1 … HV10 HV02) -V0 #HV12
-    lapply (cprs_div ? (ⓓ{b}V2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=7/
-  | #b #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
-    lapply (cprs_strap1 … HV10 HV0) -V0 #HV1
-    lapply (cprs_trans … HT10 (ⓓ{b}W2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1
-    elim (sfr_delift (L.ⓓW2) (ⓐV2.T2) 0 1 ? ?) // #X #H1
-    lapply (cprs_zeta_delift … H1) #H2
-    lapply (cprs_trans … HU2 … H2) -HU2 -H2 #HU2T3
-    elim (delift_inv_flat1 … H1) -H1 #V3 #T3 #HV23 #HT23 #H destruct
-    lapply (delift_inv_lift1_eq … HV23 … HV2) -V2 [ /2 width=1/ | skip ] #H destruct
-    lapply (cprs_zeta_delift … HT23) -HT23 #H
-    lapply (cprs_trans … HT1 … H) -W2 -T2 /3 width=5/
-  ]
-| /4 width=8/
-]
-qed-.
-*)
-(* maybe holds
-axiom cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U →
-                          ∃∃W0,T0,V1,T1. L ⊢ T ➡* ⓛW0.T0 &
-                                         L ⊢ ⓓV.T0 ➡* ⓛV1.T1 &
-                                         L ⊢ ⓛW.U ➡* ⓛV1.T1.
-#L #V #T #W #U #H
-elim (cprs_inv_appl1_cpcs … H) -H *
-[ #V0 #T0 #HV0 #HT0 #H
-  elim (cprs_inv_abst1 Abst W … H) -H #W0 #U0 #_ #_ #H destruct
-| #V0 #W0 #T0 #HV0 #HT0 #H
-  elim (cpcs_inv_abst2 … H) -H #V1 #T1 #H1 #H2
-  lapply (cprs_trans … (ⓓV.T0) … H1) -H1 /2 width=1/ -V0 /2 width=7/
-]
-qed-.
-*)
 (* Properties on inverse basic term relocation ******************************)
 
 lemma cpcs_zeta_delift_comm: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 →
diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma
index 4d5d308fa..7489da188 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma
@@ -15,20 +15,6 @@
 (* THE FORMAL SYSTEM λδ: MATITA SOURCE FILES
  * Suggested invocation to start formal specifications with:
  *   - Patience on me to gain peace and perfection! -
- * 2012 July 26:
- *   term binders polarized to control ζ reduction.
- * 2012 April 16 (anniversary milestone):
- *   context-sensitive subject equivalence for atomic arity assignment.
- * 2012 March 15:
- *   context-sensitive strong normalization for simply typed terms.
- * 2012 January 27:
- *   support for abstract candidates of reducibility.
- * 2011 September 21:
- *   confluence for context-sensitive parallel reduction. 
- * 2011 September 6:
- *   confluence for context-free parallel reduction.
- * 2011 April 17:
- *   specification starts.
  *)
 
 include "ground_2/star.ma".
diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index 42f62ca15..4e67f393a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -342,10 +342,22 @@ notation "hvbox( T1 ➡ ➡ * break term 46 T2 )"
    non associative with precedence 45
    for @{ 'PRedStarAlt $T1 $T2 }.
 
-notation "hvbox( ⦃ L1 ⦄ ➡ * ⦃ L2 ⦄ )"
+notation "hvbox( ⦃ L1 ⦄ ➡ * break ⦃ L2 ⦄ )"
    non associative with precedence 45
    for @{ 'FocalizedPRedStar $L1 $L2 }.
 
+notation "hvbox( ⦃ L1 , T1 ⦄ ➡ * break ⦃ L2 , T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPRedStar $L1 $T1 $L2 $T2 }.
+
+notation "hvbox( ⦃ L1 ⦄ ➡ ➡ * break ⦃ L2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPRedStarAlt $L1 $L2 }.
+
+notation "hvbox( ⦃ L1 , T1 ⦄ ➡ ➡ * break ⦃ L2 , T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'FocalizedPRedStarAlt $L1 $T1 $L2 $T2 }.
+
 notation "hvbox( L ⊢ break term 46 T1 ➡ * break 𝐍 ⦃ T2 ⦄ )"
    non associative with precedence 45
    for @{ 'PEval $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cfpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cfpr.ma
new file mode 100644
index 000000000..f442be28b
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cfpr_cfpr.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 "basic_2/reducibility/cpr_cpr.ma".
+include "basic_2/reducibility/cfpr.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON CLOSURES *************************)
+
+(* Main properties **********************************************************)
+
+theorem cfpr_conf: ∀L. bi_confluent … (cfpr L).
+#L #L0 #L1 #T0 #T1 * #HL01 #HT01 #L2 #T2 * >HL01 #HL12 #HT02
+elim (cpr_conf … HT01 HT02) -L0 -T0 #X #H1 #H2
+elim (cpr_fwd_shift1 … H1) #L0 #T0 #HL10 #H destruct /3 width=5/
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
index 5a572d5e1..22fbfc148 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
@@ -86,6 +86,15 @@ elim (tpr_inv_cast1 … H) -H /3 width=3/
 elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
 qed-.
 
+(* Basic forward lemmas *****************************************************)
+
+lemma cpr_fwd_shift1: ∀L,L1,T1,T. L ⊢ L1 @@ T1 ➡ T →
+                      ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#L #L1 #T1 #T * #X #H1 #H2
+elim (tpr_fwd_shift1 … H1) -H1 #L0 #T0 #HL10 #H destruct
+elim (tpss_fwd_shift1 … H2) -H2 #L2 #T2 #HL02 #H destruct /2 width=4/
+qed-.
+
 (* Basic_1: removed theorems 6: 
             pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
             pr2_gen_ctail pr2_ctail
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma
index c8adecd25..5e1ba7992 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma
@@ -27,6 +27,7 @@ interpretation
 
 (* Basic properties *********************************************************)
 
+(* Note: lemma 250 *)
 lemma lfpr_refl: ∀L. ⦃L⦄ ➡ ⦃L⦄.
 /2 width=3/ qed.
 
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tps.ma
new file mode 100644
index 000000000..12cf13c0f
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tps.ma
@@ -0,0 +1,57 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reducibility/ltpr_ldrop.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
+
+(* Properties on parallel substitution for terms ****************************)
+
+(* Basic_1: was: pr0_subst1_fwd *)
+lemma ltpr_tpr_conf: ∀L1,T,U1,d,e. L1 ⊢ T ▶ [d, e] U1 → ∀L2. L1 ➡ L2 →
+                     ∃∃U2. U1 ➡ U2 & L2 ⊢ T ▶ [d, e] U2.
+#L1 #T #U1 #d #e #H elim H -L1 -T -U1 -d -e
+[ /2 width=3/
+| #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #L2 #HL12
+  elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
+  elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct -K1
+  elim (lift_total V2 0 (i+1)) #W2 #HVW2
+  lapply (tpr_lift … HV12 … HVW1 … HVW2) -V1 /3 width=6/
+| #L1 #a #I #V #W1 #T #U1 #d #e #_ #_ #IHV #IHT #L2 #HL12
+  elim (IHV … HL12) -IHV #W2 #HW12
+  elim (IHT (L2.ⓑ{I}W2) ?) -IHT /2 width=1/ -L1 /3 width=5/
+| #L1 #I #V #W1 #T #U1 #d #e #_ #_ #IHV #IHT #L2 #HL12
+  elim (IHV … HL12) -IHV
+  elim (IHT … HL12) -IHT -HL12 /3 width=5/
+]
+qed.
+
+(* Basic_1: was: pr0_subst1_back *)
+lemma ltpr_tps_trans: ∀L2,T,U2,d,e. L2 ⊢ T ▶ [d, e] U2 → ∀L1. L1 ➡ L2 →
+                      ∃∃U1. U1 ➡ U2 & L1 ⊢ T ▶ [d, e] U1.
+#L2 #T #U2 #d #e #H elim H -L2 -T -U2 -d -e
+[ /2 width=3/
+| #L2 #K2 #V2 #W2 #i #d #e #Hdi #Hide #HLK2 #HVW2 #L1 #HL12
+  elim (ltpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+  elim (ltpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV12 #H destruct -K2
+  elim (lift_total V1 0 (i+1)) #W1 #HVW1
+  lapply (tpr_lift … HV12 … HVW1 … HVW2) -V2 /3 width=6/
+| #L2 #a #I #V #W2 #T #U2 #d #e #_ #_ #IHV #IHT #L1 #HL12
+  elim (IHV … HL12) -IHV #W1 #HW12
+  elim (IHT (L1.ⓑ{I}W1) ?) -IHT /2 width=1/ -L2 /3 width=5/
+| #L2 #I #V #W2 #T #U2 #d #e #_ #_ #IHV #IHT #L1 #HL12
+  elim (IHV … HL12) -IHV
+  elim (IHT … HL12) -IHT -HL12 /3 width=5/
+]
+qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma
index f3ea69327..e1ead4e44 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/unfold/ltpss_dx_ltpss_dx.ma".
-include "basic_2/reducibility/ltpr_ldrop.ma".
+include "basic_2/reducibility/tpr_tps.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 
@@ -25,16 +25,8 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
                     ∀L2. L1 ➡ L2 →
                     ∃∃U2. U1 ➡ U2 & L2 ⊢ T2 ▶* [d, e] U2.
 #T1 #T2 #H elim H -T1 -T2
-[ #I #L1 #d #e #X #H
-  elim (tps_inv_atom1 … H) -H
-  [ #H destruct /2 width=3/
-  | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct
-    elim (ltpr_ldrop_conf … HLK1 … HL12) -L1 #X #H #HLK2
-    elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct
-    elim (lift_total V2 0 (i+1)) #U2 #HVU2
-    lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 #HU12
-    @ex2_1_intro [2: @HU12 | skip | /3 width=4/ ] (**) (* /4 width=6/ is too slow *)
-  ]
+[ #I #L1 #d #e #U1 #H #L2 #HL12
+  elim (ltpr_tpr_conf … H … HL12) -L1 /3 width=3/
 | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
   elim (IHV12 … HVW1 … HL12) -V1
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 26dd58ee6..93916208b 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
@@ -170,3 +170,13 @@ lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}.
 lapply (tps_fwd_tw … HT2) -HT2 #HT2
 @(transitive_le … IHT1) //
 qed-.
+
+lemma tpss_fwd_shift1: ∀L,L1,T1,T,d,e. L ⊢ L1 @@ T1 ▶*[d, e] T →
+                       ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#L #L1 #T1 #T #d #e #H @(tpss_ind … H) -T
+[ /2 width=4/
+| #T #X #_ #H0 * #L0 #T0 #HL10 #H destruct
+  elim (tps_fwd_shift1 … H0) -H0 #L2 #T2 #HL02 #H destruct /2 width=4/
+]
+qed-.
+  
\ No newline at end of file
diff --git a/matita/matita/contribs/lambda_delta/ground_2/star.ma b/matita/matita/contribs/lambda_delta/ground_2/star.ma
index 2779a0940..1e46a48c6 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/star.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/star.ma
@@ -134,3 +134,25 @@ lemma NF_to_SN_sn: ∀A,R,S,a. NF_sn A R S a → SN_sn A R S a.
 @SN_sn_intro #a1 #HRa12 #HSa12
 elim (HSa12 ?) -HSa12 /2 width=1/
 qed.
+
+lemma bi_TC_strip: ∀A,B,R. bi_confluent A B R →
+                   ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. bi_TC … R a0 b0 a2 b2 →
+                   ∃∃a,b. bi_TC … R a1 b1 a b & R a2 b2 a b.
+#A #B #R #HR #a0 #a1 #b0 #b1 #H01 #a2 #b2 #H elim H -a2 -b2
+[ #a2 #b2 #H02
+  elim (HR … H01 … H02) -HR -a0 -b0 /3 width=4/
+| #a2 #b2 #a3 #b3 #_ #H23 * #a #b #H1 #H2
+  elim (HR … H23 … H2) -HR -a0 -b0 -a2 -b2 /3 width=4/
+]
+qed.
+
+lemma bi_TC_confluent: ∀A,B,R. bi_confluent A B R →
+                       bi_confluent A B (bi_TC … R).
+#A #B #R #HR #a0 #a1 #b0 #b1 #H elim H -a1 -b1
+[ #a1 #b1 #H01 #a2 #b2 #H02
+  elim (bi_TC_strip … HR … H01 … H02) -a0 -b0 /3 width=4/
+| #a1 #b1 #a3 #b3 #_ #H13 #IH #a2 #b2 #H02
+  elim (IH … H02) -a0 -b0 #a0 #b0 #H10 #H20
+  elim (bi_TC_strip … HR … H13 … H10) -a1 -b1 /3 width=7/
+]
+qed.
diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 57403f356..d74380de4 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -23,6 +23,9 @@ definition relation : Type[0] → Type[0]
 definition relation2 : Type[0] → Type[0] → Type[0]
 ≝ λA,B.A→B→Prop.
 
+definition relation3 : Type[0] → Type[0] → Type[0] → Type[0]
+≝ λA,B,C.A→B→C→Prop.
+
 definition reflexive: ∀A.∀R :relation A.Prop
 ≝ λA.λR.∀x:A.R x x.
 
@@ -163,3 +166,7 @@ definition bi_relation: Type[0] → Type[0] → Type[0]
 
 definition bi_reflexive: ∀A,B. ∀R:bi_relation A B. Prop
 ≝ λA,B,R. ∀x,y. R x y x y.
+
+definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
+                          ∀a1,a,b1,b. R a1 b1 a b →
+                          ∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2.
diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index 166ba5d7e..d8d08d09a 100644
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -254,3 +254,27 @@ definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
 lemma TC_Conf3: ∀A,B,S,R. Conf3 A B S R → Conf3 A B S (TC … R).
 #A #B #S #R #HSR #b #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/
 qed.
+
+inductive bi_TC (A,B:Type[0]) (R:bi_relation A B) (a:A) (b:B): A → B → Prop ≝
+  |bi_inj : ∀c,d. R a b c d → bi_TC A B R a b c d
+  |bi_step: ∀c,d,e,f. bi_TC A B R a b c d → R c d e f → bi_TC A B R a b e f.
+
+lemma bi_TC_reflexive: ∀A,B,R. bi_reflexive A B R →
+                       bi_reflexive A B (bi_TC … R).
+/2 width=1/ qed.
+
+lemma bi_TC_strap: ∀A,B. ∀R:bi_relation A B. ∀a1,a,a2,b1,b,b2.
+                   R a1 b1 a b → bi_TC … R a b a2 b2 → bi_TC … R a1 b1 a2 b2.
+#A #B #R #a1 #a #a2 #b1 #b #b2 #HR #H elim H -a2 -b2 /2 width=4/ /3 width=4/
+qed.
+
+lemma bi_TC_transitive: ∀A,B,R. bi_transitive A B (bi_TC … R).
+#A #B #R #a1 #a #b1 #b #H elim H -a -b /2 width=4/ /3 width=4/
+qed.
+
+definition bi_Conf3: ∀A,B,C. relation3 A B C → bi_relation A B → Prop ≝ λA,B,C,S,R.
+                     ∀c,a1,b1. S a1 b1 c → ∀a2,b2. R a1 b1 a2 b2 → S a2 b2 c.
+
+lemma bi_TC_Conf3: ∀A,B,C,S,R. bi_Conf3 A B C S R → bi_Conf3 A B C S (bi_TC … R).
+#A #B #C #S #R #HSR #c #a1 #b1 #Hab1 #a2 #b2 #H elim H -a2 -b2 /2 width=4/
+qed.