+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/ltpss.ma".
-
-(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
-
-definition ltpsss: nat → nat → relation lenv ≝
- λd,e. TC … (ltpss d e).
-
-interpretation "repeated partial unfold (local environment)"
- 'PSubstStars L1 d e L2 = (ltpsss d e L1 L2).
-
-(* Basic eliminators ********************************************************)
-
-lemma ltpsss_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 →
- (∀L,L2. L1 [d, e] ▶** L → L [d, e] ▶* L2 → R L → R L2) →
- ∀L2. L1 [d, e] ▶** L2 → R L2.
-#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
-qed-.
-
-lemma ltpsss_ind_dx: ∀d,e,L2. ∀R:predicate lenv. R L2 →
- (∀L1,L. L1 [d, e] ▶* L → L [d, e] ▶** L2 → R L → R L1) →
- ∀L1. L1 [d, e] ▶** L2 → R L1.
-#d #e #L2 #R #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma ltpsss_strap1: ∀L1,L,L2,d,e.
- L1 [d, e] ▶** L → L [d, e] ▶* L2 → L1 [d, e] ▶** L2.
-/2 width=3/ qed.
-
-lemma ltpsss_strap2: ∀L1,L,L2,d,e.
- L1 [d, e] ▶* L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2.
-/2 width=3/ qed.
-
-lemma ltpsss_refl: ∀L,d,e. L [d, e] ▶** L.
-/2 width=1/ qed.
-
-lemma ltpsss_weak_all: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → L1 [0, |L2|] ▶** L2.
-#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 //
-#L #L2 #_ #HL2
->(ltpss_fwd_length … HL2) /3 width=5/
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma ltpsss_fwd_length: ∀L1,L2,d,e. L1 [d, e] ▶** L2 → |L1| = |L2|.
-#L1 #L2 #d #e #H @(ltpsss_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL12 >IHL12 -IHL12
-/2 width=3 by ltpss_fwd_length/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma ltpsss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ▶** L2 → L1 = L2.
-#d #L1 #L2 #H @(ltpsss_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL <(ltpss_inv_refl_O2 … HL2) -HL2 //
-qed-.
-
-lemma ltpsss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶** L2 → L2 = ⋆.
-#d #e #L2 #H @(ltpsss_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL destruct
->(ltpss_inv_atom1 … HL2) -HL2 //
-qed-.
-
-lemma ltpsss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶** ⋆ → L1 = ⋆.
-#d #e #L1 #H @(ltpsss_ind_dx … H) -L1 //
-#L1 #L #HL1 #_ #IHL2 destruct
->(ltpss_inv_atom2 … HL1) -HL1 //
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/ltpss_ldrop.ma".
-include "basic_2/unfold/ltpsss.ma".
-
-(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
-
-lemma ltpsss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
- d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
-#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1 // /3 width=6/
-qed.
-
-lemma ltpsss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
- d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
-#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 // /3 width=6/
-qed.
-
-lemma ltpsss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L2 [0, d1 + e1 - e2] ▶** L & ⇩[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1
-[ /2 width=3/
-| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
- elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0
- elim (ltpss_ldrop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3 width=3/
-]
-qed.
-
-lemma ltpsss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L [0, d1 + e1 - e2] ▶** L2 & ⇩[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0
-[ /2 width=3/
-| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
- elim (ltpss_ldrop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0
- elim (IHL … HL0 Hd1e2 He2de1) -L /3 width=3/
-]
-qed.
-
-lemma ltpsss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L2 [d1 - e2, e1] ▶** L & ⇩[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H @(ltpsss_ind … H) -L1
-[ /2 width=3/
-| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
- elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0
- elim (ltpss_ldrop_conf_le … HL1 … HL0 He2d1) -L /3 width=3/
-]
-qed.
-
-lemma ltpsss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L [d1 - e2, e1] ▶** L2 & ⇩[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0
-[ /2 width=3/
-| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1
- elim (ltpss_ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0
- elim (IHL … HL0 He2d1) -L /3 width=3/
-]
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/ltpss_ltpss.ma".
-include "basic_2/unfold/ltpsss_tpss.ma".
-
-(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma ltpsss_strip: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
- ∀L2,d2,e2. L0 [d2, e2] ▶* L2 →
- ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶** L.
-/3 width=3/ qed.
-
-lemma ltpsss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 →
- ∀T2,U2. L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2.
-#L0 #L1 #d #e #H @(ltpsss_ind … H) -L1
-[ /2 width=1/
-| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2
- lapply (ltpss_tpss_trans_eq … HTU2 … HL1) -HL1 -HTU2 /2 width=1/
-]
-qed.
-
-lemma ltpsss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 →
- ∀T2,U2. L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2.
-/3 width=3/ qed.
-
-lemma ltpsss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 →
- ∀L2,ds,es. L1 [ds, es] ▶** L2 →
- ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T.
-#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpsss_ind … H) -L2
-[ /2 width=3/
-| -HT12 #L #L2 #HL1 #HL2 * #T #HT1 #HT2
- lapply (ltpsss_strap1 … HL1 HL2) -HL1 #HL12
- elim (ltpss_tpss_conf … HT1 … HL2) -L #T0 #HT10 #HT0
- lapply (ltpsss_tpss_trans_eq … HL12 … HT0) -HL12 -HT0 #HT0
- lapply (tpss_trans_eq … HT2 HT0) -T /2 width=3/
-]
-qed.
-
-lemma ltpsss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 →
- ∀L2,ds,es. L1 [ds, es] ▶** L2 →
- ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T.
-/3 width=1/ qed.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma ltpsss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶** L2 →
- ∃∃K2,V2. K1 [0, e - 1] ▶** K2 &
- K1 ⊢ V1 [0, e - 1] ▶* V2 &
- L2 = K2. ⓑ{I} V2.
-#e #K1 #I #V1 #L2 #He #H @(ltpsss_ind … H) -L2
-[ /2 width=5/
-| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
- elim (ltpss_inv_tpss21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
- lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2
- lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/
-]
-qed-.
-
-lemma ltpsss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶** L2 →
- ∃∃K2,V2. K1 [d - 1, e] ▶** K2 &
- K1 ⊢ V1 [d - 1, e] ▶* V2 &
- L2 = K2. ⓑ{I} V2.
-#d #e #K1 #I #V1 #L2 #Hd #H @(ltpsss_ind … H) -L2
-[ /2 width=5/
-| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
- elim (ltpss_inv_tpss11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
- lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2
- lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/
-]
-qed-.
-
-lemma ltpsss_fwd_tpss22: ∀I,L1,K2,V2,e. L1 [0, e] ▶** K2. ⓑ{I} V2 → 0 < e →
- ∃∃K1,V1. K1 [0, e - 1] ▶** K2 &
- K1 ⊢ V1 [0, e - 1] ▶* V2 &
- L1 = K1. ⓑ{I} V1.
-#I #L1 #K2 #V2 #e #H #He @(ltpsss_ind_dx … H) -L1
-[ /2 width=5/
-| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
- elim (ltpss_inv_tpss22 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct
- lapply (tpss_trans_eq … HV1 HV2) -V #HV12
- lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/
-]
-qed-.
-
-lemma ltpsss_inv_tpss12: ∀I,L1,K2,V2,d,e. L1 [d, e] ▶** K2. ⓑ{I} V2 → 0 < d →
- ∃∃K1,V1. K1 [d - 1, e] ▶** K2 &
- K1 ⊢ V1 [d - 1, e] ▶* V2 &
- L1 = K1. ⓑ{I} V1.
-#I #L1 #K2 #V2 #d #e #H #Hd @(ltpsss_ind_dx … H) -L1
-[ /2 width=5/
-| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
- elim (ltpss_inv_tpss12 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct
- lapply (tpss_trans_eq … HV1 HV2) -V #HV12
- lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/
-]
-qed-.
-
-(* Main properties **********************************************************)
-
-theorem ltpsss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
- ∀L2,d2,e2. L0 [d2, e2] ▶** L2 →
- ∃∃L. L1 [d2, e2] ▶** L & L2 [d1, e1] ▶** L.
-/3 width=3/ qed.
-
-theorem ltpsss_trans_eq: ∀L1,L,L2,d,e.
- L1 [d, e] ▶** L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2.
-/2 width=3/ qed.
-
-lemma ltpsss_tpss2: ∀L1,L2,I,V1,V2,e.
- L1 [0, e] ▶** L2 → L2 ⊢ V1 [0, e] ▶* V2 →
- L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
-[ /2 width=1/
-| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/
-]
-qed.
-
-lemma ltpsss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
- L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
- 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) // /2 width=1/
-qed.
-
-lemma ltpsss_tpss1: ∀L1,L2,I,V1,V2,d,e.
- L1 [d, e] ▶** L2 → L2 ⊢ V1 [d, e] ▶* V2 →
- L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
-[ /2 width=1/
-| #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/
-]
-qed.
-
-lemma ltpsss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
- L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 →
- 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) // /2 width=1/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/ltpss_tps.ma".
-include "basic_2/unfold/ltpsss.ma".
-
-(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
-
-(* Properties concerning partial substitution on terms **********************)
-
-lemma ltpsss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
- ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
- d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶ U2.
-#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 //
-#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
-lapply (ltpss_tps_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/
-qed.
-
-lemma ltpsss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
- L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶** L1 →
- L1 ⊢ T2 [d2, e2] ▶ U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 //
--HTU2 #L #L1 #_ #HL1 #IHL
-lapply (ltpss_tps_conf_ge … IHL … HL1 ?) -HL1 -IHL //
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/ltpss_tpss.ma".
-include "basic_2/unfold/ltpsss.ma".
-
-(* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
-
-(* Properties concerning partial substitution on terms **********************)
-
-lemma ltpsss_tps2: ∀L1,L2,I,e.
- L1 [0, e] ▶** L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 →
- L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2.
-#L1 #L2 #I #e #H @(ltpsss_ind … H) -L2
-[ /3 width=1/
-| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
- elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
- lapply (IHL … HV1) -IHL -HV1 /3 width=5/
-]
-qed.
-
-lemma ltpsss_tps2_lt: ∀L1,L2,I,V1,V2,e.
- L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
- 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) // /2 width=1/
-qed.
-
-lemma ltpsss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶** L2 →
- ∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 →
- L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2.
-#L1 #L2 #I #d #e #H @(ltpsss_ind … H) -L2
-[ /3 width=1/
-| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
- elim (ltpss_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
- lapply (IHL … HV1) -IHL -HV1 /3 width=5/
-]
-qed.
-
-lemma ltpsss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
- L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
- 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) // /2 width=1/
-qed.
-
-(* Properties concerning partial unfold on terms ****************************)
-
-lemma ltpsss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
- L0 ⊢ T2 [d2, e2] ▶* U2 → L0 [d1, e1] ▶** L1 →
- L1 ⊢ T2 [d2, e2] ▶* U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 //
--HTU2 #L #L1 #_ #HL1 #IHL
-lapply (ltpss_tpss_conf_ge … IHL … HL1 ?) -HL1 -IHL //
-qed.
-
-lemma ltpsss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
- ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶* U2 →
- d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶* U2.
-#L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 //
-#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
-lapply (ltpss_tpss_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
-(* *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-(* Unfold *******************************************************************)
-
-notation "hvbox( T1 break [ d , break e ] ▶** break T2 )"
- non associative with precedence 45
- for @{ 'PSubstStars $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'PSubstStarAlt $L $T1 $d $e $T2 }.
+notation "hvbox( T1 break ⊢ ▶ * [ d , break e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStarSn $T1 $d $e $T2 }.
+
+notation "hvbox( T1 break ⊢ ▶ ▶ * [ d , break e ] break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'PSubstStarSnAlt $T1 $d $e $T2 }.
+
notation "hvbox( ▼ * [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'TSubst $T1 $d $e $T2 }.
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/unfold/ltpss_sn_alt.ma".
include "basic_2/unfold/delift.ma".
(* INVERSE BASIC TERM RELOCATION *******************************************)
-(* Properties on partial unfold on local environments ***********************)
+(* Properties on sn partial unfold on local environments ********************)
-lemma delift_ltpss_conf_eq: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 →
- ∀K. L ▶* [d, e] K → K ⊢ ▼*[d, e] T1 ≡ T2.
+lemma delift_ltpss_sn_conf_eq: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 →
+ ∀K. L ⊢ ▶* [d, e] K → K ⊢ ▼*[d, e] T1 ≡ T2.
#L #T1 #T2 #d #e * #T #HT1 #HT2 #K #HLK
-elim (ltpss_tpss_conf … HT1 … HLK) -L #T0 #HT10 #HT0
+elim (ltpss_sn_tpss_conf … HT1 … HLK) -HT1 -HLK #T0 #HT10 #HT0
lapply (tpss_inv_lift1_eq … HT0 … HT2) -HT0 #H destruct /2 width=3/
qed.
-lemma ltpss_delift_trans_eq: ∀L,K,d,e. L ▶* [d, e] K →
- ∀T1,T2. K ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2.
+lemma ltpss_sn_delift_trans_eq: ∀L,K,d,e. L ⊢ ▶* [d, e] K →
+ ∀T1,T2. K ⊢ ▼*[d, e] T1 ≡ T2 → L ⊢ ▼*[d, e] T1 ≡ T2.
#L #K #d #e #HLK #T1 #T2 * #T #HT1 #HT2
-lapply (ltpss_tpss_trans_eq … HT1 … HLK) -K /2 width=3/
+lapply (ltpss_sn_tpss_trans_eq … HT1 … HLK) -K /2 width=3/
qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/tpss.ma".
-
-(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
-
-(* Basic_1: includes: csubst1_bind *)
-inductive ltpss: nat → nat → relation lenv ≝
-| ltpss_atom : ∀d,e. ltpss d e (⋆) (⋆)
-| ltpss_pair : ∀L,I,V. ltpss 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
-| ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
- ltpss 0 e L1 L2 → L2 ⊢ V1 ▶* [0, e] V2 →
- ltpss 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
-| ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
- ltpss d e L1 L2 → L2 ⊢ V1 ▶* [d, e] V2 →
- ltpss (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
-.
-
-interpretation "parallel unfold (local environment)"
- 'PSubstStar L1 d e L2 = (ltpss d e L1 L2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact ltpss_inv_refl_O2_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → e = 0 → L1 = L2.
-#d #e #L1 #L2 #H elim H -d -e -L1 -L2 //
-[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct
- >(IHL12 ?) -IHL12 // >(tpss_inv_refl_O2 … HV12) //
-]
-qed.
-
-lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 ▶* [d, 0] L2 → L1 = L2.
-/2 width=4/ qed-.
-
-fact ltpss_inv_atom1_aux: ∀d,e,L1,L2.
- L1 ▶* [d, e] L2 → L1 = ⋆ → L2 = ⋆.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ //
-| #L #I #V #H destruct
-| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
-]
-qed.
-
-lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ ▶* [d, e] L2 → L2 = ⋆.
-/2 width=5/ qed-.
-
-fact ltpss_inv_tpss21_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e →
- ∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. K1 ▶* [0, e - 1] K2 &
- K2 ⊢ V1 ▶* [0, e - 1] V2 &
- L2 = K2. ⓑ{I} V2.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #e #_ #_ #K1 #I #V1 #H destruct
-| #L1 #I #V #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct /2 width=5/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma ltpss_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 ▶* [0, e] L2 → 0 < e →
- ∃∃K2,V2. K1 ▶* [0, e - 1] K2 &
- K2 ⊢ V1 ▶* [0, e - 1] V2 &
- L2 = K2. ⓑ{I} V2.
-/2 width=5/ qed-.
-
-fact ltpss_inv_tpss11_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d →
- ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
- ∃∃K2,V2. K1 ▶* [d - 1, e] K2 &
- K2 ⊢ V1 ▶* [d - 1, e] V2 &
- L2 = K2. ⓑ{I} V2.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #e #_ #I #K1 #V1 #H destruct
-| #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct /2 width=5/
-]
-qed.
-
-lemma ltpss_inv_tpss11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 ▶* [d, e] L2 → 0 < d →
- ∃∃K2,V2. K1 ▶* [d - 1, e] K2 &
- K2 ⊢ V1 ▶* [d - 1, e] V2 &
- L2 = K2. ⓑ{I} V2.
-/2 width=3/ qed-.
-
-fact ltpss_inv_atom2_aux: ∀d,e,L1,L2.
- L1 ▶* [d, e] L2 → L2 = ⋆ → L1 = ⋆.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ //
-| #L #I #V #H destruct
-| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
-]
-qed.
-
-lemma ltpss_inv_atom2: ∀d,e,L1. L1 ▶* [d, e] ⋆ → L1 = ⋆.
-/2 width=5/ qed-.
-
-fact ltpss_inv_tpss22_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e →
- ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 ▶* [0, e - 1] K2 &
- K2 ⊢ V1 ▶* [0, e - 1] V2 &
- L1 = K1. ⓑ{I} V1.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #e #_ #_ #K1 #I #V1 #H destruct
-| #L1 #I #V #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/
-| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma ltpss_inv_tpss22: ∀e,L1,K2,I,V2. L1 ▶* [0, e] K2. ⓑ{I} V2 → 0 < e →
- ∃∃K1,V1. K1 ▶* [0, e - 1] K2 &
- K2 ⊢ V1 ▶* [0, e - 1] V2 &
- L1 = K1. ⓑ{I} V1.
-/2 width=5/ qed-.
-
-fact ltpss_inv_tpss12_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d →
- ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 ▶* [d - 1, e] K2 &
- K2 ⊢ V1 ▶* [d - 1, e] V2 &
- L1 = K1. ⓑ{I} V1.
-#d #e #L1 #L2 * -d -e -L1 -L2
-[ #d #e #_ #I #K2 #V2 #H destruct
-| #L #I #V #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
-| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct /2 width=5/
-]
-qed.
-
-lemma ltpss_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ▶* [d, e] K2. ⓑ{I} V2 → 0 < d →
- ∃∃K1,V1. K1 ▶* [d - 1, e] K2 &
- K2 ⊢ V1 ▶* [d - 1, e] V2 &
- L1 = K1. ⓑ{I} V1.
-/2 width=3/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma ltpss_tps2: ∀L1,L2,I,V1,V2,e.
- L1 ▶* [0, e] L2 → L2 ⊢ V1 ▶ [0, e] V2 →
- L1. ⓑ{I} V1 ▶* [0, e + 1] L2. ⓑ{I} V2.
-/3 width=1/ qed.
-
-lemma ltpss_tps1: ∀L1,L2,I,V1,V2,d,e.
- L1 ▶* [d, e] L2 → L2 ⊢ V1 ▶ [d, e] V2 →
- L1. ⓑ{I} V1 ▶* [d + 1, e] L2. ⓑ{I} V2.
-/3 width=1/ qed.
-
-lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
- L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶* [0, e - 1] V2 →
- 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
->(plus_minus_m_m e 1) /2 width=1/
-qed.
-
-lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
- L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶* [d - 1, e] V2 →
- 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2.
-#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
->(plus_minus_m_m d 1) /2 width=1/
-qed.
-
-lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e.
- L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶ [0, e - 1] V2 →
- 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2.
-/3 width=1/ qed.
-
-lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
- L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶ [d - 1, e] V2 →
- 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2.
-/3 width=1/ qed.
-
-(* Basic_1: was by definition: csubst1_refl *)
-lemma ltpss_refl: ∀L,d,e. L ▶* [d, e] L.
-#L elim L -L //
-#L #I #V #IHL * /2 width=1/ * /2 width=1/
-qed.
-
-lemma ltpss_weak: ∀L1,L2,d1,e1. L1 ▶* [d1, e1] L2 →
- ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → L1 ▶* [d2, e2] L2.
-#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 //
-[ #L1 #L2 #I #V1 #V2 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd2 #Hde2
- lapply (le_n_O_to_eq … Hd2) #H destruct normalize in Hde2;
- lapply (lt_to_le_to_lt 0 … Hde2) // #He2
- lapply (le_plus_to_minus_r … Hde2) -Hde2 /3 width=5/
-| #L1 #L2 #I #V1 #V2 #d1 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd21 #Hde12
- >plus_plus_comm_23 in Hde12; #Hde12
- elim (le_to_or_lt_eq 0 d2 ?) // #H destruct
- [ lapply (le_plus_to_minus_r … Hde12) -Hde12 <plus_minus // #Hde12
- lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
- | -Hd21 normalize in Hde12;
- lapply (lt_to_le_to_lt 0 … Hde12) // #He2
- lapply (le_plus_to_minus_r … Hde12) -Hde12 /3 width=5/
- ]
-]
-qed.
-
-lemma ltpss_weak_all: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-// /3 width=2/ /3 width=3/
-qed.
-
-fact ltpss_append_le_aux: ∀K1,K2,d,x. K1 ▶* [d, x] K2 → x = |K1| - d →
- ∀L1,L2,e. L1 ▶* [0, e] L2 → d ≤ |K1| →
- L1 @@ K1 ▶* [d, x + e] L2 @@ K2.
-#K1 #K2 #d #x #H elim H -K1 -K2 -d -x
-[ #d #x #H1 #L1 #L2 #e #HL12 #H2 destruct
- lapply (le_n_O_to_eq … H2) -H2 #H destruct //
-| #K #I #V <minus_n_O normalize <plus_n_Sm #H destruct
-| #K1 #K2 #I #V1 #V2 #x #_ #HV12 <minus_n_O #IHK12 <minus_n_O #H #L1 #L2 #e #HL12 #_
- lapply (injective_plus_l … H) -H #H destruct >plus_plus_comm_23
- /4 width=5 by ltpss_tpss2, tpss_append, tpss_weak, monotonic_le_plus_r/ (**) (* too slow without trace *)
-| #K1 #K2 #I #V1 #V2 #d #x #_ #HV12 #IHK12 normalize <minus_le_minus_minus_comm // <minus_plus_m_m #H1 #L1 #L2 #e #HL12 #H2 destruct
- lapply (le_plus_to_le_r … H2) -H2 #Hd
- /4 width=5 by ltpss_tpss1, tpss_append, tpss_weak, monotonic_le_plus_r/ (**) (* too slow without trace *)
-]
-qed-.
-
-lemma ltpss_append_le: ∀K1,K2,d. K1 ▶* [d, |K1| - d] K2 →
- ∀L1,L2,e. L1 ▶* [0, e] L2 → d ≤ |K1| →
- L1 @@ K1 ▶* [d, |K1| - d + e] L2 @@ K2.
-/2 width=1 by ltpss_append_le_aux/ qed.
-
-lemma ltpss_append_ge: ∀K1,K2,d,e. K1 ▶* [d, e] K2 →
- ∀L1,L2. L1 ▶* [d - |K1|, e] L2 → |K1| ≤ d →
- L1 @@ K1 ▶* [d, e] L2 @@ K2.
-#K1 #K2 #d #e #H elim H -K1 -K2 -d -e
-[ #d #e #L1 #L2 <minus_n_O //
-| #K #I #V #L1 #L2 #_ #H
- lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
-| #K1 #K2 #I #V1 #V2 #e #_ #_ #_ #L1 #L2 #_ #H
- lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
-| #K1 #K2 #I #V1 #V2 #d #e #_ #HV12 #IHK12 #L1 #L2
- normalize <minus_le_minus_minus_comm // <minus_plus_m_m #HL12 #H
- lapply (le_plus_to_le_r … H) -H /3 width=1/
-]
-qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma ltpss_fwd_length: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → |L1| = |L2|.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
-normalize //
-qed-.
-(*
-lemma tps_fwd_shift1: ∀L1,L,T1,T,d,e. L ⊢ L1 @@ T1 ▶ [d, e] T →
- ∃∃L2,T2. L @@ L1 ▶* [d + |L1|, e] L @@ L2 & T = L2 @@ T2.
-#L1 @(lenv_ind_dx … L1) -L1
-[ #L #T1 #T #d #e #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
-| #I #L1 #V1 #IH #L #T1 #T #d #e >shift_append_assoc #H
- elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- elim (IH … HT12) -IH -T1 #L2 #T #HL12 #H destruct
- <append_assoc >append_length <associative_plus
- @(ex2_2_intro … (⋆.ⓑ{I}V2@@L2)) /2 width=4/ <append_assoc normalize
- lapply (ltpss_tps1 L … I … HV12) -HV12 // #HV12
- @ltpss_append_ge /2/
-(*
-
-
- /3 width=5/
-*)
-]
-qed-.
-*)
-
-(* Basic_1: removed theorems 28:
- csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
- csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
- csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back
- csubst0_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt
- csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_lt_back
- csubst0_snd_bind csubst0_fst_bind csubst0_both_bind
- csubst1_head csubst1_flat csubst1_gen_head
- csubst1_getl_ge csubst1_getl_lt csubst1_getl_ge_back getl_csubst1
- fsubst0_gen_base
-*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/tpss.ma".
+
+(* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+(* Basic_1: includes: csubst1_bind *)
+inductive ltpss_dx: nat → nat → relation lenv ≝
+| ltpss_dx_atom : ∀d,e. ltpss_dx d e (⋆) (⋆)
+| ltpss_dx_pair : ∀L,I,V. ltpss_dx 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
+| ltpss_dx_tpss2: ∀L1,L2,I,V1,V2,e.
+ ltpss_dx 0 e L1 L2 → L2 ⊢ V1 ▶* [0, e] V2 →
+ ltpss_dx 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
+| ltpss_dx_tpss1: ∀L1,L2,I,V1,V2,d,e.
+ ltpss_dx d e L1 L2 → L2 ⊢ V1 ▶* [d, e] V2 →
+ ltpss_dx (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
+.
+
+interpretation "parallel unfold (local environment, dx variant)"
+ 'PSubstStar L1 d e L2 = (ltpss_dx d e L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact ltpss_dx_inv_refl_O2_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → e = 0 → L1 = L2.
+#d #e #L1 #L2 #H elim H -d -e -L1 -L2 //
+[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct
+ >(IHL12 ?) -IHL12 // >(tpss_inv_refl_O2 … HV12) //
+]
+qed.
+
+lemma ltpss_dx_inv_refl_O2: ∀d,L1,L2. L1 ▶* [d, 0] L2 → L1 = L2.
+/2 width=4/ qed-.
+
+fact ltpss_dx_inv_atom1_aux: ∀d,e,L1,L2.
+ L1 ▶* [d, e] L2 → L1 = ⋆ → L2 = ⋆.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ //
+| #L #I #V #H destruct
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
+qed.
+
+lemma ltpss_dx_inv_atom1: ∀d,e,L2. ⋆ ▶* [d, e] L2 → L2 = ⋆.
+/2 width=5/ qed-.
+
+fact ltpss_dx_inv_tpss21_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e →
+ ∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. K1 ▶* [0, e - 1] K2 &
+ K2 ⊢ V1 ▶* [0, e - 1] V2 &
+ L2 = K2. ⓑ{I} V2.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #_ #K1 #I #V1 #H destruct
+| #L1 #I #V #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma ltpss_dx_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 ▶* [0, e] L2 → 0 < e →
+ ∃∃K2,V2. K1 ▶* [0, e - 1] K2 &
+ K2 ⊢ V1 ▶* [0, e - 1] V2 &
+ L2 = K2. ⓑ{I} V2.
+/2 width=5/ qed-.
+
+fact ltpss_dx_inv_tpss11_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d →
+ ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. K1 ▶* [d - 1, e] K2 &
+ K2 ⊢ V1 ▶* [d - 1, e] V2 &
+ L2 = K2. ⓑ{I} V2.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #I #K1 #V1 #H destruct
+| #L #I #V #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct /2 width=5/
+]
+qed.
+
+lemma ltpss_dx_inv_tpss11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 ▶* [d, e] L2 → 0 < d →
+ ∃∃K2,V2. K1 ▶* [d - 1, e] K2 &
+ K2 ⊢ V1 ▶* [d - 1, e] V2 &
+ L2 = K2. ⓑ{I} V2.
+/2 width=3/ qed-.
+
+fact ltpss_dx_inv_atom2_aux: ∀d,e,L1,L2.
+ L1 ▶* [d, e] L2 → L2 = ⋆ → L1 = ⋆.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ //
+| #L #I #V #H destruct
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
+qed.
+
+lemma ltpss_dx_inv_atom2: ∀d,e,L1. L1 ▶* [d, e] ⋆ → L1 = ⋆.
+/2 width=5/ qed-.
+
+fact ltpss_dx_inv_tpss22_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → d = 0 → 0 < e →
+ ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ▶* [0, e - 1] K2 &
+ K2 ⊢ V1 ▶* [0, e - 1] V2 &
+ L1 = K1. ⓑ{I} V1.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #_ #K1 #I #V1 #H destruct
+| #L1 #I #V #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma ltpss_dx_inv_tpss22: ∀e,L1,K2,I,V2. L1 ▶* [0, e] K2. ⓑ{I} V2 → 0 < e →
+ ∃∃K1,V1. K1 ▶* [0, e - 1] K2 &
+ K2 ⊢ V1 ▶* [0, e - 1] V2 &
+ L1 = K1. ⓑ{I} V1.
+/2 width=5/ qed-.
+
+fact ltpss_dx_inv_tpss12_aux: ∀d,e,L1,L2. L1 ▶* [d, e] L2 → 0 < d →
+ ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ▶* [d - 1, e] K2 &
+ K2 ⊢ V1 ▶* [d - 1, e] V2 &
+ L1 = K1. ⓑ{I} V1.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #I #K2 #V2 #H destruct
+| #L #I #V #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct /2 width=5/
+]
+qed.
+
+lemma ltpss_dx_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ▶* [d, e] K2. ⓑ{I} V2 → 0 < d →
+ ∃∃K1,V1. K1 ▶* [d - 1, e] K2 &
+ K2 ⊢ V1 ▶* [d - 1, e] V2 &
+ L1 = K1. ⓑ{I} V1.
+/2 width=3/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma ltpss_dx_tps2: ∀L1,L2,I,V1,V2,e.
+ L1 ▶* [0, e] L2 → L2 ⊢ V1 ▶ [0, e] V2 →
+ L1. ⓑ{I} V1 ▶* [0, e + 1] L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+lemma ltpss_dx_tps1: ∀L1,L2,I,V1,V2,d,e.
+ L1 ▶* [d, e] L2 → L2 ⊢ V1 ▶ [d, e] V2 →
+ L1. ⓑ{I} V1 ▶* [d + 1, e] L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+lemma ltpss_dx_tpss2_lt: ∀L1,L2,I,V1,V2,e.
+ L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶* [0, e - 1] V2 →
+ 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) /2 width=1/
+qed.
+
+lemma ltpss_dx_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
+ L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶* [d - 1, e] V2 →
+ 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) /2 width=1/
+qed.
+
+lemma ltpss_dx_tps2_lt: ∀L1,L2,I,V1,V2,e.
+ L1 ▶* [0, e - 1] L2 → L2 ⊢ V1 ▶ [0, e - 1] V2 →
+ 0 < e → L1. ⓑ{I} V1 ▶* [0, e] L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+lemma ltpss_dx_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
+ L1 ▶* [d - 1, e] L2 → L2 ⊢ V1 ▶ [d - 1, e] V2 →
+ 0 < d → L1. ⓑ{I} V1 ▶* [d, e] L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+(* Basic_1: was by definition: csubst1_refl *)
+lemma ltpss_dx_refl: ∀L,d,e. L ▶* [d, e] L.
+#L elim L -L //
+#L #I #V #IHL * /2 width=1/ * /2 width=1/
+qed.
+
+lemma ltpss_dx_weak: ∀L1,L2,d1,e1. L1 ▶* [d1, e1] L2 →
+ ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → L1 ▶* [d2, e2] L2.
+#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 //
+[ #L1 #L2 #I #V1 #V2 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd2 #Hde2
+ lapply (le_n_O_to_eq … Hd2) #H destruct normalize in Hde2;
+ lapply (lt_to_le_to_lt 0 … Hde2) // #He2
+ lapply (le_plus_to_minus_r … Hde2) -Hde2 /3 width=5/
+| #L1 #L2 #I #V1 #V2 #d1 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd21 #Hde12
+ >plus_plus_comm_23 in Hde12; #Hde12
+ elim (le_to_or_lt_eq 0 d2 ?) // #H destruct
+ [ lapply (le_plus_to_minus_r … Hde12) -Hde12 <plus_minus // #Hde12
+ lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
+ | -Hd21 normalize in Hde12;
+ lapply (lt_to_le_to_lt 0 … Hde12) // #He2
+ lapply (le_plus_to_minus_r … Hde12) -Hde12 /3 width=5/
+ ]
+]
+qed.
+
+lemma ltpss_dx_weak_all: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ▶* [0, |L2|] L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+// /3 width=2/ /3 width=3/
+qed.
+
+fact ltpss_dx_append_le_aux: ∀K1,K2,d,x. K1 ▶* [d, x] K2 → x = |K1| - d →
+ ∀L1,L2,e. L1 ▶* [0, e] L2 → d ≤ |K1| →
+ L1 @@ K1 ▶* [d, x + e] L2 @@ K2.
+#K1 #K2 #d #x #H elim H -K1 -K2 -d -x
+[ #d #x #H1 #L1 #L2 #e #HL12 #H2 destruct
+ lapply (le_n_O_to_eq … H2) -H2 #H destruct //
+| #K #I #V <minus_n_O normalize <plus_n_Sm #H destruct
+| #K1 #K2 #I #V1 #V2 #x #_ #HV12 <minus_n_O #IHK12 <minus_n_O #H #L1 #L2 #e #HL12 #_
+ lapply (injective_plus_l … H) -H #H destruct >plus_plus_comm_23
+ /4 width=5 by ltpss_dx_tpss2, tpss_append, tpss_weak, monotonic_le_plus_r/ (**) (* too slow without trace *)
+| #K1 #K2 #I #V1 #V2 #d #x #_ #HV12 #IHK12 normalize <minus_le_minus_minus_comm // <minus_plus_m_m #H1 #L1 #L2 #e #HL12 #H2 destruct
+ lapply (le_plus_to_le_r … H2) -H2 #Hd
+ /4 width=5 by ltpss_dx_tpss1, tpss_append, tpss_weak, monotonic_le_plus_r/ (**) (* too slow without trace *)
+]
+qed-.
+
+lemma ltpss_dx_append_le: ∀K1,K2,d. K1 ▶* [d, |K1| - d] K2 →
+ ∀L1,L2,e. L1 ▶* [0, e] L2 → d ≤ |K1| →
+ L1 @@ K1 ▶* [d, |K1| - d + e] L2 @@ K2.
+/2 width=1 by ltpss_dx_append_le_aux/ qed.
+
+lemma ltpss_dx_append_ge: ∀K1,K2,d,e. K1 ▶* [d, e] K2 →
+ ∀L1,L2. L1 ▶* [d - |K1|, e] L2 → |K1| ≤ d →
+ L1 @@ K1 ▶* [d, e] L2 @@ K2.
+#K1 #K2 #d #e #H elim H -K1 -K2 -d -e
+[ #d #e #L1 #L2 <minus_n_O //
+| #K #I #V #L1 #L2 #_ #H
+ lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
+| #K1 #K2 #I #V1 #V2 #e #_ #_ #_ #L1 #L2 #_ #H
+ lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
+| #K1 #K2 #I #V1 #V2 #d #e #_ #HV12 #IHK12 #L1 #L2
+ normalize <minus_le_minus_minus_comm // <minus_plus_m_m #HL12 #H
+ lapply (le_plus_to_le_r … H) -H /3 width=1/
+]
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltpss_dx_fwd_length: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → |L1| = |L2|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+normalize //
+qed-.
+
+(* Basic_1: removed theorems 28:
+ csubst0_clear_O csubst0_drop_lt csubst0_drop_gt csubst0_drop_eq
+ csubst0_clear_O_back csubst0_clear_S csubst0_clear_trans
+ csubst0_drop_gt_back csubst0_drop_eq_back csubst0_drop_lt_back
+ csubst0_gen_sort csubst0_gen_head csubst0_getl_ge csubst0_getl_lt
+ csubst0_gen_S_bind_2 csubst0_getl_ge_back csubst0_getl_lt_back
+ csubst0_snd_bind csubst0_fst_bind csubst0_both_bind
+ csubst1_head csubst1_flat csubst1_gen_head
+ csubst1_getl_ge csubst1_getl_lt csubst1_getl_ge_back getl_csubst1
+ fsubst0_gen_base
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/ltpss_dx.ma".
+
+(* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+lemma ltpss_dx_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
+| //
+| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
+ elim (le_inv_plus_l … He12) #_ #He2
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
+]
+qed.
+
+lemma ltpss_dx_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
+#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
+| //
+| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
+ elim (le_inv_plus_l … He12) #_ #He2
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
+| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
+]
+qed.
+
+lemma ltpss_dx_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L2 ▶* [0, d1 + e1 - e2] L & ⇩[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+ lapply (le_n_O_to_eq … He2) -He2 #H destruct
+ lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
+ lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+ [ -IHK01 -He21 destruct <minus_n_O /3 width=3/
+ | -HK01 -HV01 <minus_le_minus_minus_comm //
+ elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
+ ]
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
+ <minus_le_minus_minus_comm //
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
+]
+qed.
+
+lemma ltpss_dx_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+ lapply (le_n_O_to_eq … He2) -He2 #H destruct
+ lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
+ lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+ [ -IHK10 -He21 destruct <minus_n_O /3 width=3/
+ | -HK10 -HV10 <minus_le_minus_minus_comm //
+ elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
+ ]
+| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
+ <minus_le_minus_minus_comm //
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
+]
+qed.
+
+lemma ltpss_dx_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L2 ▶* [d1 - e2, e1] L & ⇩[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
+ lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
+ lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
+ lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+ [ -IHK01 -He2d1 destruct <minus_n_O /3 width=3/
+ | -HK01 -HV01 <minus_le_minus_minus_comm //
+ elim (IHK01 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
+ ]
+]
+qed.
+
+lemma ltpss_dx_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L ▶* [d1 - e2, e1] L2 & ⇩[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
+ lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
+ lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
+| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
+ lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+ [ -IHK10 -He2d1 destruct <minus_n_O /3 width=3/
+ | -HK10 -HV10 <minus_le_minus_minus_comm //
+ elim (IHK10 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
+ ]
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/tpss_tpss.ma".
+include "basic_2/unfold/tpss_alt.ma".
+include "basic_2/unfold/ltpss_dx_tpss.ma".
+
+(* DX PARTIAL UNFOLD ON LOCAL ENVIRONMENTS **********************************)
+
+(* Advanced properties ******************************************************)
+
+lemma ltpss_dx_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ▶* [d1, e1] L1 →
+ ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T &
+ L1 ⊢ U2 ▶* [d1, e1] T.
+#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 @(tpss_ind … H) -U2 /2 width=3/
+#U #U2 #_ #HU2 * #X2 #HTX2 #HUX2
+elim (ltpss_dx_tps_conf … HU2 … HL01) -L0 #X1 #HUX1 #HU2X1
+elim (tpss_strip_eq … HUX2 … HUX1) -U #X #HX2 #HX1
+lapply (tpss_trans_eq … HU2X1 … HX1) -X1 /3 width=3/
+qed.
+
+lemma ltpss_dx_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 →
+ L1 ▶* [d1, e1] L0 → L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & L0 ⊢ T ▶* [d1, e1] U2.
+#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2
+[ /2 width=3/
+| #U #U2 #_ #HU2 * #T #HT2 #HTU
+ elim (tpss_strap1_down … HTU … HU2 ?) -U // #U #HTU #HU2
+ elim (ltpss_dx_tps_trans … HTU … HL10) -HTU -HL10 #X #HTX #HXU
+ lapply (tpss_trans_eq … HXU HU2) -U /3 width=3/
+]
+qed.
+
+fact ltpss_dx_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
+ L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 →
+ Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
+#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
+#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
+[ //
+| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
+ lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
+ elim (ltpss_dx_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
+ elim (ltpss_dx_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
+ lapply (tpss_fwd_tw … HV01) #H2
+ lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H
+ lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02
+ lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01
+ [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ]
+| #L #a #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
+ lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
+ lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
+ lapply (tpss_lsubs_trans … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
+ lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
+]
+qed.
+
+lemma ltpss_dx_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
+ ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma ltpss_dx_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 →
+ L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+fact ltpss_dx_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 →
+ ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K →
+ ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
+#K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
+[ -IH /2 width=3/
+| -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
+ [ /2 width=3/
+ | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/
+ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
+ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
+ ]
+| #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
+ [ -IH #d2 #e2 #H1 #H2 destruct
+ | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
+ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ lapply (tpss_trans_eq … HVU1 HU1W) -U1
+ lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
+ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ lapply (tpss_trans_eq … HVU1 HU1W) -U1
+ lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
+ ]
+| #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
+ [ -IH #d2 #e2 #H1 #H2 destruct
+ | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
+ | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ lapply (tpss_trans_eq … HVU1 HU1W) -U1
+ lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
+ | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
+ elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
+ elim (ltpss_dx_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
+ elim (ltpss_dx_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
+ elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
+ lapply (tpss_trans_eq … HVU1 HU1W) -U1
+ lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
+ ]
+]
+qed.
+
+theorem ltpss_dx_conf: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
+ ∀L2,d2,e2. L0 ▶* [d2, e2] L2 →
+ ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
+/2 width=7/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/ltpss_dx_ldrop.ma".
+
+(* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+(* Properties concerning partial substitution on terms **********************)
+
+lemma ltpss_dx_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → d1 + e1 ≤ d2 →
+ L1 ⊢ T2 ▶ [d2, e2] U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ //
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
+ lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
+ lapply (ltpss_dx_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/
+| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
+ @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_dx_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
+| /3 width=4/
+]
+qed.
+
+lemma ltpss_dx_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
+ L1 ⊢ T2 ▶ [d2, e2] U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ //
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
+ lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
+ lapply (ltpss_dx_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/
+| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
+ @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_dx_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
+| /3 width=4/
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/tpss_lift.ma".
+include "basic_2/unfold/ltpss_dx_tps.ma".
+
+(* DX PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+(* Properties concerning partial unfold on terms ****************************)
+
+lemma ltpss_dx_tpss_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → d1 + e1 ≤ d2 →
+ L1 ⊢ T2 ▶* [d2, e2] U2.
+#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU
+lapply (ltpss_dx_tps_conf_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
+qed.
+
+(* Basic_1: was: subst1_subst1_back *)
+lemma ltpss_dx_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ▶* [d1, e1] L1 →
+ ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T &
+ L1 ⊢ U2 ▶* [d1, e1] T.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ /2 width=3/
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
+ elim (lt_or_ge i2 d1) #Hi2d1
+ [ elim (ltpss_dx_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=2/ #X #H #HLK1
+ elim (ltpss_dx_inv_tpss11 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK1) #H
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tpss_lift_ge … HV01 … H HVW0 … HVW1) -V0 -H // >minus_plus <plus_minus_m_m // /3 width=4/
+ | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
+ [ elim (ltpss_dx_ldrop_conf_be … HL01 … HLK0 ? ?) -L0 // /2 width=2/ #X #H #HLK1
+ elim (ltpss_dx_inv_tpss21 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK1) #H
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tpss_lift_ge … HV01 … H HVW0 … HVW1) -V0 -H // normalize #HW01
+ lapply (tpss_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
+ | lapply (ltpss_dx_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/
+ ]
+ ]
+| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
+ elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
+ elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
+ elim (IHVW2 … HL01) -IHVW2
+ elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
+]
+qed.
+
+lemma ltpss_dx_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
+ L1 ⊢ T2 ▶* [d2, e2] U2.
+#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU
+lapply (ltpss_dx_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
+qed.
+
+(* Basic_1: was: subst1_subst1 *)
+lemma ltpss_dx_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀L1,d1,e1. L1 ▶* [d1, e1] L0 →
+ ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T &
+ L0 ⊢ T ▶* [d1, e1] U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ /2 width=3/
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
+ elim (lt_or_ge i2 d1) #Hi2d1
+ [ elim (ltpss_dx_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1
+ elim (ltpss_dx_inv_tpss12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // >minus_plus <plus_minus_m_m /2 width=1/ /3 width=4/
+ | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
+ [ elim (ltpss_dx_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 // /2 width=2/ #X #H #HLK1
+ elim (ltpss_dx_inv_tpss22 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // normalize #HW01
+ lapply (tpss_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
+ | lapply (ltpss_dx_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/
+ ]
+ ]
+| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
+ elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
+ elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
+ elim (IHVW2 … HL10) -IHVW2
+ elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/
+]
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/ltpss.ma".
-
-(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
-
-lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
- d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
-| //
-| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
- elim (le_inv_plus_l … He12) #_ #He2
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
- lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
-| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
- elim (le_inv_plus_l … Hd1e2) #_ #He2
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
- lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
-]
-qed.
-
-lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
- d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
-#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
-| //
-| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
- elim (le_inv_plus_l … He12) #_ #He2
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
- lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
-| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
- elim (le_inv_plus_l … Hd1e2) #_ #He2
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
- lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
-]
-qed.
-
-lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L2 ▶* [0, d1 + e1 - e2] L & ⇩[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
-| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
- lapply (le_n_O_to_eq … He2) -He2 #H destruct
- lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
-| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
- lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
- [ -IHK01 -He21 destruct <minus_n_O /3 width=3/
- | -HK01 -HV01 <minus_le_minus_minus_comm //
- elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
- ]
-| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
- elim (le_inv_plus_l … Hd1e2) #_ #He2
- <minus_le_minus_minus_comm //
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
- elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
-]
-qed.
-
-lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
- ∃∃L. L ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
-| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
- lapply (le_n_O_to_eq … He2) -He2 #H destruct
- lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
-| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
- lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
- [ -IHK10 -He21 destruct <minus_n_O /3 width=3/
- | -HK10 -HV10 <minus_le_minus_minus_comm //
- elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
- ]
-| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
- elim (le_inv_plus_l … Hd1e2) #_ #He2
- <minus_le_minus_minus_comm //
- lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
- elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
-]
-qed.
-
-lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L2 ▶* [d1 - e2, e1] L & ⇩[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
-| /2 width=3/
-| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
- lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
- lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
-| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
- lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
- [ -IHK01 -He2d1 destruct <minus_n_O /3 width=3/
- | -HK01 -HV01 <minus_le_minus_minus_comm //
- elim (IHK01 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
- ]
-]
-qed.
-
-lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ▶* [d1, e1] L0 →
- ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
- ∃∃L. L ▶* [d1 - e2, e1] L2 & ⇩[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
-[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
-| /2 width=3/
-| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
- lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
- lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
-| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
- lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
- [ -IHK10 -He2d1 destruct <minus_n_O /3 width=3/
- | -HK10 -HV10 <minus_le_minus_minus_comm //
- elim (IHK10 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
- ]
-]
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/tpss_tpss.ma".
-include "basic_2/unfold/tpss_alt.ma".
-include "basic_2/unfold/ltpss_tpss.ma".
-
-(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
-
-(* Advanced properties ******************************************************)
-
-lemma ltpss_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
- ∀L1,d1,e1. L0 ▶* [d1, e1] L1 →
- ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T &
- L1 ⊢ U2 ▶* [d1, e1] T.
-#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 @(tpss_ind … H) -U2 /2 width=3/
-#U #U2 #_ #HU2 * #X2 #HTX2 #HUX2
-elim (ltpss_tps_conf … HU2 … HL01) -L0 #X1 #HUX1 #HU2X1
-elim (tpss_strip_eq … HUX2 … HUX1) -U #X #HX2 #HX1
-lapply (tpss_trans_eq … HU2X1 … HX1) -X1 /3 width=3/
-qed.
-
-lemma ltpss_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 →
- L1 ▶* [d1, e1] L0 → L0 ⊢ T2 ▶* [d2, e2] U2 →
- ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & L0 ⊢ T ▶* [d1, e1] U2.
-#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #HL10 #H @(tpss_ind … H) -U2
-[ /2 width=3/
-| #U #U2 #_ #HU2 * #T #HT2 #HTU
- elim (tpss_strap1_down … HTU … HU2 ?) -U // #U #HTU #HU2
- elim (ltpss_tps_trans … HTU … HL10) -HTU -HL10 #X #HTX #HXU
- lapply (tpss_trans_eq … HXU HU2) -U /3 width=3/
-]
-qed.
-
-fact ltpss_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
- L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ▶* [d, e] L1 →
- Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
-#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
-#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
-[ //
-| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
- lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
- elim (ltpss_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
- elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
- lapply (tpss_fwd_tw … HV01) #H2
- lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H
- lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02
- lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01
- [1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ]
-| #L #a #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
- lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
- lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
- lapply (tpss_lsubs_trans … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
-| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
- lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
- lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
-]
-qed.
-
-lemma ltpss_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
- ∀L0. L0 ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
-/2 width=5/ qed.
-
-lemma ltpss_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ▶* [d, e] L1 →
- L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2.
-/3 width=3/ qed.
-
-(* Main properties **********************************************************)
-
-fact ltpss_conf_aux: ∀K,K1,L1,d1,e1. K1 ▶* [d1, e1] L1 →
- ∀K2,L2,d2,e2. K2 ▶* [d2, e2] L2 → K1 = K → K2 = K →
- ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
-#K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
-[ -IH /2 width=3/
-| -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
- [ /2 width=3/
- | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/
- | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
- | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /3 width=3/
- ]
-| #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
- [ -IH #d2 #e2 #H1 #H2 destruct
- | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
- | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
- elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
- elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
- elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
- lapply (tpss_trans_eq … HVU1 HU1W) -U1
- lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
- | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
- elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
- elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
- elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
- lapply (tpss_trans_eq … HVU1 HU1W) -U1
- lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
- ]
-| #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
- [ -IH #d2 #e2 #H1 #H2 destruct
- | -IH #K2 #I2 #V2 #H1 #H2 destruct /3 width=5/
- | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
- elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
- elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
- elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
- lapply (tpss_trans_eq … HVU1 HU1W) -U1
- lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
- | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
- elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
- elim (ltpss_tpss_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
- elim (ltpss_tpss_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
- elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
- lapply (tpss_trans_eq … HVU1 HU1W) -U1
- lapply (tpss_trans_eq … HVU2 HU2W) -U2 /3 width=5/
- ]
-]
-qed.
-
-lemma ltpss_conf: ∀L0,L1,d1,e1. L0 ▶* [d1, e1] L1 →
- ∀L2,d2,e2. L0 ▶* [d2, e2] L2 →
- ∃∃L. L1 ▶* [d2, e2] L & L2 ▶* [d1, e1] L.
-/2 width=7/ qed.
-
-theorem ltpss_trans_eq: ∀L1,L,d,e. L1 ▶* [d, e] L →
- ∀L2. L ▶* [d, e] L2 → L1 ▶* [d, e] L2.
-#L1 #L #d #e #H elim H -L1 -L -d -e //
-[ #L1 #L #I #V1 #V #e #_ #HV1 #IHL1 #X #H
- elim (ltpss_inv_tpss21 … H ?) -H // <minus_plus_m_m #L2 #V2 #HL2 #HV2 #H destruct
- elim (ltpss_tpss_conf … HV1 … HL2) -HV1 #V0 #HV10 #HV0
- elim (tpss_conf_eq … HV2 … HV0) -V #V #HV2 #HV0
- lapply (tpss_trans_eq … HV10 … HV0) -V0 #HV1
- @ltpss_tpss2 /2 width=1/
-
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/tpss.ma".
+
+(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+inductive ltpss_sn: nat → nat → relation lenv ≝
+| ltpss_sn_atom : ∀d,e. ltpss_sn d e (⋆) (⋆)
+| ltpss_sn_pair : ∀L,I,V. ltpss_sn 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
+| ltpss_sn_tpss2: ∀L1,L2,I,V1,V2,e.
+ ltpss_sn 0 e L1 L2 → L1 ⊢ V1 ▶* [0, e] V2 →
+ ltpss_sn 0 (e + 1) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
+| ltpss_sn_tpss1: ∀L1,L2,I,V1,V2,d,e.
+ ltpss_sn d e L1 L2 → L1 ⊢ V1 ▶* [d, e] V2 →
+ ltpss_sn (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
+.
+
+interpretation "parallel unfold (local environment, sn variant)"
+ 'PSubstStarSn L1 d e L2 = (ltpss_sn d e L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact ltpss_sn_inv_refl_O2_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → e = 0 → L1 = L2.
+#d #e #L1 #L2 #H elim H -d -e -L1 -L2 //
+[ #L1 #L2 #I #V1 #V2 #e #_ #_ #_ >commutative_plus normalize #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #HV12 #IHL12 #He destruct
+ >(IHL12 ?) -IHL12 // >(tpss_inv_refl_O2 … HV12) //
+]
+qed.
+
+lemma ltpss_sn_inv_refl_O2: ∀d,L1,L2. L1 ⊢ ▶* [d, 0] L2 → L1 = L2.
+/2 width=4/ qed-.
+
+fact ltpss_sn_inv_atom1_aux: ∀d,e,L1,L2.
+ L1 ⊢ ▶* [d, e] L2 → L1 = ⋆ → L2 = ⋆.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ //
+| #L #I #V #H destruct
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
+qed.
+
+lemma ltpss_sn_inv_atom1: ∀d,e,L2. ⋆ ⊢ ▶* [d, e] L2 → L2 = ⋆.
+/2 width=5/ qed-.
+
+fact ltpss_sn_inv_tpss21_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → d = 0 → 0 < e →
+ ∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. K1 ⊢ ▶* [0, e - 1] K2 &
+ K1 ⊢ V1 ▶* [0, e - 1] V2 &
+ L2 = K2. ⓑ{I} V2.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #_ #K1 #I #V1 #H destruct
+| #L1 #I #V #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K1 #J #W1 #H destruct /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma ltpss_sn_inv_tpss21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* [0, e] L2 → 0 < e →
+ ∃∃K2,V2. K1 ⊢ ▶* [0, e - 1] K2 &
+ K1 ⊢ V1 ▶* [0, e - 1] V2 &
+ L2 = K2. ⓑ{I} V2.
+/2 width=5/ qed-.
+
+fact ltpss_sn_inv_tpss11_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → 0 < d →
+ ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
+ ∃∃K2,V2. K1 ⊢ ▶* [d - 1, e] K2 &
+ K1 ⊢ V1 ▶* [d - 1, e] V2 &
+ L2 = K2. ⓑ{I} V2.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #I #K1 #V1 #H destruct
+| #L #I #V #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K1 #W1 #H destruct /2 width=5/
+]
+qed.
+
+lemma ltpss_sn_inv_tpss11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 ⊢ ▶* [d, e] L2 → 0 < d →
+ ∃∃K2,V2. K1 ⊢ ▶* [d - 1, e] K2 &
+ K1 ⊢ V1 ▶* [d - 1, e] V2 &
+ L2 = K2. ⓑ{I} V2.
+/2 width=3/ qed-.
+
+fact ltpss_sn_inv_atom2_aux: ∀d,e,L1,L2.
+ L1 ⊢ ▶* [d, e] L2 → L2 = ⋆ → L1 = ⋆.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ //
+| #L #I #V #H destruct
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
+qed.
+
+lemma ltpss_sn_inv_atom2: ∀d,e,L1. L1 ⊢ ▶* [d, e] ⋆ → L1 = ⋆.
+/2 width=5/ qed-.
+
+fact ltpss_sn_inv_tpss22_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → d = 0 → 0 < e →
+ ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ⊢ ▶* [0, e - 1] K2 &
+ K1 ⊢ V1 ▶* [0, e - 1] V2 &
+ L1 = K1. ⓑ{I} V1.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #_ #K1 #I #V1 #H destruct
+| #L1 #I #V #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ >commutative_plus normalize #H destruct
+]
+qed.
+
+lemma ltpss_sn_inv_tpss22: ∀e,L1,K2,I,V2. L1 ⊢ ▶* [0, e] K2. ⓑ{I} V2 → 0 < e →
+ ∃∃K1,V1. K1 ⊢ ▶* [0, e - 1] K2 &
+ K1 ⊢ V1 ▶* [0, e - 1] V2 &
+ L1 = K1. ⓑ{I} V1.
+/2 width=5/ qed-.
+
+fact ltpss_sn_inv_tpss12_aux: ∀d,e,L1,L2. L1 ⊢ ▶* [d, e] L2 → 0 < d →
+ ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ⊢ ▶* [d - 1, e] K2 &
+ K1 ⊢ V1 ▶* [d - 1, e] V2 &
+ L1 = K1. ⓑ{I} V1.
+#d #e #L1 #L2 * -d -e -L1 -L2
+[ #d #e #_ #I #K2 #V2 #H destruct
+| #L #I #V #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct /2 width=5/
+]
+qed.
+
+lemma ltpss_sn_inv_tpss12: ∀L1,K2,I,V2,d,e. L1 ⊢ ▶* [d, e] K2. ⓑ{I} V2 → 0 < d →
+ ∃∃K1,V1. K1 ⊢ ▶* [d - 1, e] K2 &
+ K1 ⊢ V1 ▶* [d - 1, e] V2 &
+ L1 = K1. ⓑ{I} V1.
+/2 width=3/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma ltpss_sn_tps2: ∀L1,L2,I,V1,V2,e.
+ L1 ⊢ ▶* [0, e] L2 → L1 ⊢ V1 ▶ [0, e] V2 →
+ L1. ⓑ{I} V1 ⊢ ▶* [0, e + 1] L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+lemma ltpss_sn_tps1: ∀L1,L2,I,V1,V2,d,e.
+ L1 ⊢ ▶* [d, e] L2 → L1 ⊢ V1 ▶ [d, e] V2 →
+ L1. ⓑ{I} V1 ⊢ ▶* [d + 1, e] L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+lemma ltpss_sn_tpss2_lt: ∀L1,L2,I,V1,V2,e.
+ L1 ⊢ ▶* [0, e - 1] L2 → L1 ⊢ V1 ▶* [0, e - 1] V2 →
+ 0 < e → L1. ⓑ{I} V1 ⊢ ▶* [0, e] L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) /2 width=1/
+qed.
+
+lemma ltpss_sn_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
+ L1 ⊢ ▶* [d - 1, e] L2 → L1 ⊢ V1 ▶* [d - 1, e] V2 →
+ 0 < d → L1. ⓑ{I} V1 ⊢ ▶* [d, e] L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) /2 width=1/
+qed.
+
+lemma ltpss_sn_tps2_lt: ∀L1,L2,I,V1,V2,e.
+ L1 ⊢ ▶* [0, e - 1] L2 → L1 ⊢ V1 ▶ [0, e - 1] V2 →
+ 0 < e → L1. ⓑ{I} V1 ⊢ ▶* [0, e] L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+lemma ltpss_sn_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
+ L1 ⊢ ▶* [d - 1, e] L2 → L1 ⊢ V1 ▶ [d - 1, e] V2 →
+ 0 < d → L1. ⓑ{I} V1 ⊢ ▶* [d, e] L2. ⓑ{I} V2.
+/3 width=1/ qed.
+
+lemma ltpss_sn_refl: ∀L,d,e. L ⊢ ▶* [d, e] L.
+#L elim L -L //
+#L #I #V #IHL * /2 width=1/ * /2 width=1/
+qed.
+
+lemma ltpss_sn_weak: ∀L1,L2,d1,e1. L1 ⊢ ▶* [d1, e1] L2 →
+ ∀d2,e2. d2 ≤ d1 → d1 + e1 ≤ d2 + e2 → L1 ⊢ ▶* [d2, e2] L2.
+#L1 #L2 #d1 #e1 #H elim H -L1 -L2 -d1 -e1 //
+[ #L1 #L2 #I #V1 #V2 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd2 #Hde2
+ lapply (le_n_O_to_eq … Hd2) #H destruct normalize in Hde2;
+ lapply (lt_to_le_to_lt 0 … Hde2) // #He2
+ lapply (le_plus_to_minus_r … Hde2) -Hde2 /3 width=5/
+| #L1 #L2 #I #V1 #V2 #d1 #e1 #_ #HV12 #IHL12 #d2 #e2 #Hd21 #Hde12
+ >plus_plus_comm_23 in Hde12; #Hde12
+ elim (le_to_or_lt_eq 0 d2 ?) // #H destruct
+ [ lapply (le_plus_to_minus_r … Hde12) -Hde12 <plus_minus // #Hde12
+ lapply (le_plus_to_minus … Hd21) -Hd21 #Hd21 /3 width=5/
+ | -Hd21 normalize in Hde12;
+ lapply (lt_to_le_to_lt 0 … Hde12) // #He2
+ lapply (le_plus_to_minus_r … Hde12) -Hde12 /3 width=5/
+ ]
+]
+qed.
+
+lemma ltpss_sn_weak_all: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ▶* [0, |L1|] L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+// /3 width=2/ /3 width=3/
+qed.
+
+fact ltpss_sn_append_le_aux: ∀K1,K2,d,x. K1 ⊢ ▶* [d, x] K2 → x = |K1| - d →
+ ∀L1,L2,e. L1 ⊢ ▶* [0, e] L2 → d ≤ |K1| →
+ L1 @@ K1 ⊢ ▶* [d, x + e] L2 @@ K2.
+#K1 #K2 #d #x #H elim H -K1 -K2 -d -x
+[ #d #x #H1 #L1 #L2 #e #HL12 #H2 destruct
+ lapply (le_n_O_to_eq … H2) -H2 #H destruct //
+| #K #I #V <minus_n_O normalize <plus_n_Sm #H destruct
+| #K1 #K2 #I #V1 #V2 #x #_ #HV12 <minus_n_O #IHK12 <minus_n_O #H #L1 #L2 #e #HL12 #_
+ lapply (injective_plus_l … H) -H #H destruct >plus_plus_comm_23
+ /4 width=5 by ltpss_sn_tpss2, tpss_append, tpss_weak, monotonic_le_plus_r/ (**) (* too slow without trace *)
+| #K1 #K2 #I #V1 #V2 #d #x #_ #HV12 #IHK12 normalize <minus_le_minus_minus_comm // <minus_plus_m_m #H1 #L1 #L2 #e #HL12 #H2 destruct
+ lapply (le_plus_to_le_r … H2) -H2 #Hd
+ /4 width=5 by ltpss_sn_tpss1, tpss_append, tpss_weak, monotonic_le_plus_r/ (**) (* too slow without trace *)
+]
+qed-.
+
+lemma ltpss_sn_append_le: ∀K1,K2,d. K1 ⊢ ▶* [d, |K1| - d] K2 →
+ ∀L1,L2,e. L1 ⊢ ▶* [0, e] L2 → d ≤ |K1| →
+ L1 @@ K1 ⊢ ▶* [d, |K1| - d + e] L2 @@ K2.
+/2 width=1 by ltpss_sn_append_le_aux/ qed.
+
+lemma ltpss_sn_append_ge: ∀K1,K2,d,e. K1 ⊢ ▶* [d, e] K2 →
+ ∀L1,L2. L1 ⊢ ▶* [d - |K1|, e] L2 → |K1| ≤ d →
+ L1 @@ K1 ⊢ ▶* [d, e] L2 @@ K2.
+#K1 #K2 #d #e #H elim H -K1 -K2 -d -e
+[ #d #e #L1 #L2 <minus_n_O //
+| #K #I #V #L1 #L2 #_ #H
+ lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
+| #K1 #K2 #I #V1 #V2 #e #_ #_ #_ #L1 #L2 #_ #H
+ lapply (le_n_O_to_eq … H) -H normalize <plus_n_Sm #H destruct
+| #K1 #K2 #I #V1 #V2 #d #e #_ #HV12 #IHK12 #L1 #L2
+ normalize <minus_le_minus_minus_comm // <minus_plus_m_m #HL12 #H
+ lapply (le_plus_to_le_r … H) -H /3 width=1/
+]
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltpss_sn_fwd_length: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → |L1| = |L2|.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
+normalize //
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/ltpss_dx_ltpss_dx.ma".
+include "basic_2/unfold/ltpss_sn_ltpss_sn.ma".
+
+(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+(* alternative definition of ltpss_sn *)
+definition ltpssa: nat → nat → relation lenv ≝
+ λd,e. TC … (ltpss_dx d e).
+
+interpretation "parallel unfold (local environment, sn variant) alternative"
+ 'PSubstStarSnAlt L1 d e L2 = (ltpssa d e L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma ltpssa_ind: ∀d,e,L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. L1 ⊢ ▶▶* [d, e] L → L ▶* [d, e] L2 → R L → R L2) →
+ ∀L2. L1 ⊢ ▶▶* [d, e] L2 → R L2.
+#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma ltpssa_ind_dx: ∀d,e,L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. L1 ▶* [d, e] L → L ⊢ ▶▶* [d, e] L2 → R L → R L1) →
+ ∀L1. L1 ⊢ ▶▶* [d, e] L2 → R L1.
+#d #e #L2 #R #HL2 #IHL2 #L1 #HL12 @(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma ltpssa_refl: ∀L,d,e. L ⊢ ▶▶* [d, e] L.
+/2 width=1/ qed.
+
+lemma ltpssa_tpss2: ∀I,L1,V1,V2,e. L1 ⊢ V1 ▶*[0, e] V2 →
+ ∀L2. L1 ⊢ ▶▶* [0, e] L2 →
+ L1.ⓑ{I}V1 ⊢ ▶▶* [O, e + 1] L2.ⓑ{I}V2.
+#I #L1 #V1 #V2 #e #HV12 #L2 #H @(ltpssa_ind … H) -L2
+[ /3 width=1/ | /3 width=5/ ]
+qed.
+
+lemma ltpssa_tpss1: ∀I,L1,V1,V2,d,e. L1 ⊢ V1 ▶*[d, e] V2 →
+ ∀L2. L1 ⊢ ▶▶* [d, e] L2 →
+ L1.ⓑ{I}V1 ⊢ ▶▶* [d + 1, e] L2.ⓑ{I}V2.
+#I #L1 #V1 #V2 #d #e #HV12 #L2 #H @(ltpssa_ind … H) -L2
+[ /3 width=1/ | /3 width=5/ ]
+qed.
+
+lemma ltpss_sn_ltpssa: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ▶▶* [d, e] L2.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // /2 width=1/
+qed.
+
+lemma ltpss_sn_dx_trans_eq: ∀L1,L,d,e. L1 ⊢ ▶* [d, e] L →
+ ∀L2. L ▶* [d, e] L2 → L1 ⊢ ▶* [d, e] L2.
+#L1 #L #d #e #H elim H -L1 -L -d -e
+[ #d #e #X #H
+ lapply (ltpss_dx_inv_atom1 … H) -H #H destruct //
+| #L #I #V #X #H
+ lapply (ltpss_dx_inv_refl_O2 … H) -H #H destruct //
+| #L1 #L #I #V1 #V #e #_ #HV1 #IHL1 #X #H
+ elim (ltpss_dx_inv_tpss21 … H ?) -H // <minus_plus_m_m
+ #L2 #V2 #HL2 #HV2 #H destruct
+ lapply (IHL1 … HL2) -L #HL12
+ lapply (ltpss_sn_tpss_trans_eq … HV2 … HL12) -HV2 #HV2
+ lapply (tpss_trans_eq … HV1 HV2) -V /2 width=1/
+| #L1 #L #I #V1 #V #d #e #_ #HV1 #IHL1 #X #H
+ elim (ltpss_dx_inv_tpss11 … H ?) -H // <minus_plus_m_m
+ #L2 #V2 #HL2 #HV2 #H destruct
+ lapply (IHL1 … HL2) -L #HL12
+ lapply (ltpss_sn_tpss_trans_eq … HV2 … HL12) -HV2 #HV2
+ lapply (tpss_trans_eq … HV1 HV2) -V /2 width=1/
+]
+qed.
+
+lemma ltpss_dx_sn_trans_eq: ∀L1,L,d,e. L1 ▶* [d, e] L →
+ ∀L2. L ⊢ ▶* [d, e] L2 → L1 ⊢ ▶* [d, e] L2.
+/3 width=3/ qed.
+
+lemma ltpssa_strip: ∀L0,L1,d1,e1. L0 ⊢ ▶▶* [d1, e1] L1 →
+ ∀L2,d2,e2. L0 ▶* [d2, e2] L2 →
+ ∃∃L. L1 ▶* [d2, e2] L & L2 ⊢ ▶▶* [d1, e1] L.
+/3 width=3/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltpssa_ltpss_sn: ∀L1,L2,d,e. L1 ⊢ ▶▶* [d, e] L2 → L1 ⊢ ▶* [d, e] L2.
+#L1 #L2 #d #e #H @(ltpssa_ind … H) -L2 // /2 width=3/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma ltpss_sn_strip: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
+ ∀L2,d2,e2. L0 ▶* [d2, e2] L2 →
+ ∃∃L. L1 ▶* [d2, e2] L & L2 ⊢ ▶* [d1, e1] L.
+#L0 #L1 #d1 #e1 #H #L2 #d2 #e2 #HL02
+lapply (ltpss_sn_ltpssa … H) -H #HL01
+elim (ltpssa_strip … HL01 … HL02) -L0
+/3 width=3 by ltpssa_ltpss_sn, ex2_1_intro/
+qed.
+
+(* Note: this should go in ltpss_sn_ltpss_sn.ma *)
+lemma ltpss_sn_tpss_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
+ ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T &
+ L0 ⊢ U2 ▶* [d1, e1] T.
+#L0 #T2 #U2 #d2 #e2 #HTU2 #L1 #d1 #e1 #H
+lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L1 /2 width=3/ -HTU2
+#L #L1 #H #HL1 * #T #HT2 #HU2T
+lapply (ltpssa_ltpss_sn … H) -H #HL0
+lapply (ltpss_sn_dx_trans_eq … HL0 … HL1) -HL0 #HL01
+elim (ltpss_dx_tpss_conf … HT2 … HL1) -HT2 -HL1 #T0 #HT20 #HT0
+lapply (ltpss_sn_tpss_trans_eq … HT0 … HL01) -HT0 -HL01 #HT0
+lapply (tpss_trans_eq … HU2T HT0) -T /2 width=3/
+qed.
+
+(* Note: this should go in ltpss_sn_ltpss_sn.ma *)
+lemma ltpss_sn_tpss_trans_down: ∀L0,L1,T2,U2,d1,e1,d2,e2. d2 + e2 ≤ d1 →
+ L1 ⊢ ▶* [d1, e1] L0 → L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∃∃T. L1 ⊢ T2 ▶* [d2, e2] T & L1 ⊢ T ▶* [d1, e1] U2.
+#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde2d1 #H #HTU2
+lapply (ltpss_sn_ltpssa … H) -H #HL10
+@(ltpssa_ind_dx … HL10) -L1 /2 width=3/ -HTU2
+#L1 #L #HL1 #_ * #T #HT2 #HTU2
+elim (ltpss_dx_tpss_trans_down … HL1 HT2) -HT2 // #T0 #HT20 #HT0 -Hde2d1
+lapply (tpss_trans_eq … HT0 HTU2) -T #HT0U2
+lapply (ltpss_dx_tpss_trans_eq … HT0U2 … HL1) -HT0U2 -HL1 /2 width=3/
+qed.
+
+(* Main properties **********************************************************)
+
+theorem ltpssa_conf: ∀L0,L1,d1,e1. L0 ⊢ ▶▶* [d1, e1] L1 →
+ ∀L2,d2,e2. L0 ⊢ ▶▶* [d2, e2] L2 →
+ ∃∃L. L1 ⊢ ▶▶* [d2, e2] L & L2 ⊢ ▶▶* [d1, e1] L.
+/3 width=3/ qed.
+
+(* Note: this should go in ltpss_sn_ltpss_sn.ma *)
+theorem ltpss_sn_conf: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
+ ∀L2,d2,e2. L0 ⊢ ▶* [d2, e2] L2 →
+ ∃∃L. L1 ⊢ ▶* [d2, e2] L & L2 ⊢ ▶* [d1, e1] L.
+#L0 #L1 #d1 #e1 #H1 #L2 #d2 #e2 #H2
+lapply (ltpss_sn_ltpssa … H1) -H1 #HL01
+lapply (ltpss_sn_ltpssa … H2) -H2 #HL02
+elim (ltpssa_conf … HL01 … HL02) -L0
+/3 width=3 by ltpssa_ltpss_sn, ex2_1_intro/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/ltpss_sn.ma".
+
+(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+lemma ltpss_sn_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
+| //
+| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
+ elim (le_inv_plus_l … He12) #_ #He2
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
+]
+qed.
+
+lemma ltpss_sn_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+ d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
+#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
+| //
+| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
+ elim (le_inv_plus_l … He12) #_ #He2
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
+| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
+]
+qed.
+
+lemma ltpss_sn_ldrop_conf_be: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L2 ⊢ ▶* [0, d1 + e1 - e2] L & ⇩[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+ lapply (le_n_O_to_eq … He2) -He2 #H destruct
+ lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
+ lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+ [ -IHK01 -He21 destruct <minus_n_O /3 width=3/
+ | -HK01 -HV01 <minus_le_minus_minus_comm //
+ elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
+ ]
+| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
+ <minus_le_minus_minus_comm //
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
+]
+qed.
+
+lemma ltpss_sn_ldrop_trans_be: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+ ∃∃L. L ⊢ ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
+ lapply (le_n_O_to_eq … He2) -He2 #H destruct
+ lapply (ldrop_inv_refl … HL2) -HL2 #H destruct /2 width=3/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
+ lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+ [ -IHK10 -He21 destruct <minus_n_O /3 width=3/
+ | -HK10 -HV10 <minus_le_minus_minus_comm //
+ elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
+ ]
+| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
+ elim (le_inv_plus_l … Hd1e2) #_ #He2
+ <minus_le_minus_minus_comm //
+ lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
+ elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
+]
+qed.
+
+lemma ltpss_sn_ldrop_conf_le: ∀L0,L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L2 ⊢ ▶* [d1 - e2, e1] L & ⇩[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
+ lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
+ lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
+| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
+ lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+ [ -IHK01 -He2d1 destruct <minus_n_O /3 width=3/
+ | -HK01 -HV01 <minus_le_minus_minus_comm //
+ elim (IHK01 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
+ ]
+]
+qed.
+
+lemma ltpss_sn_ldrop_trans_le: ∀L1,L0,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
+ ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+ ∃∃L. L ⊢ ▶* [d1 - e2, e1] L2 & ⇩[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
+[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
+| /2 width=3/
+| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
+ lapply (le_n_O_to_eq … He2) -He2 #He2 destruct
+ lapply (ldrop_inv_refl … H) -H #H destruct /3 width=3/
+| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
+ lapply (ldrop_inv_O1 … H) -H * * #He2 #HK0L2
+ [ -IHK10 -He2d1 destruct <minus_n_O /3 width=3/
+ | -HK10 -HV10 <minus_le_minus_minus_comm //
+ elim (IHK10 … HK0L2 ?) -K0 /2 width=1/ /3 width=3/
+ ]
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/tpss_tpss.ma".
+include "basic_2/unfold/tpss_alt.ma".
+include "basic_2/unfold/ltpss_sn_tpss.ma".
+
+(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+
+(* Advanced properties ******************************************************)
+
+fact ltpss_sn_tpss_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
+ L1 ⊢ T2 ▶* [d, e] U2 → ∀L0. L0 ⊢ ▶* [d, e] L1 →
+ Y1 = L1 → X2 = T2 → L0 ⊢ T2 ▶* [d, e] U2.
+#Y1 #X2 @(cw_wf_ind … Y1 X2) -Y1 -X2 #Y1 #X2 #IH
+#L1 #T2 #U2 #d #e #H @(tpss_ind_alt … H) -L1 -T2 -U2 -d -e
+[ //
+| #L1 #K1 #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK1 #HV12 #HVW2 #_ #L0 #HL01 #H1 #H2 destruct
+ lapply (ldrop_fwd_lw … HLK1) #H1 normalize in H1;
+ elim (ltpss_sn_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
+ elim (ltpss_sn_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
+ lapply (IH … HV12 … HK01 ? ?) -IH -HV12 -HK01 [1,3: // |2,4: skip | normalize /2 width=1/ ] #HV12
+ lapply (tpss_trans_eq … HV01 HV12) -V1 /2 width=6/
+| #L #a #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
+ lapply (tpss_lsubs_trans … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
+ lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
+ lapply (tpss_lsubs_trans … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
+| #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #_ #_ #L0 #HL0 #H1 #H2 destruct
+ lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
+ lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
+]
+qed.
+
+lemma ltpss_sn_tpss_trans_eq: ∀L1,T2,U2,d,e. L1 ⊢ T2 ▶* [d, e] U2 →
+ ∀L0. L0 ⊢ ▶* [d, e] L1 → L0 ⊢ T2 ▶* [d, e] U2.
+/2 width=5/ qed.
+
+lemma ltpss_sn_tps_trans_eq: ∀L0,L1,T2,U2,d,e. L0 ⊢ ▶* [d, e] L1 →
+ L1 ⊢ T2 ▶ [d, e] U2 → L0 ⊢ T2 ▶* [d, e] U2.
+/3 width=3/ qed.
+
+(* Main properties **********************************************************)
+
+theorem ltpss_sn_trans_eq: ∀L1,L,d,e. L1 ⊢ ▶* [d, e] L →
+ ∀L2. L ⊢ ▶* [d, e] L2 → L1 ⊢ ▶* [d, e] L2.
+#L1 #L #d #e #H elim H -L1 -L -d -e //
+[ #L1 #L #I #V1 #V #e #HL1 #HV1 #IHL1 #X #H
+ elim (ltpss_sn_inv_tpss21 … H ?) -H // <minus_plus_m_m #L2 #V2 #HL2 #HV2 #H destruct
+ lapply (ltpss_sn_tpss_trans_eq … HV2 … HL1) -HV2 -HL1 #HV2
+ lapply (tpss_trans_eq … HV1 … HV2) -V /3 width=1/
+| #L1 #L #I #V1 #V #d #e #HL1 #HV1 #IHL1 #X #H
+ elim (ltpss_sn_inv_tpss11 … H ?) -H // <minus_plus_m_m #L2 #V2 #HL2 #HV2 #H destruct
+ lapply (ltpss_sn_tpss_trans_eq … HV2 … HL1) -HV2 -HL1 #HV2
+ lapply (tpss_trans_eq … HV1 … HV2) -V /3 width=1/
+]
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma tps_fwd_shift1: ∀L1,L,T1,T,d,e. L ⊢ L1 @@ T1 ▶ [d, e] T →
+ ∃∃L2,T2. L @@ L1 ⊢ ▶* [d + |L1|, e] L @@ L2 & T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1
+[ #L #T1 #T #d #e #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
+| #I #L1 #V1 #IH #L #T1 #T #d #e >shift_append_assoc #H
+ elim (tps_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ elim (IH … HT12) -IH -T1 #L2 #T #HL12 #H destruct
+ <append_assoc >append_length <associative_plus
+ lapply (ltpss_sn_trans_eq (L.ⓑ{I}V1@@L1) … HL12) -HL12 /3 width=1/ #HL12
+ @(ex2_2_intro … (⋆.ⓑ{I}V2@@L2)) /2 width=4/ <append_assoc // (**) (* explicit constructor *)
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/ltpss_sn_ldrop.ma".
+
+(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+(* Properties concerning partial substitution on terms **********************)
+
+lemma ltpss_sn_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 → d1 + e1 ≤ d2 →
+ L1 ⊢ T2 ▶ [d2, e2] U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ //
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
+ lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
+ lapply (ltpss_sn_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/
+| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
+ @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_sn_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
+| /3 width=4/
+]
+qed.
+
+lemma ltpss_sn_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀L1,d1,e1. L1 ⊢ ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
+ L1 ⊢ T2 ▶ [d2, e2] U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ //
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
+ lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
+ lapply (ltpss_sn_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/
+| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
+ @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_sn_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
+| /3 width=4/
+]
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/tpss_lift.ma".
+include "basic_2/unfold/ltpss_sn_tps.ma".
+
+(* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
+
+(* Properties concerning partial unfold on terms ****************************)
+
+lemma ltpss_sn_tpss_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 → d1 + e1 ≤ d2 →
+ L1 ⊢ T2 ▶* [d2, e2] U2.
+#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU
+lapply (ltpss_sn_tps_conf_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
+qed.
+
+lemma ltpss_sn_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 →
+ ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T &
+ L0 ⊢ U2 ▶* [d1, e1] T.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ /2 width=3/
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
+ elim (lt_or_ge i2 d1) #Hi2d1
+ [ elim (ltpss_sn_ldrop_conf_le … HL01 … HLK0 ?) /2 width=2/ #X #H #HLK1
+ elim (ltpss_sn_inv_tpss11 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK0
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tpss_lift_ge … HV01 … HLK0 HVW0 … HVW1) -V0 -HLK0 // >minus_plus <plus_minus_m_m // /3 width=4/
+ | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
+ [ elim (ltpss_sn_ldrop_conf_be … HL01 … HLK0 ? ?) -HL01 // /2 width=2/ #X #H #HLK1
+ elim (ltpss_sn_inv_tpss21 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK0
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tpss_lift_ge … HV01 … HLK0 HVW0 … HVW1) -V0 -HLK0 // normalize #HW01
+ lapply (tpss_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
+ | lapply (ltpss_sn_ldrop_conf_ge … HL01 … HLK0 ?) -HL01 -HLK0 // /3 width=4/
+ ]
+ ]
+| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
+ elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
+ elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 #T #HT2 #H
+ lapply (tpss_lsubs_trans … H (L0.ⓑ{I}V) ?) -H /2 width=1/ /3 width=5/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
+ elim (IHVW2 … HL01) -IHVW2
+ elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
+]
+qed.
+
+lemma ltpss_sn_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
+ ∀L1,d1,e1. L1 ⊢ ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
+ L1 ⊢ T2 ▶* [d2, e2] U2.
+#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
+#U #U2 #_ #HU2 #IHU
+lapply (ltpss_sn_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
+qed.
+
+lemma ltpss_sn_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
+ ∀L1,d1,e1. L1 ⊢ ▶* [d1, e1] L0 →
+ ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T &
+ L1 ⊢ T ▶* [d1, e1] U2.
+#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
+[ /2 width=3/
+| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
+ elim (lt_or_ge i2 d1) #Hi2d1
+ [ elim (ltpss_sn_ldrop_trans_le … HL10 … HLK0 ?) -L0 /2 width=2/ #X #H #HLK1
+ elim (ltpss_sn_inv_tpss12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK1) #H
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // >minus_plus <plus_minus_m_m /2 width=1/ /3 width=4/
+ | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
+ [ elim (ltpss_sn_ldrop_trans_be … HL10 … HLK0 ? ?) -L0 // /2 width=2/ #X #H #HLK1
+ elim (ltpss_sn_inv_tpss22 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK1) #H
+ elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
+ lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // normalize #HW01
+ lapply (tpss_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
+ | lapply (ltpss_sn_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/
+ ]
+ ]
+| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
+ elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
+ elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 #T #HT2 #H
+ lapply (tpss_lsubs_trans … H (L1.ⓑ{I}W2) ?) -H /2 width=1/ /3 width=5/
+| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
+ elim (IHVW2 … HL10) -IHVW2
+ elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/
+]
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/ltpss_ldrop.ma".
-
-(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
-
-(* Properties concerning partial substitution on terms **********************)
-
-lemma ltpss_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
- ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → d1 + e1 ≤ d2 →
- L1 ⊢ T2 ▶ [d2, e2] U2.
-#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
-[ //
-| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
- lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
- lapply (ltpss_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/
-| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
- @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
-| /3 width=4/
-]
-qed.
-
-lemma ltpss_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
- ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
- L1 ⊢ T2 ▶ [d2, e2] U2.
-#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
-[ //
-| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
- lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
- lapply (ltpss_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/
-| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
- @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
-| /3 width=4/
-]
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/tpss_lift.ma".
-include "basic_2/unfold/ltpss_tps.ma".
-
-(* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
-
-(* Properties concerning partial unfold on terms ****************************)
-
-lemma ltpss_tpss_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
- ∀L1,d1,e1. L0 ▶* [d1, e1] L1 → d1 + e1 ≤ d2 →
- L1 ⊢ T2 ▶* [d2, e2] U2.
-#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU
-lapply (ltpss_tps_conf_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
-qed.
-
-(* Basic_1: was: subst1_subst1_back *)
-lemma ltpss_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
- ∀L1,d1,e1. L0 ▶* [d1, e1] L1 →
- ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T &
- L1 ⊢ U2 ▶* [d1, e1] T.
-#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
-[ /2 width=3/
-| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
- elim (lt_or_ge i2 d1) #Hi2d1
- [ elim (ltpss_ldrop_conf_le … HL01 … HLK0 ?) -L0 /2 width=2/ #X #H #HLK1
- elim (ltpss_inv_tpss11 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK1) #H
- elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
- lapply (tpss_lift_ge … HV01 … H HVW0 … HVW1) -V0 -H // >minus_plus <plus_minus_m_m // /3 width=4/
- | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
- [ elim (ltpss_ldrop_conf_be … HL01 … HLK0 ? ?) -L0 // /2 width=2/ #X #H #HLK1
- elim (ltpss_inv_tpss21 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK1) #H
- elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
- lapply (tpss_lift_ge … HV01 … H HVW0 … HVW1) -V0 -H // normalize #HW01
- lapply (tpss_weak … HW01 d1 e1 ? ?) [2: /2 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
- | lapply (ltpss_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /3 width=4/
- ]
- ]
-| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
- elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
- elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/
-| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
- elim (IHVW2 … HL01) -IHVW2
- elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
-]
-qed.
-
-lemma ltpss_tpss_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶* [d2, e2] U2 →
- ∀L1,d1,e1. L1 ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
- L1 ⊢ T2 ▶* [d2, e2] U2.
-#L0 #T2 #U2 #d2 #e2 #H #L1 #d1 #e1 #HL01 #Hde1d2 @(tpss_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU
-lapply (ltpss_tps_trans_ge … HU2 … HL01 ?) -L0 // -Hde1d2 /2 width=3/
-qed.
-
-(* Basic_1: was: subst1_subst1 *)
-lemma ltpss_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
- ∀L1,d1,e1. L1 ▶* [d1, e1] L0 →
- ∃∃T. L1 ⊢ T2 ▶ [d2, e2] T &
- L0 ⊢ T ▶* [d1, e1] U2.
-#L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
-[ /2 width=3/
-| #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
- elim (lt_or_ge i2 d1) #Hi2d1
- [ elim (ltpss_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2 width=2/ #X #H #HLK1
- elim (ltpss_inv_tpss12 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
- elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
- lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // >minus_plus <plus_minus_m_m /2 width=1/ /3 width=4/
- | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
- [ elim (ltpss_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 // /2 width=2/ #X #H #HLK1
- elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K1 #V1 #_ #HV01 #H destruct
- lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
- elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
- lapply (tpss_lift_ge … HV01 … H HVW1 … HVW0) -V0 -H // normalize #HW01
- lapply (tpss_weak … HW01 d1 e1 ? ?) [2: /3 width=1/ |3: /3 width=4/ ] >minus_plus >commutative_plus /2 width=1/
- | lapply (ltpss_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 -HLK0 // /3 width=4/
- ]
- ]
-| #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
- elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
- elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/
-| #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
- elim (IHVW2 … HL10) -IHVW2
- elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/
-]
-qed.
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss.ma".
+include "basic_2/unfold/ltpss_sn.ma".
(* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
definition thin: nat → nat → relation lenv ≝
- λd,e,L1,L2. ∃∃L. L1 ▶* [d, e] L & ⇩[d, e] L ≡ L2.
+ λd,e,L1,L2. â\88\83â\88\83L. L1 â\8a¢ â\96¶* [d, e] L & â\87©[d, e] L â\89¡ L2.
interpretation "basic thinning (local environment)"
'TSubst L1 d e L2 = (thin d e L1 L2).
lemma thin_inv_thin1: ∀I,K1,V1,L2,e. ▼*[0, e] K1.ⓑ{I} V1 ≡ L2 → 0 < e →
▼*[0, e - 1] K1 ≡ L2.
#I #K1 #V1 #L2 #e * #X #HK1 #HL2 #e
-elim (ltpss_inv_tpss21 … HK1 ?) -HK1 // #K #V #HK1 #_ #H destruct
+elim (ltpss_sn_inv_tpss21 … HK1 ?) -HK1 // #K #V #HK1 #_ #H destruct
lapply (ldrop_inv_ldrop1 … HL2 ?) -HL2 // /2 width=3/
qed-.
K1 ⊢ ▼*[d - 1, e] V1 ≡ V2 &
L2 = K2. ⓑ{I} V2.
#I #K1 #V1 #L2 #d #e * #X #HK1 #HL2 #e
-elim (ltpss_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct
-elim (ldrop_inv_skip1 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H destruct
-lapply (ltpss_tpss_trans_eq … HV1 … HK1) -HV1 /3 width=5/
+elim (ltpss_sn_inv_tpss11 … HK1 ?) -HK1 // #K #V #HK1 #HV1 #H destruct
+elim (ldrop_inv_skip1 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/
qed-.
(* Properties on inverse basic term relocation ******************************)
-lemma thin_delift1: ∀L1,L2,d,e. ▼*[d, e] L1 ≡ L2 → ∀V1,V2. L1 ⊢ ▼*[d, e] V1 ≡ V2 →
- ∀I. ▼*[d + 1, e] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
+lemma thin_delift: ∀L1,L2,d,e. ▼*[d, e] L1 ≡ L2 → ∀V1,V2. L1 ⊢ ▼*[d, e] V1 ≡ V2 →
+ ∀I. ▼*[d + 1, e] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
#L1 #L2 #d #e * #L #HL1 #HL2 #V1 #V2 * #V #HV1 #HV2 #I
-elim (ltpss_tpss_conf … HV1 … HL1) -HV1 #V0 #HV10 #HV0
-elim (tpss_inv_lift1_be … HV0 … HL2 … HV2 ? ?) -HV0 // <minus_n_n #X #H1 #H2
-lapply (tpss_inv_refl_O2 … H1) -H1 #H destruct
-lapply (lift_mono … H2 … HV2) -H2 #H destruct /3 width=5/
+elim (ltpss_sn_tpss_conf … HV1 … HL1) -HV1 #V0 #HV10 #HV0
+lapply (tpss_inv_lift1_eq … HV0 … HV2) -HV0 #H destruct
+lapply (ltpss_sn_tpss_trans_eq … HV10 … HL1) -HV10 /3 width=5/
qed.
lemma thin_delift_tpss_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶* [d, e] U2 →
∃∃T2. K ⊢ T1 ▶* [d, e] T2 &
L ⊢ ▼*[dd, ee] U2 ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdedd
-lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
-elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
-elim (delift_tpss_conf_le … HU1 … HUT1 … HYK ?) -HU1 -HUT1 // -Hdedd #T #HT1 #HUT
-lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
-lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+lapply (delift_ltpss_sn_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_sn_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_le … HU1 … HUT1 … HYK ?) -HU1 -HUT1 -HYK // -Hdedd #T #HT1 #HUT
+lapply (ltpss_sn_delift_trans_eq … HLY … HUT) -HLY -HUT #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U /2 width=3/
qed.
lemma thin_delift_tps_conf_le: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∃∃T2. K ⊢ T1 ▶* [d, dd - d] T2 &
L ⊢ ▼*[dd, ee] U2 ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hdde #Hddee
-lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
-elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
-elim (delift_tpss_conf_le_up … HU1 … HUT1 … HYK ? ? ?) -HU1 -HUT1 // -Hdd -Hdde -Hddee #T #HT1 #HUT
-lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
-lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+lapply (delift_ltpss_sn_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_sn_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_le_up … HU1 … HUT1 … HYK ? ? ?) -HU1 -HUT1 -HYK // -Hdd -Hdde -Hddee #T #HT1 #HUT
+lapply (ltpss_sn_delift_trans_eq … HLY … HUT) -HLY -HUT #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U /2 width=3/
qed.
lemma thin_delift_tps_conf_le_up: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
∃∃T2. K ⊢ T1 ▶* [d, e - ee] T2 &
L ⊢ ▼*[dd, ee] U2 ≡ T2.
#L #U1 #U2 #d #e #HU12 #T1 #dd #ee #HUT1 #K * #Y #HLY #HYK #Hdd #Hddee
-lapply (delift_ltpss_conf_eq … HUT1 … HLY) -HUT1 #HUT1
-elim (ltpss_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
-elim (delift_tpss_conf_be … HU1 … HUT1 … HYK ? ?) -HU1 -HUT1 // -Hdd -Hddee #T #HT1 #HUT
-lapply (tpss_delift_trans_eq … HU2 … HUT) -U #HU2T
-lapply (ltpss_delift_trans_eq … HLY … HU2T) -Y /2 width=3/
+lapply (delift_ltpss_sn_conf_eq … HUT1 … HLY) -HUT1 #HUT1
+elim (ltpss_sn_tpss_conf … HU12 … HLY) -HU12 #U #HU1 #HU2
+elim (delift_tpss_conf_be … HU1 … HUT1 … HYK ? ?) -HU1 -HUT1 -HYK // -Hdd -Hddee #T #HT1 #HUT
+lapply (ltpss_sn_delift_trans_eq … HLY … HUT) -HLY -HUT #HUT
+lapply (tpss_delift_trans_eq … HU2 … HUT) -U /2 width=3/
qed.
lemma thin_delift_tps_conf_be: ∀L,U1,U2,d,e. L ⊢ U1 ▶ [d, e] U2 →
(**************************************************************************)
include "basic_2/substitution/ldrop_ldrop.ma".
-include "basic_2/unfold/ltpss_ldrop.ma".
+include "basic_2/unfold/ltpss_sn_ldrop.ma".
include "basic_2/unfold/thin.ma".
(* BASIC LOCAL ENVIRONMENT THINNING *****************************************)
lemma thin_ldrop_conf_ge: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
d1 + e1 ≤ e2 → ⇩[0, e2 - e1] L1 ≡ L2.
-#L0 #L1 #d1 #e1 * /3 width=8 by ltpss_ldrop_conf_ge, ldrop_conf_ge/
+#L0 #L1 #d1 #e1 * /3 width=8 by ltpss_sn_ldrop_conf_ge, ldrop_conf_ge/
qed.
lemma thin_ldrop_conf_be: ∀L0,L1,d1,e1. ▼*[d1, e1] L0 ≡ L1 →
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
∃∃L. ▼*[0, d1 + e1 - e2] L2 ≡ L & ⇩[0, d1] L1 ≡ L.
#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #Hd1e2 #He2de1
-elim (ltpss_ldrop_conf_be … HL0 … HL02 ? ?) -L0 // #L0 #HL20 #HL0
+elim (ltpss_sn_ldrop_conf_be … HL0 … HL02 ? ?) -L0 // #L0 #HL20 #HL0
elim (ldrop_conf_be … HL1 … HL0 ? ?) -L // -Hd1e2 -He2de1 /3 width=3/
qed.
∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
∃∃L. ▼*[d1 - e2, e1] L2 ≡ L & ⇩[0, e2] L1 ≡ L.
#L0 #L1 #d1 #e1 * #L #HL0 #HL1 #L2 #e2 #HL02 #He2d1
-elim (ltpss_ldrop_conf_le … HL0 … HL02 ?) -L0 // #L0 #HL20 #HL0
+elim (ltpss_sn_ldrop_conf_le … HL0 … HL02 ?) -L0 // #L0 #HL20 #HL0
elim (ldrop_conf_le … HL1 … HL0 ?) -L // -He2d1 /3 width=3/
qed.
d1 ≤ e2 → ⇩[0, e1 + e2] L1 ≡ L2.
#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #Hd1e2
lapply (ldrop_trans_ge … HL0 … HL02 ?) -L0 // #HL2
-lapply (ltpss_ldrop_trans_ge … HL1 … HL2 ?) -L // /2 width=1/
+lapply (ltpss_sn_ldrop_trans_ge … HL1 … HL2 ?) -L // /2 width=1/
qed.
lemma thin_ldrop_trans_le: ∀L1,L0,d1,e1. ▼*[d1, e1] L1 ≡ L0 →
∃∃L. ▼*[d1 - e2, e1] L ≡ L2 & ⇩[0, e2] L1 ≡ L.
#L1 #L0 #d1 #e1 * #L #HL1 #HL0 #L2 #e2 #HL02 #He2d1
elim (ldrop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL0 #HL02
-elim (ltpss_ldrop_trans_le … HL1 … HL0 He2d1) -L -He2d1 /3 width=3/
+elim (ltpss_sn_ldrop_trans_le … HL1 … HL0 He2d1) -L -He2d1 /3 width=3/
qed.
(* Basic properties *********************************************************)
+lemma tpss_strap1: ∀L,T1,T,T2,d,e.
+ L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
+/2 width=3/ qed.
+
lemma tpss_strap2: ∀L,T1,T,T2,d,e.
L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
/2 width=3/ qed.
projects / helm.git / commitdiff