(* *)
(**************************************************************************)
-include "basic_2/unfold/ldrops.ma".
+include "basic_2/substitution/ldrops.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
(* *)
(**************************************************************************)
-include "basic_2/unfold/lifts_lifts.ma".
-include "basic_2/unfold/ldrops_ldrops.ma".
+include "basic_2/substitution/lifts_lifts.ma".
+include "basic_2/substitution/ldrops_ldrops.ma".
include "basic_2/static/aaa_lifts.ma".
include "basic_2/static/aaa_aaa.ma".
include "basic_2/computation/lsubc_ldrops.ma".
(**************************************************************************)
include "basic_2/grammar/aarity.ma".
-include "basic_2/unfold/gr2_gr2.ma".
-include "basic_2/unfold/lifts_lift_vector.ma".
-include "basic_2/unfold/ldrops_ldrop.ma".
+include "basic_2/substitution/gr2_gr2.ma".
+include "basic_2/substitution/lifts_lift_vector.ma".
+include "basic_2/substitution/ldrops_ldrop.ma".
include "basic_2/computation/acp.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
(* *)
(**************************************************************************)
-include "basic_2/reducibility/cnf.ma".
-include "basic_2/computation/tprs.ma".
+include "basic_2/reduction/cnf.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-definition cprs: lenv → relation term ≝
- λL. TC … (cpr L).
+(* Basic_1: includes: pr1_pr0 *)
+definition cprs: lenv → relation term ≝ LTC … cpr.
interpretation "context-sensitive parallel computation (term)"
'PRedStar L T1 T2 = (cprs L T1 T2).
lemma cpr_cprs: ∀L,T1,T2. L ⊢ T1 ➡ T2 → L ⊢ T1 ➡* T2.
/2 width=1/ qed.
+lemma cpss_cprs: ∀L,T1,T2. L ⊢ T1 ▶* T2 → L ⊢ T1 ➡* T2.
+/3 width=1/ qed.
+
(* Basic_1: was: pr3_refl *)
lemma cprs_refl: ∀L,T. L ⊢ T ➡* T.
/2 width=1/ qed.
lemma cprs_strap1: ∀L,T1,T,T2.
L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → L ⊢ T1 ➡* T2.
-/2 width=3/ qed.
+normalize /2 width=3/ qed.
(* Basic_1: was: pr3_step *)
lemma cprs_strap2: ∀L,T1,T,T2.
L ⊢ T1 ➡ T → L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
-/2 width=3/ qed.
+normalize /2 width=3/ qed.
+
+lemma cprs_cpss_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ▶* T2 → L ⊢ T1 ➡* T2.
+/3 width=3/ qed-.
+
+lemma cpss_cprs_trans: ∀L,T1,T. L ⊢ T1 ▶* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
+/3 width=3/ qed-.
+
+lemma cprs_lsubr_trans: lsubr_trans … cprs.
+/3 width=3 by cpr_lsubr_trans, TC_lsubr_trans/
+qed-.
+
+(* Basic_1: was: pr3_pr1 *)
+lemma tprs_cprs: ∀L,T1,T2. ⋆ ⊢ T1 ➡* T2 → L ⊢ T1 ➡* T2.
+#L #T1 #T2 #H @(cprs_lsubr_trans … H) -H //
+qed.
+
+lemma cprs_ext_bind_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 →
+ ∀a,I. L ⊢ ⓑ{a,I}V1.T1 ➡* ⓑ{a,I}V2.T2.
+#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a @(cprs_ind … HT12) -T2
+/3 width=1/ /3 width=6/
+qed.
-(* Note: it does not hold replacing |L1| with |L2| *)
-lemma cprs_lsubr_trans: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
- ∀L2. L2 ⊑ [0, |L1|] L1 → L2 ⊢ T1 ➡* T2.
-/3 width=3/
+lemma cprs_bind_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 →
+ ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
+#L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1
+/3 width=1/ /3 width=3/
qed.
(* Basic_1: was only: pr3_thin_dx *)
lemma cprs_flat_dx: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L ⊢ T1 ➡* T2 →
L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
#I #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 /3 width=1/
-#T #T2 #_ #HT2 #IHT2
-@(cprs_strap1 … IHT2) -IHT2 /2 width=1/
+#T #T2 #_ #HT2 #IHT1
+@(cprs_strap1 … IHT1) -V1 -T1 /2 width=1/
qed.
-lemma tpss_cprs: ∀L,T1,T2,d,e. L ⊢ T1 ▶*[d, e] T2 → L ⊢ T1 ➡* T2.
-#L #T1 #T2 #d #e #HT12
-lapply (cpr_intro … T1 … HT12) // /2 width=1/
+lemma cprs_flat_sn: ∀I,L,T1,T2. L ⊢ T1 ➡ T2 → ∀V1,V2. L ⊢ V1 ➡* V2 →
+ L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
+#I #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind … H) -V2 /3 width=1/
+#V #V2 #_ #HV2 #IHV1
+@(cprs_strap1 … IHV1) -V1 -T1 /2 width=1/
qed.
-(* Basic_1: was: pr3_pr1 *)
-lemma tprs_cprs: ∀T1,T2. T1 ➡* T2 → ∀L. L ⊢ T1 ➡* T2.
-#T1 #T2 #H @(tprs_ind … H) -T2 /2 width=1/ /3 width=3/
+lemma cprs_zeta: ∀L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
+ L.ⓓV ⊢ T1 ➡* T → L ⊢ +ⓓV.T1 ➡* T2.
+#L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/
+qed.
+
+lemma cprs_tau: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ∀V. L ⊢ ⓝV.T1 ➡* T2.
+#L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
+qed.
+
+lemma cprs_beta_dx: ∀a,L,V1,V2,W,T1,T2.
+ L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 →
+ L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2.
+#a #L #V1 #V2 #W #T1 #T2 #HV12 #H elim H -T2 /3 width=1/
+#T #T2 #_ #HT2 #IHT1
+@(cprs_strap1 … IHT1) -V1 -T1 /3 width=2/
+qed.
+
+lemma cprs_theta_dx: ∀a,L,V1,V,V2,W1,T1,T2.
+ L ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → L.ⓓW1 ⊢ T1 ➡* T2 →
+ ∀W2. L ⊢ W1 ➡ W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
+#a #L #V1 #V #V2 #W1 #T1 #T2 #HV1 #HV2 #H elim H -T2 [ /3 width=3/ ]
+#T #T2 #_ #HT2 #IHT1 #W2 #HW12
+lapply (IHT1 W1 ?) -IHT1 // #HT1
+@(cprs_strap1 … HT1) -HT1 -V -V1 /3 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
>(cpr_inv_sort1 … HU2) -HU2 //
qed-.
+(* Basic_1: was pr3_gen_appl *)
+lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 →
+ ∨∨ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
+ U2 = ⓐV2. T2
+ | ∃∃a,V2,W,T. L ⊢ V1 ➡* V2 &
+ L ⊢ T1 ➡* ⓛ{a}W. T & L ⊢ ⓓ{a}V2. T ➡* U2
+ | ∃∃a,V0,V2,V,T. L ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 &
+ L ⊢ T1 ➡* ⓓ{a}V. T & L ⊢ ⓓ{a}V. ⓐV2. T ➡* U2.
+#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpr_inv_appl1 … HU2) -HU2 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+ | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
+ lapply (cprs_strap1 … HV10 … HV02) -V0 /5 width=7/
+ | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
+ @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+ ]
+| /4 width=9/
+| /4 width=11/
+]
+qed-.
+
(* Basic_1: was: pr3_gen_cast *)
lemma cprs_inv_cast1: ∀L,W1,T1,U2. L ⊢ ⓝW1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨
∃∃W2,T2. L ⊢ W1 ➡* W2 & L ⊢ T1 ➡* T2 & U2 = ⓝW2.T2.
lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
qed-.
-lemma tprs_inv_cnf1: ∀T,U. T ➡* U → ⋆ ⊢ 𝐍⦃T⦄ → T = U.
-/3 width=3 by tprs_cprs, cprs_inv_cnf1/ qed-.
+(* Basic forward lemmas *****************************************************)
+
+(* Basic_1: was: pr3_gen_abst *)
+lemma cprs_fwd_abst1: ∀a,L,V1,T1,U2. L ⊢ ⓛ{a}V1. T1 ➡* U2 → ∀I,W.
+ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓑ{I} W ⊢ T1 ➡* T2 &
+ U2 = ⓛ{a}V2. T2.
+#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/
+#U #U2 #_ #HU2 #IHU1 #I #W
+elim (IHU1 I W) -IHU1 #V #T #HV1 #HT1 #H destruct
+elim (cpr_fwd_abst1 … HU2 I W) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+qed-.
+
+lemma cprs_fwd_abst: ∀a,L,V1,V2,T1,T2. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 → ∀I,W.
+ L ⊢ V1 ➡* V2 ∧ L. ⓑ{I} W ⊢ T1 ➡* T2.
+#a #L #V1 #V2 #T1 #T2 #H #I #W
+elim (cprs_fwd_abst1 … H I W) -H #V #T #HV1 #HT1 #H destruct /2 width=1/
+qed-.
-(* Basic_1: removed theorems 10:
+(* Basic_1: removed theorems 13:
+ pr1_head_1 pr1_head_2 pr1_comp
clear_pr3_trans pr3_cflat pr3_gen_bind
pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12
pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
(* *)
(**************************************************************************)
-include "basic_2/reducibility/cpr_aaa.ma".
+include "basic_2/reduction/lpr_aaa.ma".
include "basic_2/computation/cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
lemma aaa_cprs_conf: ∀L,T1,A. L ⊢ T1 ⁝ A → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ T2 ⁝ A.
#L #T1 #A #HT1 #T2 #HT12
-@(TC_Conf3 … HT1 ? HT12) /2 width=3/
-qed.
+@(TC_Conf3 … HT1 ? HT12) -A -T1 -T2 /2 width=3 by aaa_cpr_conf/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/reducibility/cpr_lift.ma".
-include "basic_2/reducibility/cpr_cpr.ma".
-include "basic_2/reducibility/lfpr_cpr.ma".
-include "basic_2/computation/cprs_lfpr.ma".
+include "basic_2/reduction/lpr_lpr.ma".
+include "basic_2/computation/cprs_lift.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-(* Advanced properties ******************************************************)
+(* Main properties **********************************************************)
-lemma cprs_abst_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 →
- ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a @(cprs_ind … HT12) -T2
-[ /3 width=2/
-| /3 width=6 by cprs_strap1, cpr_abst/ (**) (* /3 width=6/ is too slow *)
-]
-qed.
+(* Basic_1: was: pr3_t *)
+(* Basic_1: includes: pr1_t *)
+theorem cprs_trans: ∀L. Transitive … (cprs L).
+#L #T1 #T #HT1 #T2 @trans_TC @HT1 qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
-lemma cprs_abbr1_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 →
- ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
-#L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1
-[ /3 width=5/
-| #T1 #T #HT1 #_ #IHT1
- @(cprs_strap2 … IHT1) -IHT1 /2 width=1/
-]
+(* Basic_1: was: pr3_confluence *)
+(* Basic_1: includes: pr1_confluence *)
+theorem cprs_conf: ∀L. confluent2 … (cprs L) (cprs L).
+#L @TC_confluent2 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+
+theorem cprs_ext_bind: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 →
+ ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
+#L #V1 #V2 #H #V #T1 #T2 #HT12 #a #I @(TC_ind_dx … V1 H) -V1 /2 width=3/
+#V1 #V0 #HV10 #_ #IHV02
+@(cprs_trans … IHV02) /2 width=1/
qed.
-lemma cpr_abbr1: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡ T2 →
- ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
-/3 width=1/ qed.
-
-lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T2 →
- ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
-#L #V1 #V2 #HV12 #T1 #T2 #HT12
-lapply (lfpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/
+theorem cprs_bind: ∀a,I,L,V1,V2,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 → L ⊢ V1 ➡* V2 →
+ L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
+#a #I #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1
+@(cprs_trans … IHV1) -V1 /2 width=1/
qed.
-(* Basic_1: was: pr3_strip *)
-lemma cprs_strip: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡ T2 →
- ∃∃T0. L ⊢ T1 ➡ T0 & L ⊢ T2 ➡* T0.
-/3 width=3/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-(* Basic_1: was pr3_gen_appl *)
-lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 →
- ∨∨ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
- U2 = ⓐV2. T2
- | ∃∃a,V2,W,T. L ⊢ V1 ➡* V2 &
- L ⊢ T1 ➡* ⓛ{a}W. T & L ⊢ ⓓ{a}V2. T ➡* U2
- | ∃∃a,V0,V2,V,T. L ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 &
- L ⊢ T1 ➡* ⓓ{a}V. T & L ⊢ ⓓ{a}V. ⓐV2. T ➡* U2.
-#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
-#U #U2 #_ #HU2 * *
-[ #V0 #T0 #HV10 #HT10 #H destruct
- elim (cpr_inv_appl1 … HU2) -HU2 *
- [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
- | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct /4 width=7/
- | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
- @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
- ]
-| /4 width=9/
-| /4 width=11/
-]
-qed-.
-
-(* Main propertis ***********************************************************)
-
-(* Basic_1: was: pr3_confluence *)
-theorem cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡* T2 →
- ∃∃T0. L ⊢ T1 ➡* T0 & L ⊢ T2 ➡* T0.
-/3 width=3/ qed.
-
-(* Basic_1: was: pr3_t *)
-theorem cprs_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
-/2 width=3/ qed.
-
(* Basic_1: was: pr3_flat *)
-lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 →
- L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
-#I #L #T1 #T2 #HT12 #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/
+theorem cprs_flat: ∀I,L,V1,V2,T1,T2. L ⊢ T1 ➡* T2 → L ⊢ V1 ➡* V2 →
+ L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/
#V #V2 #_ #HV2 #IHV1
@(cprs_trans … IHV1) -IHV1 /2 width=1/
qed.
-lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 →
- ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a #I @(cprs_ind … HV12) -V2
-[ lapply (cprs_lsubr_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/
-| #V0 #V2 #_ #HV02 #IHV01
- @(cprs_trans … IHV01) -V1 /2 width=2/
-]
+theorem cprs_beta: ∀a,L,V1,V2,W,T1,T2.
+ L.ⓛW ⊢ T1 ➡* T2 → L ⊢ V1 ➡* V2 →
+ L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2.
+#a #L #V1 #V2 #W #T1 #T2 #HT12 #H @(cprs_ind … H) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1
+@(cprs_trans … IHV1) /2 width=1/
qed.
-lemma cprs_abbr1: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 →
- ∀a.L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
-#L #V1 #T1 #T2 #HT12 #V2 #HV12 #a @(cprs_ind … HV12) -V2 /2 width=1/
-#V #V2 #_ #HV2 #IHV1
-@(cprs_trans … IHV1) -IHV1 /2 width=1/
+theorem cprs_theta_rc: ∀a,L,V1,V,V2,W1,W2,T1,T2.
+ L ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → L.ⓓW1 ⊢ T1 ➡* T2 →
+ L ⊢ W1 ➡* W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
+#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 #HT12 #H elim H -W2 /2 width=3/
+#W #W2 #_ #HW2 #IHW1
+@(cprs_trans … IHW1) /2 width=1/
qed.
-lemma cprs_bind1: ∀I,L,V1,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 →
- ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-* /2 width=1/ /2 width=2/
+theorem cprs_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2.
+ ⇧[0, 1] V ≡ V2 → L ⊢ W1 ➡* W2 → L.ⓓW1 ⊢ T1 ➡* T2 →
+ L ⊢ V1 ➡* V → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
+#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV2 #HW12 #HT12 #H @(TC_ind_dx … V1 H) -V1 /2 width=3/
+#V1 #V0 #HV10 #_ #IHV0
+@(cprs_trans … IHV0) /2 width=1/
qed.
-lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 →
- ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
-#L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1
-[ /2 width=1/
-| #T1 #T #HT1 #_ #IHT1
- lapply (lfpr_cpr_trans (L. ⓓV1) … HT1) -HT1 /2 width=1/ #HT1
- @(cprs_trans … IHT1) -IHT1 /2 width=1/
+(* Properties concerning sn parallel reduction on local environments ********)
+
+(* Basic_1: was just: pr3_pr2_pr2_t *)
+(* Basic_1: includes: pr3_pr0_pr2_t *)
+lemma lpr_cpr_trans: s_r_trans … cpr lpr.
+#L2 #T1 #T2 #HT12 elim HT12 -L2 -T1 -T2
+[ /2 width=3/
+| #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
+ elim (lpr_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+ elim (lpr_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
+ lapply (IHV02 … HK12) -K2 #HV02
+ lapply (cprs_strap2 … HV10 … HV02) -V0 /2 width=6/
+| #a #I #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
+ lapply (IHT12 (L1.ⓑ{I}V1) ?) -IHT12 /2 width=1/ /3 width=1/
+|4,6: /3 width=1/
+| #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #HL12
+ lapply (IHT1 (L1.ⓓV2) ?) -IHT1 /2 width=1/ /2 width=3/
+| #a #L2 #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #HL12
+ lapply (IHT12 (L1.ⓛW) ?) -IHT12 /2 width=1/ /3 width=1/
+| #a #L2 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #HL12
+ lapply (IHT12 (L1.ⓓW1) ?) -IHT12 /2 width=1/ /3 width=3/
]
-qed.
+qed-.
-lemma cprs_abbr2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 →
- ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2.
-#L #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/
-#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12 #a
-lapply (IHV1 T1 T1 ? a) -IHV1 // #HV1
-@(cprs_trans … HV1) -HV1 /2 width=1/
+lemma cpr_bind2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡ T2 →
+ ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
+#L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+lapply (lpr_cpr_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
qed.
-lemma cprs_bind2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 →
- ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
-#L #V1 #V2 #HV12 * /2 width=1/ /2 width=2/
-qed.
+(* Advanced properties ******************************************************)
-lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2.
- L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 →
- ∀a.L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2.
-#L #V1 #V2 #W #T1 #T2 #HV12 #HT12 #a @(cprs_ind … HT12) -T2
-[ /3 width=1/
-| -HV12 #T #T2 #_ #HT2 #IHT1
- lapply (cpr_lsubr_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
- @(cprs_trans … IHT1) -V1 -W -T1 /3 width=1/
+(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
+lemma lpr_cprs_trans: s_rs_trans … cpr lpr.
+/3 width=5 by s_r_trans_TC1, lpr_cpr_trans/ qed-.
+
+(* Basic_1: was: pr3_strip *)
+(* Basic_1: includes: pr1_strip *)
+lemma cprs_strip: ∀L. confluent2 … (cprs L) (cpr L).
+#L @TC_strip1 /2 width=3 by cpr_conf/ qed-. (**) (* auto /3 width=3/ does not work because a δ-expansion gets in the way *)
+
+lemma cprs_lpr_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡ L1 →
+ ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
+#L0 #T0 #T1 #H elim H -T1
+[ #T1 #HT01 #L1 #HL01
+ elim (lpr_cpr_conf_dx … HT01 … HL01) -L0 /3 width=3/
+| #T #T1 #_ #HT1 #IHT0 #L1 #HL01
+ elim (IHT0 … HL01) #T2 #HT2 #HT02
+ elim (lpr_cpr_conf_dx … HT1 … HL01) -L0 #T3 #HT3 #HT13
+ elim (cprs_strip … HT2 … HT3) -T #T #HT2 #HT3
+ lapply (cprs_strap2 … HT13 … HT3) -T3
+ lapply (cprs_strap1 … HT02 … HT2) -T2 /2 width=3/
]
-qed.
+qed-.
-lemma ltpr_cprs_trans: ∀L1,L2. L1 ➡ L2 →
- ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
-#T #T2 #_ #HT2 #IHT2
-@(cprs_trans … IHT2) /2 width=3/
-qed.
+lemma cprs_lpr_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡ L1 →
+ ∃∃T. L0 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cprs_lpr_conf_dx … HT01 … HL01) -HT01 #T #HT1
+lapply (lpr_cprs_trans … HT1 … HL01) -HT1 /2 width=3/
+qed-.
-(* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
-lemma lcpr_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ →
- ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
-#T #T2 #_ #HT2 #IHT2
-@(cprs_trans … IHT2) /2 width=3/
+lemma cprs_bind2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 →
+ ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
+#L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+lapply (lpr_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /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/reducibility/cpr_delift.ma".
-include "basic_2/reducibility/cpr_cpr.ma".
-include "basic_2/computation/cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties on inverse basic term relocation ******************************)
-
-(* Note: this should be stated with tprs *)
-lemma cprs_zeta_delift: ∀L,V,T1,T2. L.ⓓV ⊢ ▼*[O, 1] T1 ≡ T2 → L ⊢ +ⓓV.T1 ➡* T2.
-#L #V #T1 #T2 * #T #HT1 #HT2
-@(cprs_strap2 … (+ⓓV.T)) [ /3 width=3/ | @inj /3 width=3/ ] (**) (* explicit constructor, /5 width=3/ is too slow *)
-qed.
-
-(* Basic_1: was only: pr3_gen_cabbr *)
-lemma thin_cprs_delift_conf: ∀L,U1,U2. L ⊢ U1 ➡* U2 →
- ∀K,d,e. ▼*[d, e] L ≡ K → ∀T1. L ⊢ ▼*[d, e] U1 ≡ T1 →
- ∃∃T2. K ⊢ T1 ➡* T2 & L ⊢ ▼*[d, e] U2 ≡ T2.
-#L #U1 #U2 #H @(cprs_ind … H) -U2 /2 width=3/
-#U #U2 #_ #HU2 #IHU1 #K #d #e #HLK #T1 #HTU1
-elim (IHU1 … HLK … HTU1) -U1 #T #HT1 #HUT
-elim (thin_cpr_delift_conf … HU2 … HLK … HUT) -U -HLK /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/reducibility/ltpr_tps.ma".
-include "basic_2/reducibility/cpr_ltpss_sn.ma".
-include "basic_2/reducibility/lfpr.ma".
-include "basic_2/computation/cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties concerning focalized parallel reduction on local environments *)
-
-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_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 lfpr_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/computation/cprs_cprs.ma".
-include "basic_2/computation/lfprs_lfprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties on focalized computation for local environments ***************)
-
-(* Basic_1: was just: pr3_pr3_pr3_t *)
-lemma lfprs_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ →
- ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-#L1 #L2 #HL12 @(lfprs_ind … HL12) -L2 // /3 width=3/
-qed.
-
-lemma lfprs_cpr_trans: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ →
- ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡* T2.
-/3 width=3 by lfprs_cprs_trans, inj/ qed.
-
-(* Advanced inversion lemmas ************************************************)
-
-(* Basic_1: was pr3_gen_abbr *)
-lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1. T1 ➡* U2 →
- (∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
- U2 = ⓓ{a}V2. T2
- ) ∨
- ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
-#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
-#U0 #U2 #_ #HU02 * *
-[ #V0 #T0 #HV10 #HT10 #H destruct
- elim (cpr_inv_abbr1 … HU02) -HU02 *
- [ #V #V2 #T2 #HV0 #HV2 #HT02 #H destruct
- lapply (cpr_intro … HV0 … HV2) -HV2 #HV02
- lapply (ltpr_cpr_trans (L.ⓓV0) … HT02) /2 width=1/ -V #HT02
- lapply (lfprs_cprs_trans (L. ⓓV1) … HT02) -HT02 /2 width=1/ /4 width=5/
- | #T2 #HT02 #HUT2
- lapply (lfprs_cpr_trans (L.ⓓV1) … HT02) -HT02 /2 width=1/ -V0 #HT02
- lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/
- ]
-| #U1 #HTU1 #HU01
- elim (lift_total U2 0 1) #U #HU2
- lapply (cpr_lift (L.ⓓV1) … HU01 … HU2 HU02) -U0 /2 width=1/ /4 width=3/
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/reducibility/cpr_lift.ma".
+include "basic_2/reduction/cpr_lift.ma".
include "basic_2/computation/cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+(* Advanced properties ******************************************************)
+
+(* Note: apparently this was missing in basic_1 *)
+lemma cprs_delta: ∀L,K,V,V2,i.
+ ⇩[0, i] L ≡ K. ⓓV → K ⊢ V ➡* V2 →
+ ∀W2. ⇧[0, i + 1] V2 ≡ W2 → L ⊢ #i ➡* W2.
+#L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ]
+#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
+lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+elim (lift_total V1 0 (i+1)) /4 width=11 by cpr_lift, cprs_strap1/
+qed.
+
(* Advanced inversion lemmas ************************************************)
(* Basic_1: was: pr3_gen_lref *)
T2 = #i ∨
∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 &
K ⊢ V1 ➡* T1 &
- ⇧[0, i + 1] T1 ≡ T2 &
- i < |L|.
+ ⇧[0, i + 1] T1 ≡ T2.
#L #T2 #i #H @(cprs_ind … H) -T2 /2 width=1/
#T #T2 #_ #HT2 *
[ #H destruct
elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1/
- * #K #V1 #T1 #HLK #HVT1 #HT12 #Hi
- @or_intror @(ex4_3_intro … HLK … HT12) // /3 width=3/ (**) (* explicit constructors *)
-| * #K #V1 #T1 #HLK #HVT1 #HT1 #Hi
+ * /4 width=6/
+| * #K #V1 #T1 #HLK #HVT1 #HT1
lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
- elim (cpr_inv_lift1 … H0LK … HT1 … HT2) -H0LK -T /4 width=6/
+ elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=6/
]
qed-.
-(* Basic_1: was: pr3_gen_abst *)
-lemma cprs_inv_abst1: ∀I,W,a,L,V1,T1,U2. L ⊢ ⓛ{a}V1. T1 ➡* U2 →
- ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓑ{I} W ⊢ T1 ➡* T2 &
- U2 = ⓛ{a}V2. T2.
-#I #W #a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/
-#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
-elim (cpr_inv_abst1 … HU2 I W) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
-qed-.
-
-lemma cprs_inv_abst: ∀a,L,V1,V2,T1,T2. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 → ∀I,W.
- L ⊢ V1 ➡* V2 ∧ L. ⓑ{I} W ⊢ T1 ➡* T2.
-#a #L #V1 #V2 #T1 #T2 #H #I #W
-elim (cprs_inv_abst1 I W … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/
-qed-.
-
(* Relocation properties ****************************************************)
(* Basic_1: was: pr3_lift *)
-lemma cprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 →
- ∀T2. K ⊢ T1 ➡* T2 → ∀U2. ⇧[d, e] T2 ≡ U2 →
- L ⊢ U1 ➡* U2.
-#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #HT12 @(cprs_ind … HT12) -T2
-[ -HLK #T2 #HT12
- <(lift_mono … HTU1 … HT12) -T1 //
-| -HTU1 #T #T2 #_ #HT2 #IHT2 #U2 #HTU2
- elim (lift_total T d e) #U #HTU
- lapply (cpr_lift … HLK … HTU … HTU2 … HT2) -T2 -HLK /3 width=3/
-]
-qed.
+lemma cprs_lift: l_liftable cprs.
+/3 width=9/ qed.
(* Basic_1: was: pr3_gen_lift *)
-lemma cprs_inv_lift1: ∀L,K,d,e. ⇩[d, e] L ≡ K →
- ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀U2. L ⊢ U1 ➡* U2 →
- ∃∃T2. ⇧[d, e] T2 ≡ U2 & K ⊢ T1 ➡* T2.
-#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 #HU12 @(cprs_ind … HU12) -U2 /2 width=3/
--HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1
-elim (cpr_inv_lift1 … HLK … HTU … HU2) -U -HLK /3 width=5/
-qed.
+lemma cprs_inv_lift1: l_deliftable_sn cprs.
+/3 width=5 by l_deliftable_sn_LTC, cpr_inv_lift1/
+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/substitution/lpss_cpss.ma".
+include "basic_2/reduction/lpr_lpss.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties on parallel substitution for terms ****************************)
+
+(* Basic_1: was: pr3_subst1 *)
+lemma cprs_cpss_conf: ∀L,T0,T1. L ⊢ T0 ➡* T1 → ∀T2. L ⊢ T0 ▶* T2 →
+ ∃∃T. L ⊢ T1 ▶* T & L ⊢ T2 ➡* T.
+#L @TC_strip1 /2 width=3 by cpr_cpss_conf/ qed-. (**) (* auto /3 width=3/ fails because a δ-expansion gets in the way *)
+
+(* Properties on sn parallel substitution for local environments ************)
+
+lemma cprs_lpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ▶* L1 →
+ ∃∃T. L1 ⊢ T1 ▶* T & L1 ⊢ T0 ➡* T.
+#L0 #T0 #T1 #H elim H -T1
+[ #T1 #HT01 #L1 #HL01
+ elim (cpr_lpss_conf_dx … HT01 … HL01) -L0 /3 width=3/
+| #T #T1 #_ #HT1 #IHT0 #L1 #HL01
+ elim (IHT0 … HL01) #T2 #HT2 #HT02
+ elim (cpr_lpss_conf_dx … HT1 … HL01) -L0 #T3 #HT13 #HT3
+ elim (cpr_cpss_conf … HT3 … HT2) -T #T #HT3 #HT2
+ lapply (cpss_trans … HT13 … HT3) -T3
+ lapply (cprs_strap1 … HT02 … HT2) -T2 /2 width=3/
+]
+qed-.
+
+lemma cprs_lpss_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ▶* L1 →
+ ∃∃T. L0 ⊢ T1 ▶* T & L1 ⊢ T0 ➡* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (cprs_lpss_conf_dx … HT01 … HL01) -HT01 #T #HT1
+lapply (lpss_cpss_trans … HL01 … HT1) -HT1 /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/reducibility/cpr_ltpr.ma".
-include "basic_2/computation/cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties concerning parallel unfold on terms ***************************)
-
-(* Basic_1: was only: pr3_subst1 *)
-lemma cprs_tpss_ltpr: ∀L1,T1,U1,d,e. L1 ⊢ T1 ▶* [d, e] U1 →
- ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
- ∃∃U2. L2 ⊢ U1 ➡* U2 & L2 ⊢ T2 ▶* [d, e] U2.
-#L1 #T1 #U1 #d #e #HTU1 #L2 #HL12 #T2 #HT12 elim HT12 -T2
-[ #T2 #HT12
- elim (cpr_tpss_ltpr … HL12 … HT12 … HTU1) -L1 -T1 /3 width=3/
-| #T #T2 #_ #HT2 * #U #HU1 #HTU
- elim (cpr_tpss_ltpr … HT2 … HTU) -L1 -T // /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/reducibility/cpr_ltpss_dx.ma".
-include "basic_2/computation/cprs_tpss.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties concerning dx partial unfold on local environments ************)
-
-lemma cprs_ltpss_dx_conf: ∀L1,T,U1. L1 ⊢ T ➡* U1 →
- ∀L2,d,e. L1 ▶* [d, e] L2 →
- ∃∃U2. L2 ⊢ T ➡* U2 & L2 ⊢ U1 ▶* [d, e] U2.
-#L1 #T #U1 #H @(cprs_ind … H) -U1 /2 width=3/
-#T1 #U1 #_ #HTU1 #IHT1 #L2 #d #e #HL12
-elim (IHT1 … HL12) -IHT1 #U #HTU #HT1U
-elim (ltpss_dx_cpr_conf … HTU1 … HL12) -L1 #U0 #HT1U0 #HU10
-elim (cpr_tpss_conf … HT1U0 … HT1U) -T1 #U2 #HU02 #HU2
-lapply (tpss_trans_eq … HU10 HU02) -U0 /3 width=3/
-qed-.
-
-lemma cprs_ltpss_dx_tpss_conf: ∀L1,T1,U1. L1 ⊢ T1 ➡* U1 →
- ∀L2,d,e. L1 ▶* [d, e] L2 →
- ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
- ∃∃U2. L2 ⊢ T2 ➡* U2 & L2 ⊢ U1 ▶* [d, e] U2.
-#L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12
-elim (cprs_ltpss_dx_conf … HTU1 … HL12) -L1 #U #HT1U #HU1
-elim (cprs_tpss_conf … HT1U … HT12) -T1 #T #HUT #HT2
-lapply (tpss_trans_eq … HU1 HUT) -U /2 width=3/
-qed-.
-
-lemma cprs_ltpss_dx_tpss2_conf: ∀L1,T1,U1. L1 ⊢ T1 ➡* U1 →
- ∀L2,d,e. L1 ▶* [d, e] L2 →
- ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
- ∀U2. L2 ⊢ U1 ▶* [d, e] U2 →
- ∃∃U. L2 ⊢ T2 ➡* U & L2 ⊢ U2 ▶* [d, e] U.
-#L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12 #U2 #HU12
-elim (cprs_ltpss_dx_tpss_conf … HTU1 … HL12 … HT12) -L1 -T1 #U #HT2U #HU1
-elim (tpss_conf_eq … HU12 … HU1) -U1 #U0 #HU20 #HU0
-lapply (cprs_tpss_trans … HT2U … HU0) -U /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/ltpss_sn_alt.ma".
-include "basic_2/computation/cprs_ltpss_dx.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties concerning sn partial unfold on local environments ************)
-
-lemma cprs_ltpss_sn_conf: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 →
- ∀T,U1. L1 ⊢ T ➡* U1 →
- ∃∃U2. L2 ⊢ T ➡* U2 & L1 ⊢ U1 ▶* [d, e] U2.
-#L1 #L2 #d #e #H
-lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 /2 width=3/
-#L #L2 #HL1 #HL2 #IHL1 #T #U1 #HTU1
-lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1
-lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12
-elim (IHL1 … HTU1) -IHL1 -HTU1 #U #HTU #HU1
-elim (cprs_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #HTU2 #HU2
-lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2
-lapply (tpss_trans_eq … HU1 HU2) -U /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/reducibility/cpr_tpss.ma".
-include "basic_2/computation/cprs.ma".
-
-(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
-
-(* Properties on partial unfold for terms ***********************************)
-
-lemma cprs_tpss_trans: ∀L,T1,T. L ⊢ T1 ➡* T →
- ∀T2,d,e. L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ➡* T2.
-#L #T1 #T #H @(cprs_ind … H) -T /2 width=3/ /3 width=5/
-qed.
-
-lemma cprs_tps_trans: ∀L,T1,T. L ⊢ T1 ➡* T →
- ∀T2,d,e. L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ➡* T2.
-/3 width=5 by inj, cprs_tpss_trans/ qed. (**) (* auto too slow without trace *)
-
-lemma cprs_tpss_conf: ∀L,T0,T1. L ⊢ T0 ➡* T1 →
- ∀T2,d,e. L ⊢ T0 ▶* [d, e] T2 →
- ∃∃T. L ⊢ T1 ▶* [d, e] T & L ⊢ T2 ➡* T.
-#L #T0 #T1 #H @(cprs_ind … H) -T1 /2 width=3/
-#T #T1 #_ #HT1 #IHT0 #T2 #d #e #HT02
-elim (IHT0 … HT02) -T0 #T0 #HT0 #HT20
-elim (cpr_tpss_conf … HT1 … HT0) -T /3 width=5/
-qed-.
(**************************************************************************)
include "basic_2/grammar/tstc.ma".
-include "basic_2/computation/cprs_lift.ma".
-include "basic_2/computation/cprs_lfprs.ma".
+include "basic_2/computation/lprs_cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
elim (cprs_inv_appl1 … H) -H *
[ #V0 #T0 #_ #_ #H destruct /2 width=1/
| #b #V0 #W0 #T0 #HV0 #HT0 #HU
- elim (cprs_inv_abst1 Abbr V … HT0) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1
+ elim (cprs_fwd_abst1 … HT0 Abbr V) -HT0 #W1 #T1 #_ #HT1 #H destruct -W1
@or_intror -W
@(cprs_trans … HU) -U /2 width=1/ (**) (* explicit constructor *)
| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
- elim (cprs_inv_abst1 Abbr V … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
+ elim (cprs_fwd_abst1 … HT1 Abbr V) -HT1 #W2 #T2 #_ #_ #H destruct
]
qed-.
#i ≃ U ∨ L ⊢ V2 ➡* U.
#L #K #V1 #i #HLK #V2 #HV12 #U #H
elim (cprs_inv_lref1 … H) -H /2 width=1/
-* #K0 #V0 #U0 #HLK0 #HVU0 #HU0 #_
+* #K0 #V0 #U0 #HLK0 #HVU0 #HU0
lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/
qed-.
@or_intror @(cprs_trans … HU) -U (**) (* explicit constructor *)
elim (cprs_inv_abbr1 … HT0) -HT0 *
[ #V5 #T5 #HV5 #HT5 #H destruct
- lapply (cprs_lift (L.ⓓV) … HV12 … HV13 … HV34) -V1 -V3 /2 width=1/
+ lapply (cprs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3 /2 width=1/
/3 width=1/
| #X #HT1 #H #H0 destruct
elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
- lapply (cprs_lift (L.ⓓV0) … HV12 … HV13 … HV34) -V3 /2 width=1/ #HV24
+ lapply (cprs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=1/ #HV24
@(cprs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1/ ] -T
@(cprs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V5 -T5
@(cprs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) [ /3 width=3/ ] -V1 /3 width=1/
(**************************************************************************)
include "basic_2/grammar/tstc_vector.ma".
-include "basic_2/substitution/lift_vector.ma".
+include "basic_2/relocation/lift_vector.ma".
include "basic_2/computation/cprs_tstc.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
@(cprs_trans … HU) -U
elim (cprs_inv_abbr1 … HT0) -HT0 *
[ #V1 #T1 #HV1 #HT1 #H destruct
- lapply (cprs_lift (L.ⓓV) … HV12a … HV10a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a
+ lapply (cprs_lift … HV10a (L.ⓓV) … HV12a … HV0a) -V1a -V0a [ /2 width=1/ ] #HV2a
@(cprs_trans … (ⓓ{a}V.ⓐV2a.T1)) [ /3 width=1/ ] -T -V2b -V2s /3 width=1/
| #X #HT1 #H #H0 destruct
elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
- lapply (cprs_lift (L.ⓓV0) … HV12a … HV10a … HV0a) -V0a [ /2 width=1/ ] #HV2a
+ lapply (cprs_lift … HV10a (L.ⓓV0) … HV12a … HV0a) -V0a [ /2 width=1/ ] #HV2a
@(cprs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1/ ] -T -V2b -V2s
@(cprs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /5 width=7/ ] -V -V1 -T1
@(cprs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/
(* *)
(**************************************************************************)
-include "basic_2/reducibility/cnf.ma".
+include "basic_2/reduction/cnf.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* Basic forward lemmas *****************************************************)
+fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬊* V.
+#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
+@csn_intro #V2 #HLV2 #HV2
+@(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
+qed-.
+
+(* Basic_1: was: sn3_gen_head *)
+lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬊* ②{I} V. T → L ⊢ ⬊* V.
+/2 width=5 by csn_fwd_pair_sn_aux/ qed-.
+
+fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬊* U →
+ ∀a,I,V,T. U = ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T.
+#L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct
+@csn_intro #T2 #HLT2 #HT2
+@(IH (ⓑ{a,I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
+qed-.
+
+(* Basic_1: was: sn3_gen_bind *)
+lemma csn_fwd_bind_dx: ∀a,I,L,V,T. L ⊢ ⬊* ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T.
+/2 width=4 by csn_fwd_bind_dx_aux/ qed-.
+
fact csn_fwd_flat_dx_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ⓕ{I} V. T → L ⊢ ⬊* T.
#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
@csn_intro #T2 #HLT2 #HT2
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-(* Properties concerning atomic arity assignment ****************************)
+(* Main properties concerning atomic arity assignment ***********************)
-lemma csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T.
+theorem csn_aaa: ∀L,T,A. L ⊢ T ⁝ A → L ⊢ ⬊* T.
#L #T #A #H
@(acp_aaa … csn_acp csn_acr … H)
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/cpr_cpr.ma".
-include "basic_2/computation/csn.ma".
-
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-
-(* Advanced forvard lemmas **************************************************)
-
-fact csn_fwd_pair_sn_aux: ∀L,U. L ⊢ ⬊* U → ∀I,V,T. U = ②{I} V. T → L ⊢ ⬊* V.
-#L #U #H elim H -H #U0 #_ #IH #I #V #T #H destruct
-@csn_intro #V2 #HLV2 #HV2
-@(IH (②{I} V2. T)) -IH // /2 width=1/ -HLV2 #H destruct /2 width=1/
-qed.
-
-(* Basic_1: was: sn3_gen_head *)
-lemma csn_fwd_pair_sn: ∀I,L,V,T. L ⊢ ⬊* ②{I} V. T → L ⊢ ⬊* V.
-/2 width=5/ qed.
-
-fact csn_fwd_bind_dx_aux: ∀L,U. L ⊢ ⬊* U →
- ∀a,I,V,T. U = ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T.
-#L #U #H elim H -H #U0 #_ #IH #a #I #V #T #H destruct
-@csn_intro #T2 #HLT2 #HT2
-@(IH (ⓑ{a,I} V. T2)) -IH // /2 width=1/ -HLT2 #H destruct /2 width=1/
-qed.
-
-(* Basic_1: was: sn3_gen_bind *)
-lemma csn_fwd_bind_dx: ∀a,I,L,V,T. L ⊢ ⬊* ⓑ{a,I} V. T → L. ⓑ{I} V ⊢ ⬊* T.
-/2 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/computation/csn_cpr.ma".
-include "basic_2/computation/csn_vector.ma".
-
-(* Advanced forward lemmas **************************************************)
-
-lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬊* Ⓐ Vs. T → L ⊢ ⬊* Vs ∧ L ⊢ ⬊* T.
-#L #T #Vs elim Vs -Vs /2 width=1/
-#V #Vs #IHVs #HVs
-lapply (csn_fwd_pair_sn … HVs) #HV
-lapply (csn_fwd_flat_dx … HVs) -HVs #HVs
-elim (IHVs HVs) -IHVs -HVs /3 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/grammar/tstc_tstc.ma".
-include "basic_2/computation/cprs_cprs.ma".
-include "basic_2/computation/csn_lift.ma".
-include "basic_2/computation/csn_cpr.ma".
-include "basic_2/computation/csn_alt.ma".
-
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma csn_lfpr_conf: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T.
-#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
-@csn_intro #T0 #HLT0 #HT0
-@IHT /2 width=2/ -IHT -HT0 /2 width=3/
-qed.
-
-lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T.
-#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
-@csn_intro #X #H1 #H2
-elim (cpr_inv_abbr1 … H1) -H1 *
-[ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct
- lapply (cpr_intro … HLV0 HLV01) -HLV01 #HLV1
- lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1
- elim (eq_false_inv_tpair_sn … H2) -H2
- [ #HV1 @IHV // /2 width=1/ -HV1
- @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
- | -IHV -HLV1 * #H destruct /3 width=1/
- ]
-| -IHV -IHT -H2 #T0 #HLT0 #HT0
- lapply (csn_cpr_trans … HT … HLT0) -T #HLT0
- lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/
-]
-qed.
-
-fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U →
- ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
-#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct
-lapply (csn_fwd_pair_sn … HVT) #HV
-lapply (csn_fwd_bind_dx … HVT) #HT -HVT
-@csn_intro #X #H #H2
-elim (cpr_inv_appl1 … H) -H *
-[ #V0 #Y #HLV0 #H #H0 destruct
- elim (cpr_inv_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct
- elim (eq_false_inv_beta … H2) -H2
- [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0
- @csn_abbr /2 width=3/ -HV
- @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
- | -IHW -HLW0 -HV -HT * #H #HVT0 destruct
- @(IHVT … HVT0) -IHVT -HVT0 // /2 width=1/
- ]
-| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct
- lapply (lfpr_cpr_trans (L. ⓓV) … HLT01) -HLT01 /2 width=1/ #HLT01
- @csn_abbr /2 width=3/ -HV
- @(csn_lfpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
-| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct
-]
-qed.
-
-(* Basic_1: was: sn3_beta *)
-lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T →
- L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
-/2 width=3/ qed.
-
-fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
-#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
-lapply (csn_fwd_pair_sn … HVT) #HV
-lapply (csn_fwd_bind_dx … HVT) -HVT #HVT
-@csn_intro #X #HL #H
-elim (cpr_inv_appl1 … HL) -HL *
-[ -HV #V0 #Y #HLV10 #HL #H0 destruct
- elim (cpr_inv_abbr1 … HL) -HL *
- [ #V3 #V4 #T3 #HV3 #HLV34 #HLT3 #H0 destruct
- lapply (cpr_intro … HV3 HLV34) -HLV34 #HLV34
- elim (lift_total V0 0 1) #V5 #HV05
- elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V4.ⓐV5.T3))
- [ -IHVT #H0 destruct
- elim (eq_false_inv_tpair_sn … H) -H
- [ -HLV10 -HLV34 -HV3 -HLT3 -HVT
- >(lift_inj … HV12 … HV05) -V5
- #H elim (H ?) //
- | * #_ #H elim (H ?) //
- ]
- | -H -HVT #H
- lapply (cpr_lift (L. ⓓV) … HV12 … HV05 HLV10) -HLV10 -HV12 /2 width=1/ #HV25
- lapply (ltpr_cpr_trans (L. ⓓV) … HLT3) /2 width=1/ -HLT3 #HLT3
- @(IHVT … H … HV05) -IHVT // -H -HV05 /3 width=1/
- ]
- | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
- lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0
- lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
- @(csn_cpr_trans … HVY) /2 width=1/
- ]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct
-| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HLW01 #HLT01 #HV03 #H1 #H2 destruct
- lapply (cpr_lift (L. ⓓW0) … HV12 … HV03 HLV10) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23
- lapply (lfpr_cpr_trans (L. ⓓW0) … HLT01) -HLT01 /2 width=1/ #HLT01
- @csn_abbr /2 width=3/ -HV
- @(csn_lfpr_conf (L. ⓓW0)) /2 width=1/ -W1
- @(csn_cprs_trans … HVT) -HVT /2 width=1/
-]
-qed.
-
-lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
- ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
-/2 width=5/ qed.
-
-(* Basic_1: was only: sn3_appl_appl *)
-lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1.
- L ⊢ ⬊* T1 →
- (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) →
- 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1.
-#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
-@csn_intro #X #HL #H
-elim (cpr_inv_appl1_simple … HL ?) -HL //
-#V0 #T0 #HLV0 #HLT10 #H0 destruct
-elim (eq_false_inv_tpair_sn … H) -H
-[ -IHT1 #HV0
- @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10
- @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0
- #T2 #HLT12 #HT12
- @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
- @H2T1 -H2T1 // -HLT12 /2 width=1/
-| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
- elim (tstc_dec T1 T0) #H2T10
- [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1
- #T2 #HLT02 #HT02
- @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/
- | -IHT1 -H3T1 -H1T10
- @H2T1 -H2T1 /2 width=1/
- ]
-]
-qed.
(* *)
(**************************************************************************)
-include "basic_2/reducibility/cnf_lift.ma".
+include "basic_2/reduction/cnf_lift.ma".
include "basic_2/computation/acp.ma".
include "basic_2/computation/csn.ma".
∀T2. ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → L2 ⊢ ⬊* T2.
#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL21 #HT12
@csn_intro #T #HLT2 #HT2
-elim (cpr_inv_lift1 … HL21 … HT12 … HLT2) -HLT2 #T0 #HT0 #HLT10
+elim (cpr_inv_lift1 … HLT2 … HL21 … HT12) -HLT2 #T0 #HT0 #HLT10
@(IHT1 … HLT10) // -L1 -L2 #H destruct
>(lift_mono … HT0 … HT12) in HT2; -T1 /2 width=1/
qed.
#L2 #L1 #T1 #d #e #H elim H -T1 #T1 #_ #IHT1 #T2 #HL12 #HT21
@csn_intro #T #HLT2 #HT2
elim (lift_total T d e) #T0 #HT0
-lapply (cpr_lift … HL12 … HT21 … HT0 HLT2) -HLT2 #HLT10
+lapply (cpr_lift … HLT2 … HL12 … HT21 … HT0) -HLT2 #HLT10
@(IHT1 … HLT10) // -L1 -L2 #H destruct
>(lift_inj … HT0 … HT21) in HT2; -T1 /2 width=1/
qed.
@csn_intro #X #H #Hi
elim (cpr_inv_lref1 … H) -H
[ #H destruct elim (Hi ?) //
-| -Hi * #K0 #V0 #V1 #HLK0 #HV01 #HV1 #_
+| -Hi * #K0 #V0 #V1 #HLK0 #HV01 #HV1
lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct
lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #HLK
@(csn_lift … HLK HV1) -HLK -HV1
- @(csn_cpr_trans … HV) -HV
- @(cpr_intro … HV01) -HV01 //
+ @(csn_cpr_trans … HV) -HV //
]
qed.
lemma csn_abst: ∀a,L,W. L ⊢ ⬊* W → ∀I,V,T. L. ⓑ{I} V ⊢ ⬊* T → L ⊢ ⬊* ⓛ{a}W. T.
#a #L #W #HW elim HW -W #W #_ #IHW #I #V #T #HT @(csn_ind … HT) -T #T #HT #IHT
@csn_intro #X #H1 #H2
-elim (cpr_inv_abst1 … H1 I V) -H1
+elim (cpr_fwd_abst1 … H1 I V) -H1
#W0 #T0 #HLW0 #HLT0 #H destruct
elim (eq_false_inv_tpair_sn … H2) -H2
[ /3 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/grammar/tstc_tstc.ma".
+include "basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/csn_alt.ma".
+include "basic_2/computation/csn_lift.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma csn_lpr_conf: ∀L1,L2. L1 ⊢ ➡ L2 → ∀T. L1 ⊢ ⬊* T → L2 ⊢ ⬊* T.
+#L1 #L2 #HL12 #T #H @(csn_ind_alt … H) -T #T #_ #IHT
+@csn_intro #T0 #HLT0 #HT0
+@IHT /2 width=2/ -IHT -HT0 /2 width=3 by lpr_cpr_trans/
+qed.
+
+lemma csn_abbr: ∀a,L,V. L ⊢ ⬊* V → ∀T. L. ⓓV ⊢ ⬊* T → L ⊢ ⬊* ⓓ{a}V. T.
+#a #L #V #HV elim HV -V #V #_ #IHV #T #HT @(csn_ind_alt … HT) -T #T #HT #IHT
+@csn_intro #X #H1 #H2
+elim (cpr_inv_abbr1 … H1) -H1 *
+[ #V1 #T1 #HLV1 #HLT1 #H destruct
+ elim (eq_false_inv_tpair_sn … H2) -H2
+ [ #HV1 @IHV // /2 width=1/ -HV1
+ @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
+ | -IHV -HLV1 * #H destruct /3 width=1/
+ ]
+| -IHV -IHT -H2 #T0 #HLT0 #HT0
+ lapply (csn_cpr_trans … HT … HLT0) -T #HLT0
+ lapply (csn_inv_lift … HLT0 … HT0) -T0 /2 width=3/
+]
+qed.
+
+fact csn_appl_beta_aux: ∀a,L,W. L ⊢ ⬊* W → ∀U. L ⊢ ⬊* U →
+ ∀V,T. U = ⓓ{a}V. T → L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
+#a #L #W #H elim H -W #W #_ #IHW #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V #T #H destruct
+lapply (csn_fwd_pair_sn … HVT) #HV
+lapply (csn_fwd_bind_dx … HVT) #HT -HVT
+@csn_intro #X #H #H2
+elim (cpr_inv_appl1 … H) -H *
+[ #V0 #Y #HLV0 #H #H0 destruct
+ elim (cpr_fwd_abst1 … H Abbr V) -H #W0 #T0 #HLW0 #HLT0 #H destruct
+ elim (eq_false_inv_beta … H2) -H2
+ [ -IHVT #HW0 @IHW -IHW [1,5: // |3: skip ] -HLW0 /2 width=1/ -HW0
+ @csn_abbr /2 width=3/ -HV
+ @(csn_lpr_conf (L.ⓓV)) /2 width=1/ -V0 /2 width=3/
+ | -IHW -HLW0 -HV -HT * #H #HVT0 destruct
+ @(IHVT … HVT0) -IHVT -HVT0 // /3 width=1/
+ ]
+| -IHW -IHVT -H2 #b #V0 #W0 #T0 #T1 #HLV0 #HLT01 #H1 #H2 destruct
+ lapply (cpr_lsubr_trans … HLT01 (L.ⓓV) ?) -HLT01 /2 width=1/ #HLT01
+ @csn_abbr /2 width=3/ -HV
+ @(csn_lpr_conf (L. ⓓV)) /2 width=1/ -V0 /2 width=3/
+| -IHW -IHVT -HV -HT -H2 #b #V0 #V1 #W0 #W1 #T0 #T1 #_ #_ #_ #_ #H destruct
+]
+qed-.
+
+(* Basic_1: was: sn3_beta *)
+lemma csn_appl_beta: ∀a,L,W. L ⊢ ⬊* W → ∀V,T. L ⊢ ⬊* ⓓ{a}V. T →
+ L ⊢ ⬊* ⓐV. ⓛ{a}W. T.
+/2 width=3 by csn_appl_beta_aux/ qed.
+
+fact csn_appl_theta_aux: ∀a,L,U. L ⊢ ⬊* U → ∀V1,V2. ⇧[0, 1] V1 ≡ V2 →
+ ∀V,T. U = ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
+#a #L #X #H @(csn_ind_alt … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
+lapply (csn_fwd_pair_sn … HVT) #HV
+lapply (csn_fwd_bind_dx … HVT) -HVT #HVT
+@csn_intro #X #HL #H
+elim (cpr_inv_appl1 … HL) -HL *
+[ -HV #V0 #Y #HLV10 #HL #H0 destruct
+ elim (cpr_inv_abbr1 … HL) -HL *
+ [ #V3 #T3 #HV3 #HLT3 #H0 destruct
+ elim (lift_total V0 0 1) #V4 #HV04
+ elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3))
+ [ -IHVT #H0 destruct
+ elim (eq_false_inv_tpair_sn … H) -H
+ [ -HLV10 -HV3 -HLT3 -HVT
+ >(lift_inj … HV12 … HV04) -V4
+ #H elim H //
+ | * #_ #H elim H //
+ ]
+ | -H -HVT #H
+ lapply (cpr_lift … HLV10 (L. ⓓV) … HV12 … HV04) -HLV10 -HV12 /2 width=1/ #HV24
+ @(IHVT … H … HV04) -IHVT // -H -HV04 /4 width=1/
+ ]
+ | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
+ lapply (csn_cpr_trans … HVT (ⓐV2.T0) ?) /2 width=1/ -T #HVT0
+ lapply (csn_inv_lift L … 1 HVT0 ? ? ?) -HVT0 [ /2 width=4/ |2,3: skip | /2 width=1/ ] -V2 -T0 #HVY
+ @(csn_cpr_trans … HVY) /2 width=1/
+ ]
+| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #T0 #T1 #_ #_ #H destruct
+| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
+ lapply (cpr_lift … HLV10 (L. ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /2 width=1/ #HLV23
+ @csn_abbr /2 width=3/ -HV
+ @(csn_lpr_conf (L. ⓓW0)) /2 width=1/ -W1
+ @(csn_cprs_trans … HVT) -HVT /3 width=1/
+]
+qed-.
+
+lemma csn_appl_theta: ∀a,V1,V2. ⇧[0, 1] V1 ≡ V2 →
+ ∀L,V,T. L ⊢ ⬊* ⓓ{a}V. ⓐV2. T → L ⊢ ⬊* ⓐV1. ⓓ{a}V. T.
+/2 width=5 by csn_appl_theta_aux/ qed.
+
+(* Basic_1: was only: sn3_appl_appl *)
+lemma csn_appl_simple_tstc: ∀L,V. L ⊢ ⬊* V → ∀T1.
+ L ⊢ ⬊* T1 →
+ (∀T2. L ⊢ T1 ➡* T2 → (T1 ≃ T2 → ⊥) → L ⊢ ⬊* ⓐV. T2) →
+ 𝐒⦃T1⦄ → L ⊢ ⬊* ⓐV. T1.
+#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #H @(csn_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
+@csn_intro #X #HL #H
+elim (cpr_inv_appl1_simple … HL ?) -HL //
+#V0 #T0 #HLV0 #HLT10 #H0 destruct
+elim (eq_false_inv_tpair_sn … H) -H
+[ -IHT1 #HV0
+ @(csn_cpr_trans … (ⓐV0.T1)) /2 width=1/ -HLT10
+ @IHV -IHV // -H1T1 -H3T1 /2 width=1/ -HV0
+ #T2 #HLT12 #HT12
+ @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
+ @H2T1 -H2T1 // -HLT12 /2 width=1/
+| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
+ elim (tstc_dec T1 T0) #H2T10
+ [ @IHT1 -IHT1 // /2 width=1/ -H1T10 /2 width=3/ -H3T1
+ #T2 #HLT02 #HT02
+ @H2T1 -H2T1 /2 width=3/ -HLT10 -HLT02 /3 width=3/
+ | -IHT1 -H3T1 -H1T10
+ @H2T1 -H2T1 /2 width=1/
+ ]
+]
+qed.
include "basic_2/computation/acp_cr.ma".
include "basic_2/computation/cprs_tstc_vector.ma".
-include "basic_2/computation/csn_lfpr.ma".
+include "basic_2/computation/csn_lpr.ma".
include "basic_2/computation/csn_vector.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬊* T @ Ts → L ⊢ ⬊* T ∧ L ⊢ ⬊* Ts.
normalize // qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬊* Ⓐ Vs. T → L ⊢ ⬊* Vs ∧ L ⊢ ⬊* T.
+#L #T #Vs elim Vs -Vs /2 width=1/
+#V #Vs #IHVs #HVs
+lapply (csn_fwd_pair_sn … HVs) #HV
+lapply (csn_fwd_flat_dx … HVs) -HVs #HVs
+elim (IHVs HVs) -IHVs -HVs /3 width=1/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/unwind/sstas.ma".
+include "basic_2/unfold/sstas.ma".
include "basic_2/computation/cprs.ma".
(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
#h #g #L #T1 #T #T2 #l #HT1 * /3 width=4/
qed.
+
+lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ →
+ L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+/3 width=3/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma dxprs_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 •*➡*[g] U2 →
+ ∃∃V2,T2. L ⊢ V1 ➡* V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 •*➡*[g] T2 &
+ U2 = ⓛ{a}V2. T2.
+#h #g #a #L #V1 #T1 #U2 * #X #H1 #H2
+elim (sstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
+elim (cprs_fwd_abst1 … H2 Abst V1) -H2 #V2 #T2 #HV12 #HUT2 #H destruct /3 width=5/
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/unwind/sstas_aaa.ma".
+include "basic_2/unfold/sstas_aaa.ma".
include "basic_2/computation/cprs_aaa.ma".
include "basic_2/computation/dxprs.ma".
(* Properties on atomic arity assignment for terms **************************)
lemma dxprs_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U. ⦃h, L⦄ ⊢ T •*➡*[g] U → L ⊢ U ⁝ A.
-#h #g #L #T #A #HT #U * /3 width=5/
+#h #g #L #T #A #HT #U * /3 width=5 by sstas_aaa, aaa_cprs_conf/
qed.
(* *)
(**************************************************************************)
-include "basic_2/unwind/sstas_sstas.ma".
-include "basic_2/computation/cprs_lfprs.ma".
+include "basic_2/unfold/sstas_sstas.ma".
+include "basic_2/computation/lprs_cprs.ma".
include "basic_2/computation/dxprs.ma".
(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
(* *)
(**************************************************************************)
-include "basic_2/unwind/sstas_lift.ma".
+include "basic_2/unfold/sstas_lift.ma".
include "basic_2/computation/cprs_lift.ma".
include "basic_2/computation/dxprs.ma".
(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-(* Advanced inversion lemmas *************************************************)
-
-lemma dxprs_inv_abst1: ∀h,g,a,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓛ{a}V1. T1 •*➡*[g] U2 →
- ∃∃V2,T2. L ⊢ V1 ➡* V2 & ⦃h, L.ⓛV1⦄ ⊢ T1 •*➡*[g] T2 &
- U2 = ⓛ{a}V2. T2.
-#h #g #a #L #V1 #T1 #U2 * #X #H1 #H2
-elim (sstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
-elim (cprs_inv_abst1 Abst V1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct /3 width=5/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ →
- L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
-/3 width=3/ qed.
-
(* Relocation properties ****************************************************)
lemma dxprs_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K → ∀T1,U1. ⇧[d, e] T1 ≡ U1 →
∃∃T2. ⇧[d, e] T2 ≡ U2 & ⦃h, K⦄ ⊢ T1 •*➡*[g] T2.
#L #K #d #e #HLK #T1 #U1 #HTU1 #h #g #U2 * #U #HU1 #HU2
elim (sstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HT1 #HTU
-elim (cprs_inv_lift1 … HLK … HTU … HU2) -U -L /3 width=5/
+elim (cprs_inv_lift1 … HU2 … HLK … HTU) -U -L /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/sstas_lpss.ma".
+include "basic_2/computation/cprs_lpss.ma".
+include "basic_2/computation/dxprs.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
+
+(* Properties about sn parallel substitution for local environments *********)
+
+lemma dxprs_lpss_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 → ∀L2. L1 ⊢ ▶* L2 →
+ ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L1 ⊢ U1 ▶* U2.
+#h #g #L1 #T #U1 * #U #HTU #HU1 #L2 #HL12
+elim (sstas_lpss_conf … HTU … HL12) -HTU #U0 #HTU0 #HU0
+elim (cprs_cpss_conf … HU1 … HU0) -U #U #HU1 #HU0
+elim (cprs_lpss_conf_sn … HU0 … HL12) -HU0 -HL12 #U2 #HU2 #HU02
+lapply (cpss_trans … HU1 … HU2) -U /3 width=3/
+qed-.
+
+lemma dxprs_cpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*➡*[g] U1 → ∀T2. L ⊢ T1 ▶* T2 →
+ ∃∃U2. ⦃h, L⦄ ⊢ T2 •*➡*[g] U2 & L ⊢ U1 ▶* U2.
+#h #g #L #T1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12
+elim (sstas_tpss_conf … HTW1 … HT12) -T1 #W2 #HTW2 #HW12
+elim (cprs_cpss_conf … HWU1 … HW12) -W1 /3 width=3/
+qed-.
+
+lemma dxprs_lpss_cpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 →
+ ∀L2. L1 ⊢ ▶* L2 → ∀T2. L1 ⊢ T1 ▶* T2 →
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L1 ⊢ U1 ▶* U2.
+#h #g #L1 #T1 #U1 #HTU1 #L2 #HL12 #T2 #HT12
+elim (dxprs_cpss_conf … HTU1 … HT12) -T1 #U2 #HTU2 #HU12
+elim (dxprs_lpss_conf … HTU2 … HL12) -HTU2 -HL12 #U #HT2U #HU2
+lapply (cpss_trans … HU12 … HU2) -U2 /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/unwind/sstas_ltpss_dx.ma".
-include "basic_2/computation/cprs_ltpss_dx.ma".
-include "basic_2/computation/dxprs.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-
-(* Properties about dx parallel unfold **************************************)
-
-lemma dxprs_ltpss_dx_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 →
- ∀L2,d,e. L1 ▶* [d, e] L2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2.
-#h #g #L1 #T #U1 * #U #HTU #HU1 #L2 #d #e #HL12
-elim (sstas_ltpss_dx_conf … HTU … HL12) -HTU #U0 #HTU0 #HU0
-elim (cprs_ltpss_dx_conf … HU1 … HL12) -L1 #U2 #HU2 #HU12
-elim (cprs_tpss_conf … HU2 … HU0) -U #U #HU2 #HU0
-lapply (tpss_trans_eq … HU12 HU2) -U2 /3 width=3/
-qed-.
-
-lemma dxprs_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*➡*[g] U1 →
- ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 →
- ∃∃U2. ⦃h, L⦄ ⊢ T2 •*➡*[g] U2 & L ⊢ U1 ▶* [d, e] U2.
-#h #g #L #T1 #U1 * #W1 #HTW1 #HWU1 #T2 #d #e #HT12
-elim (sstas_tpss_conf … HTW1 … HT12) -T1 #W2 #HTW2 #HW12
-elim (cprs_tpss_conf … HWU1 … HW12) -W1 /3 width=3/
-qed-.
-
-lemma dxprs_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 →
- ∀L2,d,e. L1 ▶* [d, e] L2 →
- ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 &
- L2 ⊢ U1 ▶* [d, e] U2.
-#h #g #L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12
-elim (dxprs_ltpss_dx_conf … HTU1 … HL12) -L1 #U #HT1U #HU1
-elim (dxprs_tpss_conf … HT1U … HT12) -T1 #U2 #HTU2 #HU2
-lapply (tpss_trans_eq … HU1 HU2) -U /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/ltpss_sn_alt.ma".
-include "basic_2/computation/dxprs_ltpss_dx.ma".
-
-(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
-
-(* Properties about sn parallel unfold **************************************)
-
-lemma dxprs_ltpss_sn_conf: ∀h,g,L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 →
- ∀T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 →
- ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L1 ⊢ U1 ▶* [d, e] U2.
-#h #g #L1 #L2 #d #e #H
-lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 [ /2 width=3/ ]
-#L #L2 #HL1 #HL2 #IHL1 #T #U1 #HTU1
-lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1
-lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12
-elim (IHL1 … HTU1) -IHL1 -HTU1 #U #HTU #HU1
-elim (dxprs_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #HTU2 #HU2
-lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2
-lapply (tpss_trans_eq … HU1 HU2) -U /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/reducibility/fpr.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
-
-definition fprs: bi_relation lenv term ≝ bi_TC … fpr.
-
-interpretation "context-free parallel computation (closure)"
- 'FocalizedPRedStar L1 T1 L2 T2 = (fprs L1 T1 L2 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma fprs_ind: ∀L1,T1. ∀R:relation2 lenv term. R L1 T1 →
- (∀L,L2,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ → R L T → R L2 T2) →
- ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L2 T2.
-/3 width=7 by bi_TC_star_ind/ qed-.
-
-lemma fprs_ind_dx: ∀L2,T2. ∀R:relation2 lenv term. R L2 T2 →
- (∀L1,L,T1,T. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ → R L T → R L1 T1) →
- ∀L1,T1. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → R L1 T1.
-/3 width=7 by bi_TC_star_ind_dx/ qed-.
-
-(* Basic properties *********************************************************)
-
-lemma fpr_fprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡ ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
-/2 width=1/ qed.
-
-lemma fprs_refl: bi_reflexive … fprs.
-/2 width=1/ qed.
-
-lemma fprs_strap1: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡* ⦃L, T⦄ → ⦃L, T⦄ ➡ ⦃L2, T2⦄ →
- ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
-/2 width=4/ qed.
-
-lemma fprs_strap2: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ➡ ⦃L, T⦄ → ⦃L, T⦄ ➡* ⦃L2, T2⦄ →
- ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
-/2 width=4/ qed.
+++ /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/cfpr_aaa.ma".
-include "basic_2/computation/fprs.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
-
-(* Properties about atomic arity assignment on terms ************************)
-
-lemma aaa_fprs_conf: ∀L1,T1,A. L1 ⊢ T1 ⁝ A →
- ∀L2,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L2 ⊢ T2 ⁝ A.
-#L1 #T1 #A #HT1 #L2 #T2 #HLT12
-@(bi_TC_Conf3 … HT1 ?? HLT12) /2 width=4/
-qed.
+++ /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/fpr_cpr.ma".
-include "basic_2/computation/cprs_lfprs.ma".
-include "basic_2/computation/lfprs_ltprs.ma".
-include "basic_2/computation/lfprs_fprs.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma fprs_flat_dx_tpr: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ∀V1,V2. V1 ➡ V2 →
- ∀I. ⦃L1, ⓕ{I}V1.T1⦄ ➡* ⦃L2, ⓕ{I}V2.T2⦄.
-#L1 #L2 #T1 #T2 #HT12 @(fprs_ind … HT12) -L2 -T2 /3 width=1/
-#L #L2 #T #T2 #_ #HT2 #IHT2 #V1 #V2 #HV12 #I
-lapply (IHT2 … HV12 I) -IHT2 -HV12 /3 width=6/
-qed.
-
-lemma fprs_bind2_minus: ∀I,L1,L2,V1,T1,U2. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L2, U2⦄ →
- ∃∃V2,T2. ⦃L1.ⓑ{I}V1, T1⦄ ➡* ⦃L2.ⓑ{I}V2, T2⦄ &
- U2 = -ⓑ{I}V2.T2.
-#I #L1 #L2 #V1 #T1 #U2 #H @(fprs_ind … H) -L2 -U2 /2 width=4/
-#L #L2 #U #U2 #_ #HU2 * #V #T #HT1 #H destruct
-elim (fpr_bind2_minus … HU2) -HU2 /3 width=4/
-qed-.
-
-lemma fprs_lift: ∀K1,K2,T1,T2. ⦃K1, T1⦄ ➡* ⦃K2, T2⦄ →
- ∀d,e,L1. ⇩[d, e] L1 ≡ K1 →
- ∀U1,U2. ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
- ∃∃L2. ⦃L1, U1⦄ ➡* ⦃L2, U2⦄ & ⇩[d, e] L2 ≡ K2.
-#K1 #K2 #T1 #T2 #HT12 @(fprs_ind … HT12) -K2 -T2
-[ #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2
- >(lift_mono … HTU2 … HTU1) -U2 /2 width=3/
-| #K #K2 #T #T2 #_ #HT2 #IHT1 #d #e #L1 #HLK1 #U1 #U2 #HTU1 #HTU2
- elim (lift_total T d e) #U #HTU
- elim (IHT1 … HLK1 … HTU1 HTU) -K1 -T1 #L #HU1 #HKL
- elim (fpr_lift … HT2 … HKL … HTU HTU2) -K -T -T2 /3 width=4/
-]
-qed-.
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma fprs_inv_pair1: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
- ∃∃K2,V2. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ &
- ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄ &
- L2 = K2.ⓑ{I}V2.
-#I #K1 #L2 #V1 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 /2 width=5/
-#L #L2 #T #T2 #_ #HT2 * #K #V #HV1 #HT1 #H destruct
-elim (fpr_inv_pair1 … HT2) -HT2 #K2 #V2 #HV2 #HT2 #H destruct /3 width=5/
-qed-.
-
-lemma fprs_inv_pair3: ∀I,L1,K2,V2,T1,T2. ⦃L1, T1⦄ ➡* ⦃K2.ⓑ{I}V2, T2⦄ →
- ∃∃K1,V1. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ &
- ⦃K1, -ⓑ{I}V1.T1⦄ ➡* ⦃K2, -ⓑ{I}V2.T2⦄ &
- L1 = K1.ⓑ{I}V1.
-#I2 #L1 #K2 #V2 #T1 #T2 #H @(fprs_ind_dx … H) -L1 -T1 /2 width=5/
-#L1 #L #T1 #T #HT1 #_ * #K #V #HV2 #HT2 #H destruct
-elim (fpr_inv_pair3 … HT1) -HT1 #K1 #V1 #HV1 #HT1 #H destruct /3 width=5/
-qed-.
-
-(* Advanced forward lemmas **************************************************)
-
-lemma fprs_fwd_bind2_minus: ∀I,L1,L,V1,T1,T. ⦃L1, -ⓑ{I}V1.T1⦄ ➡* ⦃L, T⦄ → ∀b.
- ∃∃V2,T2. ⦃L1, ⓑ{b,I}V1.T1⦄ ➡* ⦃L, ⓑ{b,I}V2.T2⦄ &
- T = -ⓑ{I}V2.T2.
-#I #L1 #L #V1 #T1 #T #H1 #b @(fprs_ind … H1) -L -T /2 width=4/
-#L0 #L #T0 #T #_ #H0 * #W1 #U1 #HTU1 #H destruct
-elim (fpr_fwd_bind2_minus … H0 b) -H0 /3 width=4/
-qed-.
-
-lemma fprs_fwd_pair1_full: ∀I,K1,L2,V1,T1,T2. ⦃K1.ⓑ{I}V1, T1⦄ ➡* ⦃L2, T2⦄ →
- ∀b. ∃∃K2,V2. ⦃K1, V1⦄ ➡* ⦃K2, V2⦄ &
- ⦃K1, ⓑ{b,I}V1.T1⦄ ➡* ⦃K2, ⓑ{b,I}V2.T2⦄ &
- L2 = K2.ⓑ{I}V2.
-#I #K1 #L2 #V1 #T1 #T2 #H #b
-elim (fprs_inv_pair1 … H) -H #K2 #V2 #HV12 #HT12 #H destruct
-elim (fprs_fwd_bind2_minus … HT12 b) -HT12 #W1 #U1 #HTU1 #H destruct /2 width=5/
-qed-.
-
-lemma fprs_fwd_abst2: ∀a,L1,L2,V1,T1,U2. ⦃L1, ⓛ{a}V1.T1⦄ ➡* ⦃L2, U2⦄ → ∀b,I,W.
- ∃∃V2,T2. ⦃L1, ⓑ{b,I}W.T1⦄ ➡* ⦃L2, ⓑ{b,I}W.T2⦄ &
- U2 = ⓛ{a}V2.T2.
-#a #L1 #L2 #V1 #T1 #U2 #H #b #I #W @(fprs_ind … H) -L2 -U2 /2 width=4/
-#L #L2 #U #U2 #_ #H2 * #V #T #HT1 #H destruct
-elim (fpr_fwd_abst2 … H2 b I W) -H2 /3 width=4/
-qed-.
-
-(* Properties on context-sensitive parallel computation for terms ***********)
-
-lemma cprs_fprs: ∀L,T1,T2. L ⊢ T1 ➡* T2 → ⦃L, T1⦄ ➡* ⦃L, T2⦄.
-#L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4/
-qed.
-
-(* Forward lemmas on context-sensitive parallel computation for terms *******)
-
-lemma fprs_fwd_cprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → L1 ⊢ T1 ➡* T2.
-#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 //
-#L #L2 #T #T2 #H1 #H2 #IH1
-elim (fpr_inv_all … H2) -H2 #L0 #HL0 #HT2 #_ -L2
-lapply (lfprs_cpr_trans L1 … HT2) -HT2 /3 width=3/
-qed-.
-(*
-(* Advanced properties ******************************************************)
-
-lamma fpr_bind_sn: ∀L1,L2,V1,V2. ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ → ∀T1,T2. T1 ➡ T2 →
- ∀a,I. ⦃L1, ⓑ{a,I}V1.T1⦄ ➡ ⦃L2, ⓑ{a,I}V2.T2⦄.
-#L1 #L2 #V1 #V2 #H #T1 #T2 #HT12 #a #I
-elim (fpr_inv_all … H) /3 width=4/
-qed.
-
-(* Advanced forward lemmas **************************************************)
-
-lamma fpr_fwd_shift_bind_minus: ∀I1,I2,L1,L2,V1,V2,T1,T2.
- ⦃L1, -ⓑ{I1}V1.T1⦄ ➡ ⦃L2, -ⓑ{I2}V2.T2⦄ →
- ⦃L1, V1⦄ ➡ ⦃L2, V2⦄ ∧ I1 = I2.
-* #I2 #L1 #L2 #V1 #V2 #T1 #T2 #H
-elim (fpr_inv_all … H) -H #L #HL1 #H #HL2
-[ elim (cpr_inv_abbr1 … H) -H *
- [ #V #V0 #T #HV1 #HV0 #_ #H destruct /4 width=4/
- | #T #_ #_ #H destruct
- ]
-| elim (cpr_inv_abst1 … H Abst V2) -H
- #V #T #HV1 #_ #H destruct /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/reducibility/fpr_fpr.ma".
-include "basic_2/computation/fprs.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON CLOSURES ****************************)
-
-(* Advanced properties ******************************************************)
-
-lemma fprs_strip: ∀L0,L1,T0,T1. ⦃L0, T0⦄ ➡ ⦃L1, T1⦄ →
- ∀L2,T2. ⦃L0, T0⦄ ➡* ⦃L2, T2⦄ →
- ∃∃L,T. ⦃L1, T1⦄ ➡* ⦃L, T⦄ & ⦃L2, T2⦄ ➡ ⦃L, T⦄.
-#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8
-/2 width=4/ qed.
-
-(* Main propertis ***********************************************************)
-
-theorem fprs_conf: bi_confluent … fprs.
-/2 width=4/ qed.
-
-theorem fprs_trans: bi_transitive … fprs.
-/2 width=4/ qed.
+++ /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/lfpr.ma".
-
-(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
-
-definition lfprs: relation lenv ≝ TC … lfpr.
-
-interpretation
- "focalized parallel computation (environment)"
- 'FocalizedPRedStar L1 L2 = (lfprs L1 L2).
-
-(* Basic eliminators ********************************************************)
-
-lemma lfprs_ind: ∀L1. ∀R:predicate lenv. R L1 →
- (∀L,L2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L⦄ ➡ ⦃L2⦄ → R L → R L2) →
- ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ → R L2.
-#L1 #R #HL1 #IHL1 #L2 #HL12
-@(TC_star_ind … HL1 IHL1 … HL12) //
-qed-.
-
-lemma lfprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 →
- (∀L1,L. ⦃L1⦄ ➡ ⦃L⦄ → ⦃L⦄ ➡* ⦃L2⦄ → R L → R L1) →
- ∀L1. ⦃L1⦄ ➡* ⦃L2⦄ → R L1.
-#L2 #R #HL2 #IHL2 #L1 #HL12
-@(TC_star_ind_dx … HL2 IHL2 … HL12) //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma lfpr_lfprs: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
-/2 width=1/ qed.
-
-lemma lfprs_refl: ∀L. ⦃L⦄ ➡* ⦃L⦄.
-/2 width=1/ qed.
-
-lemma lfprs_strap1: ∀L1,L,L2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L⦄ ➡ ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
-/2 width=3/ qed.
-
-lemma lfprs_strap2: ∀L1,L,L2. ⦃L1⦄ ➡ ⦃L⦄ → ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
-/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/reducibility/lfpr_aaa.ma".
-include "basic_2/computation/lfprs.ma".
-
-(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
-
-(* Properties about atomic arity assignment on terms ************************)
-
-lemma aaa_lfprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. ⦃L1⦄ ➡* ⦃L2⦄ → L2 ⊢ T ⁝ A.
-#L1 #T #A #HT #L2 #HL12
-@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /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/reducibility/lfpr_cpr.ma".
-include "basic_2/computation/cprs.ma".
-include "basic_2/computation/lfprs.ma".
-
-(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
-
-(* Advanced properties ******************************************************)
-
-lemma lfprs_pair_dx: ∀I,L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
- ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄.
-#I #L1 #L2 #HL12 #V1 #V2 #H @(cprs_ind … H) -V2
-/3 width=1/ /3 width=5/
-qed.
-(*
-lamma lfprs_cprs_conf: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L2⦄ → L1 ⊢ T1 ➡* T2 → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
-*)
+++ /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/lfpr_fpr.ma".
-include "basic_2/computation/fprs_fprs.ma".
-include "basic_2/computation/lfprs.ma".
-
-(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
-
-(* Inversion lemmas on context-free parallel reduction for closures *********)
-
-lemma lfprs_inv_fprs: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀T. ⦃L1, T⦄ ➡* ⦃L2, T⦄.
-#L1 #L2 #H @(lfprs_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL1 #T
-lapply (lfpr_inv_fpr … HL2 T) -HL2 /3 width=4/
-qed-.
-
-(* Properties on context-free parallel computation for closures *************)
-
-lemma fprs_lfprs: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
-#L1 #L2 #T1 #T2 #H @(fprs_ind … H) -L2 -T2 // /3 width=5/
-qed.
-
-lemma lfprs_fprs_trans: ∀L1,L,L2,T1,T2. ⦃L1⦄ ➡* ⦃L⦄ → ⦃L, T1⦄ ➡* ⦃L2, T2⦄ → ⦃L1, T1⦄ ➡* ⦃L2, T2⦄.
-#L1 #L #L2 #T1 #T2 #HL1 #HL2
-lapply (lfprs_inv_fprs … HL1 T1) -HL1 /2 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/reducibility/lfpr_lfpr.ma".
-include "basic_2/computation/lfprs_cprs.ma".
-
-(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
-
-(* Advanced properties ******************************************************)
-
-lemma lfprs_strip: ∀L,L1. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ➡ ⦃L2⦄ →
- ∃∃L0. ⦃L1⦄ ➡ ⦃L0⦄ & ⦃L2⦄ ➡* ⦃L0⦄.
-/3 width=3/ qed.
-
-(* Main properties **********************************************************)
-
-theorem lfprs_conf: ∀L,L1. ⦃L⦄ ➡* ⦃L1⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ →
- ∃∃L0. ⦃L1⦄ ➡* ⦃L0⦄ & ⦃L2⦄ ➡* ⦃L0⦄.
-/3 width=3/ qed.
-
-theorem lfprs_trans: ∀L1,L. ⦃L1⦄ ➡* ⦃L⦄ → ∀L2. ⦃L⦄ ➡* ⦃L2⦄ → ⦃L1⦄ ➡* ⦃L2⦄.
-/2 width=3/ qed.
-
-lemma lfprs_pair: ∀L1,L2. ⦃L1⦄ ➡* ⦃L2⦄ → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
- ∀I. ⦃L1. ⓑ{I} V1⦄ ➡* ⦃L2. ⓑ{I} V2⦄.
-#L1 #L2 #H @(lfprs_ind … H) -L2 /2 width=1/
-#L #L2 #_ #HL2 #IHL1 #V1 #V2 #HV12 #I
-@(lfprs_trans … (L.ⓑ{I}V1)) /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/computation/ltprs.ma".
-include "basic_2/computation/lfprs.ma".
-
-(* FOCALIZED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *********************)
-
-(* Properties on context-free parallel computation for local environments ***)
-
-lemma ltprs_lfprs: ∀L1,L2. L1 ➡* L2 → ⦃L1⦄ ➡* ⦃L2⦄.
-/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/grammar/lpx_sn_tc.ma".
+include "basic_2/reduction/lpr.ma".
+
+(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+
+definition lprs: relation lenv ≝ TC … lpr.
+
+interpretation "parallel computation (local environment, sn variant)"
+ 'PRedSnStar L1 L2 = (lprs L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma lprs_ind: ∀L1. ∀R:predicate lenv. R L1 →
+ (∀L,L2. L1 ⊢ ➡* L → L ⊢ ➡ L2 → R L → R L2) →
+ ∀L2. L1 ⊢ ➡* L2 → R L2.
+#L1 #R #HL1 #IHL1 #L2 #HL12
+@(TC_star_ind … HL1 IHL1 … HL12) //
+qed-.
+
+lemma lprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 →
+ (∀L1,L. L1 ⊢ ➡ L → L ⊢ ➡* L2 → R L → R L1) →
+ ∀L1. L1 ⊢ ➡* L2 → R L1.
+#L2 #R #HL2 #IHL2 #L1 #HL12
+@(TC_star_ind_dx … HL2 IHL2 … HL12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lpr_lprs: ∀L1,L2. L1 ⊢ ➡ L2 → L1 ⊢ ➡* L2.
+/2 width=1/ qed.
+
+lemma lprs_refl: ∀L. L ⊢ ➡* L.
+/2 width=1/ qed.
+
+lemma lprs_strap1: ∀L1,L,L2. L1 ⊢ ➡* L → L ⊢ ➡ L2 → L1 ⊢ ➡* L2.
+/2 width=3/ qed.
+
+lemma lprs_strap2: ∀L1,L,L2. L1 ⊢ ➡ L → L ⊢ ➡* L2 → L1 ⊢ ➡* L2.
+/2 width=3/ qed.
+
+lemma lprs_pair_refl: ∀L1,L2. L1 ⊢ ➡* L2 → ∀I,V. L1. ⓑ{I} V ⊢ ➡* L2. ⓑ{I} V.
+/2 width=1 by TC_lpx_sn_pair_refl/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lprs_inv_atom1: ∀L2. ⋆ ⊢ ➡* L2 → L2 = ⋆.
+/2 width=2 by TC_lpx_sn_inv_atom1/ qed-.
+
+lemma lprs_inv_atom2: ∀L1. L1 ⊢ ➡* ⋆ → L1 = ⋆.
+/2 width=2 by TC_lpx_sn_inv_atom2/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lprs_fwd_length: ∀L1,L2. L1 ⊢ ➡* L2 → |L1| = |L2|.
+/2 width=2 by TC_lpx_sn_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 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reduction/lpr_aaa.ma".
+include "basic_2/computation/lprs.ma".
+
+(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+
+(* Properties about atomic arity assignment on terms ************************)
+
+lemma aaa_lprs_conf: ∀L1,T,A. L1 ⊢ T ⁝ A → ∀L2. L1 ⊢ ➡* L2 → L2 ⊢ T ⁝ A.
+#L1 #T #A #HT #L2 #HL12
+@(TC_Conf3 … (λL,A. L ⊢ T ⁝ A) … HT ? HL12) /2 width=3 by aaa_lpr_conf/
+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/computation/cprs_cprs.ma".
+include "basic_2/computation/lprs.ma".
+
+(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+
+(* alternative definition *)
+definition lprsa: relation lenv ≝ lpx_sn … cprs.
+
+interpretation "parallel computation (local environment, sn variant) alternative"
+ 'PRedSnStarAlt L1 L2 = (lprsa L1 L2).
+
+(* Main properties on the alternative definition **********************************)
+
+theorem lprsa_lprs: ∀L1,L2. L1 ⊢ ➡➡* L2 → L1 ⊢ ➡* L2.
+/2 width=1 by lpx_sn_LTC_TC_lpx_sn/ qed-.
+
+(* Main inversion lemmas on the alternative definition ****************************)
+
+theorem lprs_inv_lprsa: ∀L1,L2. L1 ⊢ ➡* L2 → L1 ⊢ ➡➡* L2.
+/3 width=3 by TC_lpx_sn_inv_lpx_sn_LTC, lpr_cprs_trans/ qed-.
+
+(* Alternative eliminators ********************************************************)
+
+lemma lprs_ind_alt: ∀R:relation lenv.
+ R (⋆) (⋆) → (
+ ∀I,K1,K2,V1,V2.
+ K1 ⊢ ➡* K2 → K1 ⊢ V1 ➡* V2 →
+ R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2)
+ ) →
+ ∀L1,L2. L1 ⊢ ➡* L2 → R L1 L2.
+/3 width=4 by TC_lpx_sn_ind, lpr_cprs_trans/ 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/computation/cprs_cprs.ma".
+include "basic_2/computation/lprs.ma".
+
+(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma lprs_pair: ∀I,L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L1 ⊢ V1 ➡* V2 →
+ L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2.
+/2 width=1 by TC_lpx_sn_pair/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma lprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ⊢ ➡* L2 →
+ ∃∃K2,V2. K1 ⊢ ➡* K2 & K1 ⊢ V1 ➡* V2 & L2 = K2. ⓑ{I} V2.
+/3 width=3 by TC_lpx_sn_inv_pair1, lpr_cprs_trans/ qed-.
+
+lemma lprs_inv_pair2: ∀I,L1,K2,V2. L1 ⊢ ➡* K2. ⓑ{I} V2 →
+ ∃∃K1,V1. K1 ⊢ ➡* K2 & K1 ⊢ V1 ➡* V2 & L1 = K1. ⓑ{I} V1.
+/3 width=3 by TC_lpx_sn_inv_pair2, lpr_cprs_trans/ qed-.
+
+(* Properties on context-sensitive parallel computation for terms ***********)
+
+lemma lprs_cpr_trans: s_r_trans … cpr lprs.
+/3 width=5 by s_r_trans_TC2, lpr_cprs_trans/ qed-.
+
+(* Basic_1: was just: pr3_pr3_pr3_t *)
+lemma lprs_cprs_trans: s_rs_trans … cpr lprs.
+/3 width=5 by s_r_trans_TC1, lprs_cpr_trans/ qed-.
+
+lemma lprs_cprs_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡* L1 →
+ ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
+#L0 #T0 #T1 #HT01 #L1 #H elim H -L1
+[ #L1 #HL01
+ elim (cprs_lpr_conf_dx … HT01 … HL01) -L0 /2 width=3/
+| #L #L1 #_ #HL1 * #T #HT1 #HT0 -L0
+ elim (cprs_lpr_conf_dx … HT1 … HL1) -HT1 #T2 #HT2 #HT12
+ elim (cprs_lpr_conf_dx … HT0 … HL1) -L #T3 #HT3 #HT03
+ elim (cprs_conf … HT2 … HT3) -T #T #HT2 #HT3
+ lapply (cprs_trans … HT03 … HT3) -T3
+ lapply (cprs_trans … HT12 … HT2) -T2 /2 width=3/
+]
+qed-.
+
+lemma lprs_cpr_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡* L1 →
+ ∃∃T. L1 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
+/3 width=3 by lprs_cprs_conf_dx, cpr_cprs/ qed-.
+
+lemma lprs_cprs_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ➡* L1 →
+ ∃∃T. L0 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
+#L0 #T0 #T1 #HT01 #L1 #HL01
+elim (lprs_cprs_conf_dx … HT01 … HL01) -HT01 #T #HT1
+lapply (lprs_cprs_trans … HT1 … HL01) -HT1 /2 width=3/
+qed-.
+
+lemma lprs_cpr_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡ T1 → ∀L1. L0 ⊢ ➡* L1 →
+ ∃∃T. L0 ⊢ T1 ➡* T & L1 ⊢ T0 ➡* T.
+/3 width=3 by lprs_cprs_conf_sn, cpr_cprs/ qed-.
+
+lemma cprs_bind2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 →
+ ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2.
+#L #V1 #V2 #HV12 #I #T1 #T2 #HT12
+lapply (lprs_cprs_trans … HT12 (L.ⓑ{I}V1) ?) /2 width=1/
+qed.
+
+(* Inversion lemmas on context-sensitive parallel computation for terms *****)
+
+(* Basic_1: was pr3_gen_abbr *)
+lemma cprs_inv_abbr1: ∀a,L,V1,T1,U2. L ⊢ ⓓ{a}V1.T1 ➡* U2 → (
+ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓓV1 ⊢ T1 ➡* T2 &
+ U2 = ⓓ{a}V2.T2
+ ) ∨
+ ∃∃T2. L. ⓓV1 ⊢ T1 ➡* T2 & ⇧[0, 1] U2 ≡ T2 & a = true.
+#a #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpr_inv_abbr1 … HU02) -HU02 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct
+ lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) /2 width=1/ -HT02 #HT02
+ lapply (cprs_strap1 … HV10 … HV02) -V0
+ lapply (cprs_trans … HT10 … HT02) -T0 /3 width=5/
+ | #T2 #HT02 #HUT2
+ lapply (lprs_cpr_trans … HT02 (L.ⓓV1) ?) -HT02 /2 width=1/ -V0 #HT02
+ lapply (cprs_trans … HT10 … HT02) -T0 /3 width=3/
+ ]
+| #U1 #HTU1 #HU01
+ elim (lift_total U2 0 1) #U #HU2
+ lapply (cpr_lift … HU02 (L.ⓓV1) … HU01 … HU2) -U0 /2 width=1/ /4 width=3/
+]
+qed-.
+
+(* More advanced properties *************************************************)
+
+lemma lprs_pair2: ∀I,L1,L2. L1 ⊢ ➡* L2 → ∀V1,V2. L2 ⊢ V1 ➡* V2 →
+ L1. ⓑ{I} V1 ⊢ ➡* L2. ⓑ{I} V2.
+/3 width=3 by lprs_pair, lprs_cprs_trans/ 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/reduction/lpr_ldrop.ma".
+include "basic_2/computation/lprs.ma".
+
+(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+
+(* Properies on local environment slicing ***********************************)
+
+lemma lprs_ldrop_conf: dropable_sn lprs.
+/3 width=3 by dropable_sn_TC, lpr_ldrop_conf/ qed-.
+
+lemma ldrop_lprs_trans: dedropable_sn lprs.
+/3 width=3 by dedropable_sn_TC, ldrop_lpr_trans/ qed-.
+
+lemma lprs_ldrop_trans_O1: dropable_dx lprs.
+/3 width=3 by dropable_dx_TC, lpr_ldrop_trans_O1/ 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/reduction/lpr_lpr.ma".
+include "basic_2/computation/lprs.ma".
+
+(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+
+(* Advanced properties ******************************************************)
+
+lemma lprs_strip: confluent2 … lprs lpr.
+/3 width=3 by TC_strip1, lpr_conf/ qed-.
+
+(* Main properties **********************************************************)
+
+theorem lprs_conf: confluent2 … lprs lprs.
+/3 width=3 by TC_confluent2, lpr_conf/ qed-.
+
+theorem lfprs_trans: Transitive … lprs.
+/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/reduction/lpr_lpss.ma".
+include "basic_2/computation/lprs.ma".
+
+(* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************)
+
+(* Properties on sn parallel substitution on local environments *************)
+
+lemma lprs_lpss_conf: confluent2 … lprs lpss.
+/3 width=3 by TC_strip1, lpr_lpss_conf/
+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.ma".
-include "basic_2/computation/tprs.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
-
-definition ltprs: relation lenv ≝ TC … ltpr.
-
-interpretation
- "context-free parallel computation (environment)"
- 'PRedStar L1 L2 = (ltprs L1 L2).
-
-(* Basic eliminators ********************************************************)
-
-lemma ltprs_ind: ∀L1. ∀R:predicate lenv. R L1 →
- (∀L,L2. L1 ➡* L → L ➡ L2 → R L → R L2) →
- ∀L2. L1 ➡* L2 → R L2.
-#L1 #R #HL1 #IHL1 #L2 #HL12
-@(TC_star_ind … HL1 IHL1 … HL12) //
-qed-.
-
-lemma ltprs_ind_dx: ∀L2. ∀R:predicate lenv. R L2 →
- (∀L1,L. L1 ➡ L → L ➡* L2 → R L → R L1) →
- ∀L1. L1 ➡* L2 → R L1.
-#L2 #R #HL2 #IHL2 #L1 #HL12
-@(TC_star_ind_dx … HL2 IHL2 … HL12) //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma ltprs_refl: reflexive … ltprs.
-/2 width=1/ qed.
-
-lemma ltpr_ltprs: ∀L1,L2. L1 ➡ L2 → L1 ➡* L2.
-/2 width=1/ qed.
-
-lemma ltprs_strap1: ∀L1,L,L2. L1 ➡* L → L ➡ L2 → L1 ➡* L2.
-/2 width=3/ qed.
-
-lemma ltprs_strap2: ∀L1,L,L2. L1 ➡ L → L ➡* L2 → L1 ➡* L2.
-/2 width=3/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma ltprs_inv_atom1: ∀L2. ⋆ ➡* L2 → L2 = ⋆.
-#L2 #H @(ltprs_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL1 destruct
->(ltpr_inv_atom1 … HL2) -L2 //
-qed-.
-
-lemma ltprs_inv_pair1: ∀I,K1,L2,V1. K1. ⓑ{I} V1 ➡* L2 →
- ∃∃K2,V2. K1 ➡* K2 & V1 ➡* V2 & L2 = K2. ⓑ{I} V2.
-#I #K1 #L2 #V1 #H @(ltprs_ind … H) -L2 /2 width=5/
-#L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
-elim (ltpr_inv_pair1 … HL2) -HL2 #K2 #V2 #HK2 #HV2 #H destruct /3 width=5/
-qed-.
-
-lemma ltprs_inv_atom2: ∀L1. L1 ➡* ⋆ → L1 = ⋆.
-#L1 #H @(ltprs_ind_dx … H) -L1 //
-#L1 #L #HL1 #_ #IHL2 destruct
->(ltpr_inv_atom2 … HL1) -L1 //
-qed-.
-
-lemma ltprs_inv_pair2: ∀I,L1,K2,V2. L1 ➡* K2. ⓑ{I} V2 →
- ∃∃K1,V1. K1 ➡* K2 & V1 ➡* V2 & L1 = K1. ⓑ{I} V1.
-#I #L1 #K2 #V2 #H @(ltprs_ind_dx … H) -L1 /2 width=5/
-#L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
-elim (ltpr_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct /3 width=5/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma ltprs_fwd_length: ∀L1,L2. L1 ➡* L2 → |L1| = |L2|.
-#L1 #L2 #H @(ltprs_ind … H) -L2 //
-#L #L2 #_ #HL2 #IHL1
->IHL1 -L1 >(ltpr_fwd_length … 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/computation/ltprs.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
-
-(* alternative definition of ltprs *)
-definition ltprsa: relation lenv ≝ lpx tprs.
-
-interpretation
- "context-free parallel computation (environment) alternative"
- 'PRedStarAlt L1 L2 = (ltprsa L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma ltprs_ltprsa: ∀L1,L2. L1 ➡* L2 → L1 ➡➡* L2.
-/2 width=1/ qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma ltprsa_ltprs: ∀L1,L2. L1 ➡➡* L2 → L1 ➡* L2.
-/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/reducibility/ltpr_ldrop.ma".
-include "basic_2/computation/ltprs.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
-
-lemma ltprs_ldrop_conf: dropable_sn ltprs.
-/2 width=3/ qed.
-
-lemma ldrop_ltprs_trans: dedropable_sn ltprs.
-/2 width=3/ qed.
-
-lemma ltprs_ldrop_trans_O1: dropable_dx ltprs.
-/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/reducibility/ltpr_ltpr.ma".
-include "basic_2/computation/ltprs.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ******************)
-
-(* Advanced properties ******************************************************)
-
-lemma ltprs_strip: ∀L1. ∀L:lenv. L ➡* L1 → ∀L2. L ➡ L2 →
- ∃∃L0. L1 ➡ L0 & L2 ➡* L0.
-/3 width=3/ qed.
-
-(* Main properties **********************************************************)
-
-theorem ltprs_conf: confluent … ltprs.
-/3 width=3/ qed.
-
-theorem ltprs_trans: Transitive … ltprs.
-/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/reducibility/tpr.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
-
-(* Basic_1: includes: pr1_pr0 *)
-definition tprs: relation term ≝ TC … tpr.
-
-interpretation "context-free parallel computation (term)"
- 'PRedStar T1 T2 = (tprs T1 T2).
-
-(* Basic eliminators ********************************************************)
-
-lemma tprs_ind: ∀T1. ∀R:predicate term. R T1 →
- (∀T,T2. T1 ➡* T → T ➡ T2 → R T → R T2) →
- ∀T2. T1 ➡* T2 → R T2.
-#T1 #R #HT1 #IHT1 #T2 #HT12
-@(TC_star_ind … HT1 IHT1 … HT12) //
-qed-.
-
-lemma tprs_ind_dx: ∀T2. ∀R:predicate term. R T2 →
- (∀T1,T. T1 ➡ T → T ➡* T2 → R T → R T1) →
- ∀T1. T1 ➡* T2 → R T1.
-#T2 #R #HT2 #IHT2 #T1 #HT12
-@(TC_star_ind_dx … HT2 IHT2 … HT12) //
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tprs_refl: reflexive … tprs.
-/2 width=1/ qed.
-
-lemma tpr_tprs: ∀T1,T2. T1 ➡ T2 → T2 ➡* T2.
-/2 width=1/ qed.
-
-lemma tprs_strap1: ∀T1,T,T2. T1 ➡* T → T ➡ T2 → T1 ➡* T2.
-/2 width=3/ qed.
-
-lemma tprs_strap2: ∀T1,T,T2. T1 ➡ T → T ➡* T2 → T1 ➡* T2.
-/2 width=3/ qed.
-
-(* Basic_1: was only: pr1_head_1 *)
-lemma tprs_pair_sn: ∀I,T1,T2. T1 ➡ T2 → ∀V1,V2. V1 ➡* V2 →
- ②{I} V1. T1 ➡* ②{I} V2. T2.
-* [ #a ] #I #T1 #T2 #HT12 #V1 #V2 #H @(tprs_ind … H) -V2
-[1,3: /3 width=1/
-|2,4: #V #V2 #_ #HV2 #IHV1
- @(tprs_strap1 … IHV1) -IHV1 /2 width=1/
-]
-qed.
-
-(* Basic_1: was only: pr1_head_2 *)
-lemma tprs_pair_dx: ∀I,V1,V2. V1 ➡ V2 → ∀T1,T2. T1 ➡* T2 →
- ②{I} V1. T1 ➡* ②{I} V2. T2.
-* [ #a ] #I #V1 #V2 #HV12 #T1 #T2 #H @(tprs_ind … H) -T2
-[1,3: /3 width=1/
-|2,4: #T #T2 #_ #HT2 #IHT1
- @(tprs_strap1 … IHT1) -IHT1 /2 width=1/
-]
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma tprs_inv_atom1: ∀U2,k. ⋆k ➡* U2 → U2 = ⋆k.
-#U2 #k #H @(tprs_ind … H) -U2 //
-#U #U2 #_ #HU2 #IHU1 destruct
->(tpr_inv_atom1 … HU2) -HU2 //
-qed-.
-
-lemma tprs_inv_cast1: ∀W1,T1,U2. ⓝW1.T1 ➡* U2 → T1 ➡* U2 ∨
- ∃∃W2,T2. W1 ➡* W2 & T1 ➡* T2 & U2 = ⓝW2.T2.
-#W1 #T1 #U2 #H @(tprs_ind … H) -U2 /3 width=5/
-#U #U2 #_ #HU2 * /3 width=3/ *
-#W #T #HW1 #HT1 #H destruct
-elim (tpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
-#W2 #T2 #HW2 #HT2 #H destruct /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/reducibility/tpr_lift.ma".
-include "basic_2/computation/tprs.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
-
-(* Advanced inversion lemmas ************************************************)
-
-lemma tprs_inv_abst1: ∀a,V1,T1,U2. ⓛ{a}V1. T1 ➡* U2 →
- ∃∃V2,T2. V1 ➡* V2 & T1 ➡* T2 & U2 = ⓛ{a}V2. T2.
-#a #V1 #T1 #U2 #H @(tprs_ind … H) -U2 /2 width=5/
-#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
-elim (tpr_inv_abst1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
-qed-.
-
-lemma tprs_inv_abst: ∀a,V1,V2,T1,T2. ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2 →
- V1 ➡* V2 ∧ T1 ➡* T2.
-#a #V1 #V2 #T1 #T2 #H
-elim (tprs_inv_abst1 … H) -H #V #T #HV1 #HT1 #H destruct /2 width=1/
-qed-.
-
-(* Relocation properties ****************************************************)
-
-(* Note: this was missing in basic_1 *)
-lemma tprs_lift: t_liftable tprs.
-/3 width=7/ qed.
-
-(* Note: this was missing in basic_1 *)
-lemma tprs_inv_lift1: t_deliftable_sn tprs.
-/3 width=3 by tpr_inv_lift1, t_deliftable_sn_TC/ 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_tpr.ma".
-include "basic_2/computation/tprs.ma".
-
-(* CONTEXT-FREE PARALLEL COMPUTATION ON TERMS *******************************)
-
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was: pr1_strip *)
-lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 →
- ∃∃T0. T1 ➡ T0 & T2 ➡* T0.
-/3 width=3 by TC_strip1, tpr_conf/ qed.
-
-(* Main propertis ***********************************************************)
-
-(* Basic_1: was: pr1_confluence *)
-theorem tprs_conf: confluent … tprs.
-/3 width=3/ qed.
-
-(* Basic_1: was: pr1_t *)
-theorem tprs_trans: Transitive … tprs.
-/2 width=3/ qed.
-
-(* Basic_1: was: pr1_comp *)
-lemma tprs_pair: ∀I,V1,V2. V1 ➡* V2 → ∀T1,T2. T1 ➡* T2 →
- ②{I} V1. T1 ➡* ②{I} V2. T2.
-#I #V1 #V2 #H @(tprs_ind … H) -V2 /2 width=1/
-#V #V2 #_ #HV2 #IHV1 #T1 #T2 #HT12
-@(tprs_trans … (②{I}V.T2)) /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/reducibility/cpr_ltpss_dx.ma".
+include "basic_2/computation/cprs_tpss.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties concerning dx partial unfold on local environments ************)
+
+lemma cprs_ltpss_dx_conf: ∀L1,T,U1. L1 ⊢ T ➡* U1 →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∃∃U2. L2 ⊢ T ➡* U2 & L2 ⊢ U1 ▶* [d, e] U2.
+#L1 #T #U1 #H @(cprs_ind … H) -U1 /2 width=3/
+#T1 #U1 #_ #HTU1 #IHT1 #L2 #d #e #HL12
+elim (IHT1 … HL12) -IHT1 #U #HTU #HT1U
+elim (ltpss_dx_cpr_conf … HTU1 … HL12) -L1 #U0 #HT1U0 #HU10
+elim (cpr_tpss_conf … HT1U0 … HT1U) -T1 #U2 #HU02 #HU2
+lapply (tpss_trans_eq … HU10 HU02) -U0 /3 width=3/
+qed-.
+
+lemma cprs_ltpss_dx_tpss_conf: ∀L1,T1,U1. L1 ⊢ T1 ➡* U1 →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
+ ∃∃U2. L2 ⊢ T2 ➡* U2 & L2 ⊢ U1 ▶* [d, e] U2.
+#L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12
+elim (cprs_ltpss_dx_conf … HTU1 … HL12) -L1 #U #HT1U #HU1
+elim (cprs_tpss_conf … HT1U … HT12) -T1 #T #HUT #HT2
+lapply (tpss_trans_eq … HU1 HUT) -U /2 width=3/
+qed-.
+
+lemma cprs_ltpss_dx_tpss2_conf: ∀L1,T1,U1. L1 ⊢ T1 ➡* U1 →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
+ ∀U2. L2 ⊢ U1 ▶* [d, e] U2 →
+ ∃∃U. L2 ⊢ T2 ➡* U & L2 ⊢ U2 ▶* [d, e] U.
+#L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12 #U2 #HU12
+elim (cprs_ltpss_dx_tpss_conf … HTU1 … HL12 … HT12) -L1 -T1 #U #HT2U #HU1
+elim (tpss_conf_eq … HU12 … HU1) -U1 #U0 #HU20 #HU0
+lapply (cprs_tpss_trans … HT2U … HU0) -U /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/ltpss_sn_alt.ma".
+include "basic_2/computation/cprs_ltpss_dx.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties concerning sn partial unfold on local environments ************)
+
+lemma cprs_ltpss_sn_conf: ∀L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 →
+ ∀T,U1. L1 ⊢ T ➡* U1 →
+ ∃∃U2. L2 ⊢ T ➡* U2 & L1 ⊢ U1 ▶* [d, e] U2.
+#L1 #L2 #d #e #H
+lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 /2 width=3/
+#L #L2 #HL1 #HL2 #IHL1 #T #U1 #HTU1
+lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1
+lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12
+elim (IHL1 … HTU1) -IHL1 -HTU1 #U #HTU #HU1
+elim (cprs_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #HTU2 #HU2
+lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2
+lapply (tpss_trans_eq … HU1 HU2) -U /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/unwind/sstas_ltpss_dx.ma".
+include "basic_2/computation/cprs_ltpss_dx.ma".
+include "basic_2/computation/dxprs.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
+
+(* Properties about dx parallel unfold **************************************)
+
+lemma dxprs_ltpss_dx_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L2 ⊢ U1 ▶* [d, e] U2.
+#h #g #L1 #T #U1 * #U #HTU #HU1 #L2 #d #e #HL12
+elim (sstas_ltpss_dx_conf … HTU … HL12) -HTU #U0 #HTU0 #HU0
+elim (cprs_ltpss_dx_conf … HU1 … HL12) -L1 #U2 #HU2 #HU12
+elim (cprs_tpss_conf … HU2 … HU0) -U #U #HU2 #HU0
+lapply (tpss_trans_eq … HU12 HU2) -U2 /3 width=3/
+qed-.
+
+lemma dxprs_tpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*➡*[g] U1 →
+ ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 →
+ ∃∃U2. ⦃h, L⦄ ⊢ T2 •*➡*[g] U2 & L ⊢ U1 ▶* [d, e] U2.
+#h #g #L #T1 #U1 * #W1 #HTW1 #HWU1 #T2 #d #e #HT12
+elim (sstas_tpss_conf … HTW1 … HT12) -T1 #W2 #HTW2 #HW12
+elim (cprs_tpss_conf … HWU1 … HW12) -W1 /3 width=3/
+qed-.
+
+lemma dxprs_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 →
+ ∀L2,d,e. L1 ▶* [d, e] L2 →
+ ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
+ ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 &
+ L2 ⊢ U1 ▶* [d, e] U2.
+#h #g #L1 #T1 #U1 #HTU1 #L2 #d #e #HL12 #T2 #HT12
+elim (dxprs_ltpss_dx_conf … HTU1 … HL12) -L1 #U #HT1U #HU1
+elim (dxprs_tpss_conf … HT1U … HT12) -T1 #U2 #HTU2 #HU2
+lapply (tpss_trans_eq … HU1 HU2) -U /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/ltpss_sn_alt.ma".
+include "basic_2/computation/dxprs_ltpss_dx.ma".
+
+(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
+
+(* Properties about sn parallel unfold **************************************)
+
+lemma dxprs_ltpss_sn_conf: ∀h,g,L1,L2,d,e. L1 ⊢ ▶* [d, e] L2 →
+ ∀T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 →
+ ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L1 ⊢ U1 ▶* [d, e] U2.
+#h #g #L1 #L2 #d #e #H
+lapply (ltpss_sn_ltpssa … H) -H #H @(ltpssa_ind … H) -L2 [ /2 width=3/ ]
+#L #L2 #HL1 #HL2 #IHL1 #T #U1 #HTU1
+lapply (ltpssa_ltpss_sn … HL1) -HL1 #HL1
+lapply (ltpss_sn_dx_trans_eq … HL1 … HL2) -HL1 #HL12
+elim (IHL1 … HTU1) -IHL1 -HTU1 #U #HTU #HU1
+elim (dxprs_ltpss_dx_conf … HTU … HL2) -HTU -HL2 #U2 #HTU2 #HU2
+lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2
+lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/
+qed-.
interpretation "simple (term)" 'Simple T = (simple T).
(* Basic inversion lemmas ***************************************************)
-(*
-lemma mt: ∀R1,R2:Prop. (R1 → R2) → (R2 → ⊥) → R1 → ⊥.
-/3 width=1/ qed.
-*)
+
fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀a,J,W,U. T = ⓑ{a,J} W. U → ⊥.
#T * -T
[ #I #a #J #W #U #H destruct
qed.
lemma simple_inv_bind: ∀a,I,V,T. 𝐒⦃ⓑ{a,I} V. T⦄ → ⊥.
-/2 width=7/ qed-. (**) (* auto fails if mt is enabled *)
+/2 width=7/ qed-.
lemma simple_inv_pair: ∀I,V,T. 𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J.
* /2 width=2/ #a #I #V #T #H
(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************)
-(* Basic_1: includes: pr0_delta1 pr2_delta1 pr2_thin_dx pr2_head_1 *)
+(* Basic_1: includes: pr0_delta1 pr2_delta1 pr2_thin_dx *)
(* Note: cpr_flat: does not hold in basic_1 *)
inductive cpr: lenv → relation term ≝
| cpr_atom : ∀I,L. cpr L (⓪{I}) (⓪{I})
lemma cpr_refl: ∀T,L. L ⊢ T ➡ T.
/2 width=1/ qed.
+(* Basic_1: was: pr2_head_1 *)
+lemma cpr_pair_sn: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 →
+ ∀T. L⊢ ②{I}V1.T ➡ ②{I}V2.T.
+* /2 width=1/ qed.
+
lemma cpr_delift: ∀L,K,V,T1,d. ⇩[0, d] L ≡ (K. ⓓV) →
∃∃T2,T. L ⊢ T1 ➡ T2 & ⇧[d, 1] T ≡ T2.
#L #K #V #T1 #d #HLK
]
qed-.
-(* Basic_1: removed theorems 12:
+(* Basic_1: removed theorems 11:
pr0_subst0_back pr0_subst0_fwd pr0_subst0
pr2_head_2 pr2_cflat clear_pr2_trans
pr2_gen_csort pr2_gen_cflat pr2_gen_cbind
- pr2_subst1
pr2_gen_ctail pr2_ctail
-*)
+*)
(* Basic_1: removed local theorems 4:
pr0_delta_tau pr0_cong_delta
pr2_free_free pr2_free_delta
elim (cpr_inv_abbr1 … H) -H *
[ #W1 #T1 #HW01 #HT01 #H destruct
elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/
- elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 /4 width=7/
+ elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0
+ /4 width=7 by cpr_bind, cpr_flat, cpr_theta, ex2_intro/ (**) (* timeout=35 *)
| #T1 #HT01 #HXT1 #H destruct
elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
elim (cpr_inv_lift1 … HT1 L1 … HXT1) -HXT1 /2 width=1/ #Y #HYT #HXY
elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0
elim (lift_total V 0 1) #U #HVU
lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1/
-lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/ /4 width=7/
+lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1/
+/4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* timeout 40 *)
qed-.
theorem cpr_conf_lpr: lpx_sn_confluent cpr cpr.
qed-.
(* Basic_1: includes: pr0_subst1 *)
+(* Basic_1: was: pr2_subst1 *)
lemma cpr_cpss_conf: ∀L. confluent2 … (cpr L) (cpss L).
/2 width=6 by cpr_cpss_conf_lpr_lpss/ qed-.
(*
(* Advanced inversion lemmas on plus-iterated supclosure ********************)
-lemma fsupp_inv_bind1_fsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃L2, T2⦄ →
+lamma fsupp_inv_bind1_fsups: ∀b,J,L1,L2,W,U,T2. ⦃L1, ⓑ{b,J}W.U⦄ ⊃+ ⦃L2, T2⦄ →
⦃L1, W⦄ ⊃* ⦃L2, T2⦄ ∨ ⦃L1.ⓑ{J}W, U⦄ ⊃* ⦃L2, T2⦄.
#b #J #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -L2 -T2
[ #L2 #T2 #H
elim (fsup_inv_bind1 … H) -H * #H1 #H2 destruct /2 width=1/
| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
]
-qed-.
+qad-.
-lemma fsupp_inv_flat1_fsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃+ ⦃L2, T2⦄ →
+lamma fsupp_inv_flat1_fsups: ∀J,L1,L2,W,U,T2. ⦃L1, ⓕ{J}W.U⦄ ⊃+ ⦃L2, T2⦄ →
⦃L1, W⦄ ⊃* ⦃L2, T2⦄ ∨ ⦃L1, U⦄ ⊃* ⦃L2, T2⦄.
#J #L1 #L2 #W #U #T2 #H @(fsupp_ind … H) -L2 -T2
[ #L2 #T2 #H
elim (fsup_inv_flat1 … H) -H #H1 * #H2 destruct /2 width=1/
| #L #T #L2 #T2 #_ #HT2 * /3 width=4/
]
-qed-.
+qad-.
*)
]
class "cyan"
[ { "computation" * } {
- [ { "focalized computation" * } {
- [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ]
- [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
- }
- ]
[ { "decomposed extended computation" * } {
- [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxprs_dxprs" * ]
+ [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ]
}
]
[ { "weakly normalizing computation" * } {
}
]
[ { "strongly normalizing computation" * } {
- [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_cpr_vector" + "csn_tstc_vector" + "csn_aaa" * ]
- [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_cpr" + "csn_lfpr" * ]
+ [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_tstc_vector" + "csn_aaa" * ]
+ [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_lpr" * ]
}
]
[ { "context-sensitive computation" * } {
- [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_aaa" + "lprs_cprs" + "lprs_lprs" * ]
- [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_aaa" + "cprs_lpr" + "cprs_cprs" + "cprs_tstc" + "cprs_tstc_vector" * ]
+ [ "lprs ( ? ⊢ ➡* ? )" "lprs_alt ( ? ⊢ ➡➡* ? )" "lprs_ldrop" + "lprs_lpss" + "lprs_aaa" + "lprs_cprs" + "lprs_lprs" * ]
+ [ "cprs ( ? ⊢ ? ➡* ?)" "cprs_tstc" + "cprs_tstc_vector" + "cprs_lift" + "cprs_lpss" + "cprs_aaa" + "cprs_cprs" * ]
}
]
[ { "local env. ref. for abstract candidates of reducibility" * } {
projects / helm.git / commitdiff