(* Properties concerning partial unfold on local environments ***************)
-lemma ltpss_cpr_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
- ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2.
+lemma ltpss_dx_cpr_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T1,T2. L1 ⊢ T1 ➡ T2 → L2 ⊢ T1 ⬌* T2.
#L1 #L2 #d #e #HL12 #T1 #T2 *
-lapply (ltpss_weak_all … HL12)
->(ltpss_fwd_length … HL12) -HL12 #HL12 #T #HT1 #HT2
-elim (ltpss_tpss_conf … HT2 … HL12) -L1 #T0 #HT0 #HT20
+lapply (ltpss_dx_weak_all … HL12)
+>(ltpss_dx_fwd_length … HL12) -HL12 #HL12 #T #HT1 #HT2
+elim (ltpss_dx_tpss_conf … HT2 … HL12) -L1 #T0 #HT0 #HT20
@(cprs_div … T0) /3 width=3/ (**) (* /4/ is too slow *)
qed.
-lemma ltpss_cprs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
- ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2.
+lemma ltpss_dx_cprs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T1,T2. L1 ⊢ T1 ➡* T2 → L2 ⊢ T1 ⬌* T2.
#L1 #L2 #d #e #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT1
@(cpcs_trans … IHT1) -T1 /2 width=5/
qed.
-lemma ltpss_cpcs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
- ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
+lemma ltpss_dx_cpcs_conf: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T1,T2. L1 ⊢ T1 ⬌* T2 → L2 ⊢ T1 ⬌* T2.
#L1 #L2 #d #e #HL12 #T1 #T2 #H
elim (cpcs_inv_cprs … H) -H #T #HT1 #HT2
@(cpcs_canc_dx … T) /2 width=5/
+++ /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/ltpsss.ma".
-include "basic_2/reducibility/cpr_ltpss.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
-
-(* Properties on iterated partial unfold on local environments **************)
-
-lemma ltpsss_cpr_trans: ∀L1,L2,d,e. L1 [d, e] ▶** L2 →
- ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
-#L1 #L2 #d #e #HL12 #T1 #T2 #HT12 @(ltpsss_ind_dx … HL12) -L1 // /2 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/reducibility/ltpr_tps.ma".
-include "basic_2/reducibility/cpr_ltpsss.ma".
-include "basic_2/reducibility/lcpr.ma".
-include "basic_2/computation/cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties concerning context-sensitive parallel reduction on lenv's *****)
-
-lemma ltpr_tpss_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2,d,e. L2 ⊢ T1 [d, e] ▶* T2 →
- ∃∃T. L1 ⊢ T1 [d, e] ▶* T & L1 ⊢ T ➡* T2.
-#L1 #L2 #HL12 #T1 #T2 #d #e #H @(tpss_ind … H) -T2
-[ /2 width=3/
-| #T #T2 #_ #HT2 * #T0 #HT10 #HT0
- elim (ltpr_tps_trans … HT2 … HL12) -L2 #T3 #HT3 #HT32
- @(ex2_1_intro … HT10) -T1 (**) (* explicit constructors *)
- @(cprs_strap1 … T3 …) /2 width=1/ -HT32
- @(cprs_strap1 … HT0) -HT0 /3 width=3/
-]
-qed.
-
-(* Basic_1: was just: pr3_pr0_pr2_t *)
-lemma ltpr_cpr_trans: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
-#L1 #L2 #HL12 #T1 #T2 * #T #HT1
-<(ltpr_fwd_length … HL12) #HT2
-elim (ltpr_tpss_trans … HL12 … HT2) -L2 /3 width=3/
-qed.
-
-(* Basic_1: was just: pr3_pr2_pr2_t *)
-lemma lcpr_cpr_trans: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
-#L1 #L2 * /3 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/ltpsss.ma".
-include "basic_2/reducibility/ltpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
-
-definition lcpr: relation lenv ≝
- λL1,L2. ∃∃L. L1 ➡ L & L [0, |L|] ▶** L2
-.
-
-interpretation
- "context-sensitive parallel reduction (environment)"
- 'CPRed L1 L2 = (lcpr L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma lcpr_refl: ∀L. L ⊢ ➡ L.
-/2 width=3/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆.
-#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpsss_inv_atom1 … HL2) -HL2 //
-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/static/aaa_ltpsss.ma".
-include "basic_2/reducibility/ltpr_aaa.ma".
-include "basic_2/reducibility/cpr.ma".
-include "basic_2/reducibility/lcpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
-
-(* Properties about atomic arity assignment on terms ************************)
-
-lemma aaa_lcpr_conf: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L1 ⊢ ➡ L2 → L2 ⊢ T ÷ A.
-#L1 #T #A #HT #L2 * /3 width=5/
-qed.
-
-lemma aaa_cpr_conf: ∀L,T1,A. L ⊢ T1 ÷ A → ∀T2. L ⊢ T1 ➡ T2 → L ⊢ T2 ÷ A.
-#L #T1 #A #HT1 #T2 * /3 width=5/
-qed.
-
-lemma aaa_lcpr_cpr_conf: ∀L1,T1,A. L1 ⊢ T1 ÷ A → ∀L2. L1 ⊢ ➡ L2 →
- ∀T2. L2 ⊢ T1 ➡ T2 → L2 ⊢ T2 ÷ A.
-/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/ltpsss_ltpsss.ma".
-include "basic_2/reducibility/cpr.ma".
-include "basic_2/reducibility/lcpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
-
-(* Advanced properties ****************************************************)
-
-lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 →
- ∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2.
-#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
-<(ltpsss_fwd_length … HL2) /4 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/ltpsss_ltpsss.ma".
-include "basic_2/reducibility/ltpr_ltpsss.ma".
-include "basic_2/reducibility/ltpr_ltpr.ma".
-include "basic_2/reducibility/lcpr.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ***************)
-
-(* Main properties **********************************************************)
-
-theorem lcpr_conf: ∀L0,L1,L2. L0 ⊢ ➡ L1 → L0 ⊢ ➡ L2 →
- ∃∃L. L1 ⊢ ➡ L & L2 ⊢ ➡ L.
-#K0 #L1 #L2 * #K1 #HK01 #HKL1 * #K2 #HK02 #HKL2
-lapply (ltpr_fwd_length … HK01) #H
->(ltpr_fwd_length … HK02) in H; #H
-elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2
-lapply (ltpsss_fwd_length … HKL1) #H1
-lapply (ltpsss_fwd_length … HKL2) #H2
->H1 in HKL1 H; -H1 #HKL1
->H2 in HKL2; -H2 #HKL2 #H
-elim (ltpr_ltpsss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
-elim (ltpr_ltpsss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
-elim (ltpsss_conf … HK1 … HK2) -K #K #HK1 #HK2
-lapply (ltpr_fwd_length … HLK1) #H1
-lapply (ltpr_fwd_length … HLK2) #H2
-/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/ltpsss.ma".
-include "basic_2/reducibility/ltpr_ltpss.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
-
-(* Properties on iterated parallel unfold on local environments *************)
-
-lemma ltpr_ltpsss_conf: ∀L1,K1,d,e. L1 [d, e] ▶** K1 → ∀L2. L1 ➡ L2 →
- ∃∃K2. L2 [d, e] ▶** K2 & K1 ➡ K2.
-#L1 #K1 #d #e #H @(ltpsss_ind … H) -K1 /2 width=3/
-#K #K1 #_ #HK1 #IHK #L2 #HL12
-elim (IHK … HL12) -L1 #K2 #HLK2 #HK2
-elim (ltpr_ltpss_conf … HK1 … HK2) -K /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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( T1 𝟙 break term 46 T2 )"
+ non associative with precedence 45
+ for @{ 'RTop $T1 $T2 }.
+
+include "basic_2/grammar/lenv_px.ma".
+
+(* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************)
+
+definition ttop: relation term ≝ λT1,T2. True.
+
+definition ltop: relation lenv ≝ lpx ttop.
+
+interpretation
+ "top reduction (environment)"
+ 'RTop L1 L2 = (ltop L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma ltop_refl: reflexive … ltop.
+/2 width=1/ qed.
+
+lemma ltop_sym: symmetric … ltop.
+/2 width=1/ qed.
+
+lemma ltop_trans: transitive … ltop.
+/2 width=3/ qed.
+
+lemma ltop_append: ∀K1,K2. K1 𝟙 K2 → ∀L1,L2. L1 𝟙 L2 → L1 @@ K1 𝟙 L2 @@ K2.
+/2 width=1/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltop_inv_atom1: ∀L2. ⋆ 𝟙 L2 → L2 = ⋆.
+/2 width=2 by lpx_inv_atom1/ qed-.
+
+lemma ltop_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 𝟙 L2 →
+ ∃∃K2,V2. K1 𝟙 K2 & L2 = K2. ⓑ{I} V2.
+#K1 #I #V1 #L2 #H
+elim (lpx_inv_pair1 … H) -H /2 width=4/
+qed-.
+
+lemma ltop_inv_atom2: ∀L1. L1 𝟙 ⋆ → L1 = ⋆.
+/2 width=2 by lpx_inv_atom2/ qed-.
+
+lemma ltop_inv_pair2: ∀L1,K2,I,V2. L1 𝟙 K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 𝟙 K2 & L1 = K1. ⓑ{I} V1.
+#L1 #K2 #I #V2 #H
+elim (lpx_inv_pair2 … H) -H /2 width=4/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma ltop_fwd_length: ∀L1,L2. L1 𝟙 L2 → |L1| = |L2|.
+/2 width=2 by lpx_fwd_length/ 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 "hvbox( T1 𝟙 break term 46 T2 )"
- non associative with precedence 45
- for @{ 'RTop $T1 $T2 }.
-
-include "basic_2/grammar/lenv_px.ma".
-
-(* POINTWISE EXTENSION OF TOP RELATION FOR TERMS ****************************)
-
-definition ttop: relation term ≝ λT1,T2. True.
-
-definition ltop: relation lenv ≝ lpx ttop.
-
-interpretation
- "top reduction (environment)"
- 'RTop L1 L2 = (ltop L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma ltop_refl: reflexive … ltop.
-/2 width=1/ qed.
-
-lemma ltop_sym: symmetric … ltop.
-/2 width=1/ qed.
-
-lemma ltop_trans: transitive … ltop.
-/2 width=3/ qed.
-
-lemma ltop_append: ∀K1,K2. K1 𝟙 K2 → ∀L1,L2. L1 𝟙 L2 → L1 @@ K1 𝟙 L2 @@ K2.
-/2 width=1/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma ltop_inv_atom1: ∀L2. ⋆ 𝟙 L2 → L2 = ⋆.
-/2 width=2 by lpx_inv_atom1/ qed-.
-
-lemma ltop_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 𝟙 L2 →
- ∃∃K2,V2. K1 𝟙 K2 & L2 = K2. ⓑ{I} V2.
-#K1 #I #V1 #L2 #H
-elim (lpx_inv_pair1 … H) -H /2 width=4/
-qed-.
-
-lemma ltop_inv_atom2: ∀L1. L1 𝟙 ⋆ → L1 = ⋆.
-/2 width=2 by lpx_inv_atom2/ qed-.
-
-lemma ltop_inv_pair2: ∀L1,K2,I,V2. L1 𝟙 K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 𝟙 K2 & L1 = K1. ⓑ{I} V1.
-#L1 #K2 #I #V2 #H
-elim (lpx_inv_pair2 … H) -H /2 width=4/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma ltop_fwd_length: ∀L1,L2. L1 𝟙 L2 → |L1| = |L2|.
-/2 width=2 by lpx_fwd_length/ qed-.
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/unfold/ltpss_sn_ltpss_sn.ma".
include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
(* Properties concerning partial unfold on local environments ***************)
-lemma ltpss_cpr_trans: ∀L1,L2,d,e. L1 ▶* [d, e] L2 →
- ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
+lemma ltpss_sn_cpr_trans: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
#L1 #L2 #d #e #HL12 #T1 #T2 *
-lapply (ltpss_weak_all … HL12)
-<(ltpss_fwd_length … HL12) -HL12 /3 width=5/
+lapply (ltpss_sn_weak_all … HL12)
+<(ltpss_sn_fwd_length … HL12) -HL12 /3 width=5/
qed.
#L2 #T1 #T2 * #H
lapply (length_inv_zero_sn … H) -H #H destruct /2 width=1/
qed-.
-
+(*
lemma fpr_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡ ⦃L2, T2⦄ →
∃∃K2,V2. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ &
L2 = K2.ⓑ{I}V2.
elim (length_inv_pos_sn … H) -H #I2 #K2 #V2 #HK12 #H destruct #H
elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/
qed-.
-
+*)
lemma fpr_inv_atom3: ∀L1,T1,T2. ⦃L1,T1⦄ ➡ ⦃⋆,T2⦄ → T1 ➡ T2 ∧ L1 = ⋆.
#L1 #T1 #T2 * #H
lapply (length_inv_zero_dx … H) -H #H destruct /2 width=1/
qed-.
-
+(*
lemma fpr_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡ ⦃K2.ⓑ{I}V2, T2⦄ →
∃∃K1,V1. ⦃K1, -ⓑ{I}V1.T1⦄ ➡ ⦃K2, -ⓑ{I}V2.T2⦄ &
L1 = K1.ⓑ{I}V1.
elim (length_inv_pos_dx … H) -H #I1 #K1 #V1 #HK12 #H destruct #H
elim (tpr_fwd_shift_bind_minus … H) // #_ #H0 destruct /3 width=4/
qed-.
+*)
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss.ma".
+include "basic_2/unfold/ltpss_sn.ma".
include "basic_2/reducibility/ltpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
definition lcpr: relation lenv ≝
- λL1,L2. ∃∃L. L1 ➡ L & L ▶* [0, |L|] L2
+ λL1,L2. â\88\83â\88\83L. L1 â\9e¡ L & L â\8a¢ â\96¶* [0, |L|] L2
.
interpretation
lemma lcpr_refl: ∀L. L ⊢ ➡ L.
/2 width=3/ qed.
+lemma ltpss_sn_lcpr: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 → L1 ⊢ ➡ L2.
+/3 width=5/ qed.
+
(* Basic inversion lemmas ***************************************************)
lemma lcpr_inv_atom1: ∀L2. ⋆ ⊢ ➡ L2 → L2 = ⋆.
-#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_inv_atom1 … HL2) -HL2 //
+#L2 * #L #HL >(ltpr_inv_atom1 … HL) -HL #HL2 >(ltpss_sn_inv_atom1 … HL2) -HL2 //
qed-.
(* *)
(**************************************************************************)
+include "basic_2/static/aaa_ltpss_sn.ma".
include "basic_2/reducibility/ltpr_aaa.ma".
include "basic_2/reducibility/cpr.ma".
include "basic_2/reducibility/lcpr.ma".
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/unfold/ltpss_sn_ltpss_sn.ma".
include "basic_2/reducibility/cpr.ma".
include "basic_2/reducibility/lcpr.ma".
lemma lcpr_pair: ∀L1,L2. L1 ⊢ ➡ L2 → ∀V1,V2. L2 ⊢ V1 ➡ V2 →
∀I. L1. ⓑ{I} V1 ⊢ ➡ L2. ⓑ{I} V2.
#L1 #L2 * #L #HL1 #HL2 #V1 #V2 *
-<(ltpss_fwd_length … HL2) /4 width=5/
+<(ltpss_sn_fwd_length … HL2) #V #HV1 #HV2 #I
+lapply (ltpss_sn_tpss_trans_eq … HV2 … HL2) -HV2 #V2
+@(ex2_1_intro … (L.ⓑ{I}V)) /2 width=1/ (**) (* explicit constructor *)
qed.
-
-lemma ltpss_lcpr: ∀L1,L2,d,e. L1 ▶* [d, e] L2 → L1 ⊢ ➡ L2.
-#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // /3 width=3/
-qed.
(* *)
(**************************************************************************)
-include "basic_2/reducibility/ltpr_ltpss.ma".
+include "basic_2/reducibility/ltpr_ltpss_sn.ma".
include "basic_2/reducibility/ltpr_ltpr.ma".
include "basic_2/reducibility/lcpr.ma".
lapply (ltpr_fwd_length … HK01) #H
>(ltpr_fwd_length … HK02) in H; #H
elim (ltpr_conf … HK01 … HK02) -K0 #K #HK1 #HK2
-lapply (ltpss_fwd_length … HKL1) #H1
-lapply (ltpss_fwd_length … HKL2) #H2
+lapply (ltpss_sn_fwd_length … HKL1) #H1
+lapply (ltpss_sn_fwd_length … HKL2) #H2
>H1 in HKL1 H; -H1 #HKL1
>H2 in HKL2; -H2 #HKL2 #H
-elim (ltpr_ltpss_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
-elim (ltpr_ltpss_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
-elim (ltpss_conf … HK1 … HK2) -K #K #HK1 #HK2
+elim (ltpr_ltpss_sn_conf … HKL1 … HK1) -K1 #K1 #HK1 #HLK1
+elim (ltpr_ltpss_sn_conf … HKL2 … HK2) -K2 #K2 #HK2 #HLK2
+elim (ltpss_sn_conf … HK1 … HK2) -K #K #HK1 #HK2
lapply (ltpr_fwd_length … HLK1) #H1
lapply (ltpr_fwd_length … HLK2) #H2
/3 width=5/
/2 width=2 by lpx_bi_fwd_length/ qed-.
(****************************************************************************)
-
+(*
lemma fpr_lfpra: ∀L1,T1,L2,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1⦄ ➡➡ ⦃L2⦄.
#L1 #T1 @(cw_wf_ind … L1 T1) -L1 -T1 *
[ #T1 #_ #L2 #T2 #H
<(ltpss_fwd_length … HL2) /4 width=5/
qed.
*)
+*)
*)
\ No newline at end of file
(* *)
(**************************************************************************)
-include "basic_2/static/aaa_ltpss.ma".
+include "basic_2/static/aaa_ltpss_dx.ma".
include "basic_2/static/lsuba_aaa.ma".
include "basic_2/reducibility/ltpr_ldrop.ma".
+++ /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/reducibility/tpr_tpss.ma".
-
-(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
-
-(* Properties concerning parallel unfold on local environments **************)
-
-lemma ltpr_ltpss_conf: ∀L1,K1,d,e. L1 ▶* [d, e] K1 → ∀L2. L1 ➡ L2 →
- ∃∃K2. L2 ▶* [d, e] K2 & K1 ➡ K2.
-#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
-[ /2 width=3/
-| #L1 #I #V1 #X #H
- elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
-| #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H
- elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
- elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
- elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
-| #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H
- elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
- elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
- elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /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/reducibility/tpr_tpss.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* Properties concerning dx parallel unfold on local environments ***********)
+
+lemma ltpr_ltpss_dx_conf: ∀L1,K1,d,e. L1 ▶* [d, e] K1 → ∀L2. L1 ➡ L2 →
+ ∃∃K2. L2 ▶* [d, e] K2 & K1 ➡ K2.
+#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ /2 width=3/
+| #L1 #I #V1 #X #H
+ elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct /3 width=5/
+| #L1 #K1 #I #V1 #W1 #e #_ #HVW1 #IHLK1 #X #H
+ elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
+ elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /3 width=5/
+| #L1 #K1 #I #V1 #W1 #d #e #_ #HVW1 #IHLK1 #X #H
+ elim (ltpr_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct
+ elim (IHLK1 … HL12) -L1 #K2 #HLK2 #HK12
+ elim (tpr_tpss_ltpr … HK12 … HV12 … HVW1) -V1 /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_sn_alt.ma".
+include "basic_2/reducibility/ltpr_ltpss_dx.ma".
+
+(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
+
+(* Properties on sn parallel unfold on local environments *******************)
+
+(* Note: this can also be proved like ltpr_ltpss_dx_conf *)
+lemma ltpr_ltpss_sn_conf: ∀L1,K1,d,e. L1 ⊢ ▶* [d, e] K1 → ∀L2. L1 ➡ L2 →
+ ∃∃K2. L2 ⊢ ▶* [d, e] K2 & K1 ➡ K2.
+#L1 #K1 #d #e #H
+lapply (ltpss_sn_ltpssa … H) -H #H
+@(ltpssa_ind … H) -K1 /2 width=3/
+#K #K1 #_ #HK1 #IHK #L2 #HL12
+elim (IHK … HL12) -L1 #K2 #HLK2 #HK2
+elim (ltpr_ltpss_dx_conf … HK1 … HK2) -K /3 width=3/
+qed.
/2 width=3/ qed-.
(* Basic forward lemmas *****************************************************)
-
+(*
lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T →
∃∃L2,T2. L1 𝟙 L2 & T = L2 @@ T2.
#L1 @(lenv_ind_dx … L1) -L1
| lapply (ltop_fwd_length … HL1) -HL1 normalize //
]
qed-.
-
+*)
(* Basic_1: removed theorems 3:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
Basic_1: removed local theorems: 1: pr0_delta_tau
(* *)
(**************************************************************************)
-include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/unfold/ltpss_dx_ltpss_dx.ma".
include "basic_2/reducibility/ltpr_ldrop.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
elim (IHT1 … HTU1 (L2. ⓑ{I} W2) ?) -T1 /2 width=1/ -HL12 #U #HU1 #HTU
elim (tpss_strip_neq … HTU … HT2 ?) -T /2 width=1/ #U2 #HU2 #HTU2
lapply (tps_lsubs_trans … HU2 (L2. ⓑ{I} V2) ?) -HU2 /2 width=1/ #HU2
- elim (ltpss_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23
+ elim (ltpss_dx_tps_conf … HU2 (L2. ⓑ{I} W2) (d + 1) e ?) -HU2 /2 width=1/ #U3 #HU3 #HU23
lapply (tps_lsubs_trans … HU3 (⋆. ⓑ{I} W2) ?) -HU3 /2 width=1/ #HU3
lapply (tpss_lsubs_trans … HU23 (L2. ⓑ{I} W2) ?) -HU23 /2 width=1/ #HU23
lapply (tpss_trans_eq … HTU2 … HU23) -U2 /3 width=5/
projects / helm.git / commitdiff