--- /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/rt_transition/cpx_fqus.ma".
+include "basic_2/rt_transition/lfpx_fquq.ma".
+include "basic_2/rt_computation/cpxs_drops.ma".
+include "basic_2/rt_computation/cpxs_cpxs.ma".
+
+(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
+
+(* Properties with unbound parallel rt-transition on referred entries *******)
+
+lemma lfpx_cpxs_conf: ∀h,G. s_r_confluent1 … (cpxs h G) (lfpx h G).
+/3 width=5 by lfpx_cpx_conf, s_r_conf1_CTC1/ qed-.
+
+lemma lfpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpx h G).
+#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 //
+[ #G #L2 #s1 #L1 #H elim (lfpx_inv_sort … H) -H * /2 width=1 by cpx_cpxs/
+| #I #G #L2 #V #V2 #W2 #_ #IH #HVW2 #Y1 #H
+ elim (lfpx_inv_zero_pair_dx … H) -H #L1 #V1 #HL1 #HV1 #H destruct
+ /5 width=3 by lfpx_cpx_conf, cpxs_delta, cpxs_strap2/
+| #I2 #G #L2 #V2 #W2 #i #_ #IH #HVW2 #Y1 #H
+ elim (lfpx_inv_lref_bind_dx … H) -H #I1 #L1 #HL1 #H destruct
+ /4 width=3 by cpxs_lref, cpxs_strap2/
+| #p #I #G #L2 #V #V2 #T #T2 #_ #_ #IHV #IHT #L1 #H
+ elim (lfpx_inv_bind … H) -H /3 width=1 by cpxs_bind/
+| #I #G #L2 #V #V2 #T #T2 #_ #_ #IHV #IHT #L1 #H
+ elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_flat/
+| #G #L2 #V #T #T2 #T0 #_ #IH #HT02 #L1 #H
+ elim (lfpx_inv_bind … H) -H /3 width=3 by cpxs_zeta/
+| #G #L2 #V #T #T2 #_ #IH #L1 #H
+ elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_eps/
+| #G #L2 #V #V2 #T #_ #IH #L1 #H
+ elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_ee/
+| #p #G #L2 #V #V2 #W #W2 #T #T2 #_ #_ #_ #IHV #IHW #IHT #L1 #H
+ elim (lfpx_inv_flat … H) -H #HV #H
+ elim (lfpx_inv_bind … H) -H /3 width=1 by cpxs_beta/
+| #p #G #L2 #V #V2 #V0 #W #W2 #T #T2 #_ #_ #_ #IHV #IHW #IHT #HV20 #L1 #H
+ elim (lfpx_inv_flat … H) -H #HV #H
+ elim (lfpx_inv_bind … H) -H /3 width=3 by cpxs_theta/
+]
+qed.
+
+lemma lfpx_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpx h G).
+/3 width=6 by lfpx_cpx_conf, lfpx_cpx_trans, s_r_trans_CTC1/
+qed-.
+
+(* Properties with plus-iterated structural successor for closures **********)
+
+lemma lfpx_fqup_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h, T1] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, K1, T⦄ ⊐+[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h, T2] L2.
+#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lfpx_fqu_trans … H12 … HKL1) -L1
+ /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+ #L0 #T0 #HT10 #HT0 #HL0 elim (lfpx_fqu_trans … H2 … HL0) -L
+ #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
+ /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
+]
+qed-.
+
+(* Properties with star-iterated structural successor for closures **********)
+
+lemma lfpx_fqus_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h, T1] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, K1, T⦄ ⊐*[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h, T2] L2.
+#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fqus_inv_fqup … H) -H
+[ #H12 elim (lfpx_fqup_trans … H12 … HKL1) -L1 /3 width=5 by fqup_fqus, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/cpxs_lfpx.ma".
+include "basic_2/rt_computation/csx_cpxs.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
+
+(* Properties with unbound parallel rt-transition on referred entries *******)
+
+lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+#h #o #G #L1 #T #H @(csx_ind_cpxs … H) -T
+/5 width=3 by csx_intro, lfpx_cpx_trans, lfpx_cpxs_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/rt_computation/csx_lfpx.ma".
+include "basic_2/rt_computation/lfpxs_fqup.ma".
+
+(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
+
+(* Properties with unbound parallel rt-computation on referred entries ******)
+
+lemma csx_lfpxs_conf: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
+ ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+#h #o #G #L1 #L2 #T #H @(lfpxs_ind_sn … H) -L2 /3 by lfpxs_step_dx, csx_lfpx_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/rt_computation/fpbs_lfpxs.ma".
+include "basic_2/rt_computation/fpbg.ma".
+
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties with unbound parallel rt-computation on referred entries ******)
+
+(* Basic_2A1: uses: lpxs_fpbg *)
+lemma lfpxs_lfdneq_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
+ (L1 ≛[h, o, T] L2 → ⊥) → ⦃G, L1, T⦄ >[h, o] ⦃G, L2, T⦄.
+#h #o #G #L1 #L2 #T #H #H0
+elim (lfpxs_lfdneq_inv_step_sn … H … H0) -H -H0
+/4 width=7 by fpb_lfpx, lfpxs_ffdeq_fpbs, ffdeq_intro_sn, ex2_3_intro/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/static/ffdeq_fqus.ma".
+include "basic_2/static/ffdeq_ffdeq.ma".
+include "basic_2/rt_computation/cpxs_fqus.ma".
+include "basic_2/rt_computation/cpxs_ffdeq.ma".
+include "basic_2/rt_computation/cpxs_lfpx.ma".
+include "basic_2/rt_computation/lfpxs_ffdeq.ma".
+include "basic_2/rt_computation/fpbs_cpxs.ma".
+
+(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
+
+(* Properties with unbound parallel rt-computation on referred entries ******)
+
+(* Basic_2A1: uses: lpxs_fpbs *)
+lemma lfpxs_fpbs: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄.
+#h #o #G #L1 #L2 #T #H @(lfpxs_ind_sn … H) -L2
+/3 width=5 by fpbq_lfpx, fpbs_strap1/
+qed.
+
+(* Basic_2A1: uses: fpbs_lpxs_trans *)
+lemma fpbs_lfpxs_trans: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L, T2⦄ →
+ ∀L2. ⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G2 #L1 #L #T1 #T2 #H1 #L2 #H @(lfpxs_ind_sn … H) -L2
+/3 width=5 by fpbs_strap1, fpbq_lfpx/
+qed-.
+
+(* Basic_2A1: uses: lpxs_fpbs_trans *)
+lemma lfpxs_fpbs_trans: ∀h,o,G1,G2,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
+ ∀L1. ⦃G1, L1⦄ ⊢ ⬈*[h, T1] L → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G2 #L #L2 #T1 #T2 #H1 #L1 #H @(lfpxs_ind_dx … H) -L1
+/3 width=5 by fpbs_strap2, fpbq_lfpx/
+qed-.
+
+(* Basic_2A1: uses: lpxs_lleq_fpbs *)
+lemma lfpxs_ffdeq_fpbs: ∀h,o,G1,L1,L,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, T1] L →
+ ∀G2,L2,T2. ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+/3 width=3 by lfpxs_fpbs_trans, ffdeq_fpbs/ qed.
+
+lemma fpbs_lfpx_trans: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L, T2⦄ →
+ ∀L2. ⦃G2, L⦄ ⊢ ⬈[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+/3 width=3 by fpbs_lfpxs_trans, lfpx_lfpxs/ qed-.
+
+(* Properties with star-iterated structural successor for closures **********)
+
+(* Basic_2A1: uses: fqus_lpxs_fpbs *)
+lemma fqus_lfpxs_fpbs: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L, T2⦄ →
+ ∀L2. ⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+/3 width=3 by fpbs_lfpxs_trans, fqus_fpbs/ qed.
+
+(* Properties with unbound context-sensitive parallel rt-computation ********)
+
+(* Basic_2A1: uses: cpxs_fqus_lpxs_fpbs *)
+lemma cpxs_fqus_lfpxs_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
+ ∀G2,L,T2. ⦃G1, L1, T⦄ ⊐* ⦃G2, L, T2⦄ →
+ ∀L2.⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+/3 width=5 by cpxs_fqus_fpbs, fpbs_lfpxs_trans/ qed.
+
+lemma fpbs_cpxs_tdeq_fqup_lfpx_trans: ∀h,o,G1,G3,L1,L3,T1,T3. ⦃G1, L1, T1⦄ ≥ [h, o] ⦃G3, L3, T3⦄ →
+ ∀T4. ⦃G3, L3⦄ ⊢ T3 ⬈*[h] T4 → ∀T5. T4 ≛[h, o] T5 →
+ ∀G2,L4,T2. ⦃G3, L3, T5⦄ ⊐+ ⦃G2, L4, T2⦄ →
+ ∀L2. ⦃G2, L4⦄ ⊢ ⬈[h, T2] L2 → ⦃G1, L1, T1⦄ ≥ [h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G3 #L1 #L3 #T1 #T3 #H13 #T4 #HT34 #T5 #HT45 #G2 #L4 #T2 #H34 #L2 #HL42
+@(fpbs_lfpx_trans … HL42) -L2 (**) (* full auto too slow *)
+@(fpbs_fqup_trans … H34) -G2 -L4 -T2
+/3 width=3 by fpbs_cpxs_trans, fpbs_tdeq_trans/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma fpbs_intro_fstar: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
+ ∀G,L,T0. ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ →
+ ∀L0. ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 →
+ ∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ .
+/3 width=5 by cpxs_fqus_lfpxs_fpbs, fpbs_strap1, fpbq_ffdeq/ qed.
+
+(* Advanced inversion lemmas *************************************************)
+
+lemma fpbs_inv_fstar: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
+ ∃∃G,L,L0,T,T0. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄
+ & ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 & ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1
+[ /2 width=9 by ex4_5_intro/
+| #G1 #G0 #L1 #L0 #T1 #T0 * -G0 -L0 -T0
+ [ #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
+ elim (fquq_cpxs_trans … HT03 … H10) -T0
+ /3 width=9 by fqus_strap2, ex4_5_intro/
+ | #T0 #HT10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
+ /3 width=9 by cpxs_strap2, ex4_5_intro/
+ | #L0 #HL10 #_ * #G3 #L3 #L4 #T3 #T4 #HT13 #H34 #HL34 #H42
+ lapply (lfpx_cpxs_trans … HT13 … HL10) -HT13 #HT13
+ lapply (lfpx_cpxs_conf … HT13 … HL10) -HL10 #HL10
+ elim (lfpx_fqus_trans … H34 … HL10) -L0
+ /3 width=9 by lfpxs_step_sn, cpxs_trans, ex4_5_intro/
+ | #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
+ elim (ffdeq_cpxs_trans … H10 … HT03) -T0 #T0 #HT10 #H03
+ elim (ffdeq_fqus_trans … H03 … H34) -G0 -L0 -T3 #G0 #L0 #T3 #H03 #H34
+ elim (ffdeq_lfpxs_trans … H34 … HL34) -L3 #L3 #HL03 #H34
+ /3 width=13 by ffdeq_trans, ex4_5_intro/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/lfpx_aaa.ma".
+include "basic_2/rt_transition/lpx_aaa.ma".
include "basic_2/rt_computation/cpxs.ma".
(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
qed-.
(* Note: a proof based on fqu_cpx_trans_tdneq might exist *)
+(* Basic_2A1: uses: fqu_cpxs_trans_neq *)
lemma fqu_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) →
∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄.
]
qed-.
+(* Basic_2A1: uses: fquq_cpxs_trans_neq *)
lemma fquq_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) →
∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄.
]
qed-.
+(* Basic_2A1: uses: fqup_cpxs_trans_neq *)
lemma fqup_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) →
∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄.
]
qed-.
+(* Basic_2A1: uses: fqus_cpxs_trans_neq *)
lemma fqus_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ →
∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 → (T2 ≛[h, o] U2 → ⊥) →
∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] U1 & T1 ≛[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄.
+++ /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/rt_transition/cpx_fqus.ma".
-include "basic_2/rt_transition/lfpx_fquq.ma".
-include "basic_2/rt_computation/cpxs_drops.ma".
-include "basic_2/rt_computation/cpxs_cpxs.ma".
-
-(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-
-(* Properties with unbound parallel rt-transition on referred entries *******)
-
-lemma lfpx_cpxs_conf: ∀h,G. s_r_confluent1 … (cpxs h G) (lfpx h G).
-/3 width=5 by lfpx_cpx_conf, s_r_conf1_CTC1/ qed-.
-
-lemma lfpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpx h G).
-#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 //
-[ #G #L2 #s1 #L1 #H elim (lfpx_inv_sort … H) -H * /2 width=1 by cpx_cpxs/
-| #I #G #L2 #V #V2 #W2 #_ #IH #HVW2 #Y1 #H
- elim (lfpx_inv_zero_pair_dx … H) -H #L1 #V1 #HL1 #HV1 #H destruct
- /5 width=3 by lfpx_cpx_conf, cpxs_delta, cpxs_strap2/
-| #I2 #G #L2 #V2 #W2 #i #_ #IH #HVW2 #Y1 #H
- elim (lfpx_inv_lref_bind_dx … H) -H #I1 #L1 #HL1 #H destruct
- /4 width=3 by cpxs_lref, cpxs_strap2/
-| #p #I #G #L2 #V #V2 #T #T2 #_ #_ #IHV #IHT #L1 #H
- elim (lfpx_inv_bind … H) -H /3 width=1 by cpxs_bind/
-| #I #G #L2 #V #V2 #T #T2 #_ #_ #IHV #IHT #L1 #H
- elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_flat/
-| #G #L2 #V #T #T2 #T0 #_ #IH #HT02 #L1 #H
- elim (lfpx_inv_bind … H) -H /3 width=3 by cpxs_zeta/
-| #G #L2 #V #T #T2 #_ #IH #L1 #H
- elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_eps/
-| #G #L2 #V #V2 #T #_ #IH #L1 #H
- elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_ee/
-| #p #G #L2 #V #V2 #W #W2 #T #T2 #_ #_ #_ #IHV #IHW #IHT #L1 #H
- elim (lfpx_inv_flat … H) -H #HV #H
- elim (lfpx_inv_bind … H) -H /3 width=1 by cpxs_beta/
-| #p #G #L2 #V #V2 #V0 #W #W2 #T #T2 #_ #_ #_ #IHV #IHW #IHT #HV20 #L1 #H
- elim (lfpx_inv_flat … H) -H #HV #H
- elim (lfpx_inv_bind … H) -H /3 width=3 by cpxs_theta/
-]
-qed.
-
-lemma lfpx_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpx h G).
-/3 width=6 by lfpx_cpx_conf, lfpx_cpx_trans, s_r_trans_CTC1/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma cpx_bind2: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
- ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈[h] T2 →
- ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
-/4 width=5 by lfpx_cpx_trans, cpxs_bind_dx, lfpx_pair_refl/ qed.
-
-lemma cpxs_bind2_dx: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
- ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 →
- ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
-/4 width=5 by lfpx_cpxs_trans, cpxs_bind_dx, lfpx_pair_refl/ qed.
-
-(* Properties with plus-iterated structural successor for closures **********)
-
-(* Basic_2A1: uses: lpx_fqup_trans *)
-lemma lfpx_fqup_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h, T1] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, K1, T⦄ ⊐+[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h, T2] L2.
-#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
-[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lfpx_fqu_trans … H12 … HKL1) -L1
- /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
-| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
- #L0 #T0 #HT10 #HT0 #HL0 elim (lfpx_fqu_trans … H2 … HL0) -L
- #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
- /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
-]
-qed-.
-
-(* Properties with star-iterated structural successor for closures **********)
-
-(* Basic_2A1: uses: lpx_fqus_trans *)
-lemma lfpx_fqus_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ →
- ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h, T1] L1 →
- ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, K1, T⦄ ⊐*[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h, T2] L2.
-#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fqus_inv_fqup … H) -H
-[ #H12 elim (lfpx_fqup_trans … H12 … HKL1) -L1 /3 width=5 by fqup_fqus, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/lpx.ma".
+include "basic_2/rt_transition/cpx_fqus.ma".
+include "basic_2/rt_transition/lpx_fquq.ma".
include "basic_2/rt_computation/cpxs_drops.ma".
include "basic_2/rt_computation/cpxs_cpxs.ma".
(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
-(* Properties with unbound parallel rt-transition for local environments ****)
+(* Properties with unbound rt-transition for full local environments ********)
lemma lpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpx h G).
#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2
lemma lpx_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (λ_.lpx h G).
#h #G @s_r_trans_CTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *)
qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma cpx_bind2: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈[h] T2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
+/4 width=5 by lpx_cpx_trans, cpxs_bind_dx, lpx_pair/ qed.
+
+lemma cpxs_bind2_dx: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 →
+ ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 →
+ ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
+/4 width=5 by lpx_cpxs_trans, cpxs_bind_dx, lpx_pair/ qed.
+
+(* Properties with plus-iterated structural successor for closures **********)
+
+(* Basic_2A1: uses: lpx_fqup_trans *)
+lemma lpx_fqup_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, K1, T⦄ ⊐+[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h] L2.
+#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2
+[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1
+ /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/
+| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1
+ #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L
+ #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T
+ /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/
+]
+qed-.
+
+(* Properties with star-iterated structural successor for closures **********)
+
+(* Basic_2A1: uses: lpx_fqus_trans *)
+lemma lpx_fqus_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ →
+ ∀K1. ⦃G1, K1⦄ ⊢ ⬈[h] L1 →
+ ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, K1, T⦄ ⊐*[b] ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ⬈[h] L2.
+#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fqus_inv_fqup … H) -H
+[ #H12 elim (lpx_fqup_trans … H12 … HKL1) -L1 /3 width=5 by fqup_fqus, ex3_2_intro/
+| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
+]
+qed-.
include "basic_2/syntax/theq_tdeq.ma".
include "basic_2/rt_computation/cpxs_lsubr.ma".
include "basic_2/rt_computation/cpxs_cnx.ma".
-include "basic_2/rt_computation/lfpxs_cpxs.ma".
+include "basic_2/rt_computation/lpxs_cpxs.ma".
(* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
(* *)
(**************************************************************************)
-include "basic_2/rt_transition/lfpx_lfdeq.ma".
+include "basic_2/rt_transition/lpx_lfdeq.ma".
include "basic_2/rt_computation/csx_drops.ma".
(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
include "basic_2/rt_computation/cpxs_theq_vector.ma".
include "basic_2/rt_computation/csx_simple_theq.ma".
include "basic_2/rt_computation/csx_lsubr.ma".
-include "basic_2/rt_computation/csx_lfpx.ma".
+include "basic_2/rt_computation/csx_lpx.ma".
include "basic_2/rt_computation/csx_vector.ma".
(* STRONGLY NORMALIZING TERM VECTORS FOR UNBOUND PARALLEL RT-TRANSITION *****)
include "basic_2/rt_transition/fpbq.ma".
include "basic_2/rt_computation/csx_fqus.ma".
include "basic_2/rt_computation/csx_ffdeq.ma".
-include "basic_2/rt_computation/csx_lfpx.ma".
+include "basic_2/rt_computation/csx_lpx.ma".
(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
lemma csx_fpbq_conf: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ →
∀G2,L2,T2. ⦃G1, L1, T1⦄ ≽[h, o] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄.
#h #o #G1 #L1 #T1 #HT1 #G2 #L2 #T2 *
-/2 width=6 by csx_cpx_trans, csx_fquq_conf, csx_lfpx_conf, csx_ffdeq_conf/
+/2 width=6 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf, csx_ffdeq_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/rt_computation/cpxs_lfpx.ma".
-include "basic_2/rt_computation/csx_cpxs.ma".
-
-(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
-
-(* Properties with unbound parallel rt-transition on referred entries *******)
-
-(* Basic_2A1: was just: csx_lpx_conf *)
-lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
- ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
-#h #o #G #L1 #T #H @(csx_ind_cpxs … H) -T
-/5 width=3 by csx_intro, lfpx_cpx_trans, lfpx_cpxs_conf/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma csx_abst: ∀h,o,p,G,L,W. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃W⦄ →
- ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓛ{p}W.T⦄.
-#h #o #p #G #L #W #HW @(csx_ind … HW) -W
-#W #_ #IHW #T #HT @(csx_ind … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abst1 … H1) -H1
-#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (tdneq_inv_pair … H2) -H2
-[ #H elim H -H //
-| -IHT #H lapply (csx_cpx_trans … o … HLT0) // -HT
- #HT0 lapply (csx_lfpx_conf … HT0 … (L.ⓛW0)) -HT0 /4 width=1 by lfpx_pair_refl/
-| -IHW -HT /4 width=3 by csx_cpx_trans, cpx_pair_sn/
-]
-qed.
-
-lemma csx_abbr: ∀h,o,p,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ →
- ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.T⦄.
-#h #o #p #G #L #V #HV @(csx_ind … HV) -V
-#V #_ #IHV #T #HT @(csx_ind_cpxs … HT) -T #T #HT #IHT
-@csx_intro #X #H1 #H2
-elim (cpx_inv_abbr1 … H1) -H1 *
-[ #V1 #T1 #HLV1 #HLT1 #H destruct
- elim (tdneq_inv_pair … H2) -H2
- [ #H elim H -H //
- | /4 width=3 by csx_cpx_trans, csx_lfpx_conf, lfpx_pair_refl/
- | -IHV /4 width=3 by csx_cpx_trans, cpx_cpxs, cpx_pair_sn/
- ]
-| -IHV -IHT -H2
- /4 width=7 by csx_cpx_trans, csx_inv_lifts, drops_drop, drops_refl/
-]
-qed.
-
-fact csx_appl_theta_aux: ∀h,o,p,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → ∀V1,V2. ⬆*[1] V1 ≘ V2 →
- ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
-#h #o #p #G #L #X #H @(csx_ind_cpxs … H) -X
-#X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
-lapply (csx_fwd_pair_sn … HVT) #HV
-lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
-@csx_intro #X #HL #H
-elim (cpx_inv_appl1 … HL) -HL *
-[ -HV #V0 #Y #HLV10 #HL #H0 destruct
- elim (cpx_inv_abbr1 … HL) -HL *
- [ -HVT #V3 #T3 #HV3 #HLT3 #H0 destruct
- elim (cpx_lifts_sn … HLV10 (Ⓣ) … (L.ⓓV) … HV12) -HLV10 /3 width=1 by drops_refl, drops_drop/ #V4 #HV04 #HV24
- elim (tdeq_dec h o (ⓓ{p}V.ⓐV2.T) (ⓓ{p}V3.ⓐV4.T3)) #H0
- [ -IHVT -HV3 -HV24 -HLT3
- elim (tdeq_inv_pair … H0) -H0 #_ #HV3 #H0
- elim (tdeq_inv_pair … H0) -H0 #_ #HV24 #HT3
- elim (tdneq_inv_pair … H) -H #H elim H -H -G -L
- /3 width=6 by tdeq_inv_lifts_bi, tdeq_pair/
- | -V1 @(IHVT … H0 … HV04) -o -V0 /4 width=1 by cpx_cpxs, cpx_flat, cpx_bind/
- ]
- | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
- lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
- lapply (csx_inv_lifts … HVT0 (Ⓣ) … L ???) -HVT0
- /3 width=5 by csx_cpx_trans, cpx_pair_sn, drops_refl, drops_drop, lifts_flat/
- ]
-| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
-| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
- lapply (cpx_lifts_bi … HLV10 (Ⓣ) … (L.ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /3 width=1 by drops_refl, drops_drop/ #HLV23
- @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
- @(csx_lfpx_conf … (L.ⓓW0)) /2 width=1 by lfpx_pair_refl/ -W1
- /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
-]
-qed-.
-
-lemma csx_appl_theta: ∀h,o,p,G,L,V,V2,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ →
- ∀V1. ⬆*[1] V1 ≘ V2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
-/2 width=5 by csx_appl_theta_aux/ 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/rt_computation/csx_lfpx.ma".
-include "basic_2/rt_computation/lfpxs_fqup.ma".
-
-(* STRONGLY NORMALIZING TERMS FOR UNBOUND PARALLEL RT-TRANSITION ************)
-
-(* Properties with unbound parallel rt-computation on referred entries ******)
-
-(* Basic_2A1: uses: csx_lpxs_conf *)
-lemma csx_lfpxs_conf: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
- ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
-#h #o #G #L1 #L2 #T #H @(lfpxs_ind_sn … H) -L2 /3 by lfpxs_step_dx, csx_lfpx_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/rt_computation/cpxs_lpx.ma".
+include "basic_2/rt_computation/csx_cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
+
+(* Properties with unbound parallel rt-transition on all entries ************)
+
+lemma csx_lpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ →
+ ∀L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+#h #o #G #L1 #T #H @(csx_ind_cpxs … H) -T
+/4 width=3 by csx_intro, lpx_cpx_trans/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+lemma csx_abst: ∀h,o,p,G,L,W. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃W⦄ →
+ ∀T. ⦃G, L.ⓛW⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓛ{p}W.T⦄.
+#h #o #p #G #L #W #HW
+@(csx_ind … HW) -W #W #_ #IHW #T #HT
+@(csx_ind … HT) -T #T #HT #IHT
+@csx_intro #X #H1 #H2
+elim (cpx_inv_abst1 … H1) -H1 #W0 #T0 #HLW0 #HLT0 #H destruct
+elim (tdneq_inv_pair … H2) -H2
+[ #H elim H -H //
+| -IHT #H lapply (csx_cpx_trans … o … HLT0) // -HT #HT0
+ /4 width=5 by csx_lpx_conf, lpx_pair/
+| -IHW -HT /4 width=3 by csx_cpx_trans, cpx_pair_sn/
+]
+qed.
+
+lemma csx_abbr: ∀h,o,p,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ →
+ ∀T. ⦃G, L.ⓓV⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.T⦄.
+#h #o #p #G #L #V #HV
+@(csx_ind … HV) -V #V #_ #IHV #T #HT
+@(csx_ind_cpxs … HT) -T #T #HT #IHT
+@csx_intro #X #H1 #H2
+elim (cpx_inv_abbr1 … H1) -H1 *
+[ #V1 #T1 #HLV1 #HLT1 #H destruct
+ elim (tdneq_inv_pair … H2) -H2
+ [ #H elim H -H //
+ | /4 width=5 by csx_cpx_trans, csx_lpx_conf, lpx_pair/
+ | -IHV /4 width=3 by csx_cpx_trans, cpx_cpxs, cpx_pair_sn/
+ ]
+| -IHV -IHT -H2
+ /4 width=7 by csx_cpx_trans, csx_inv_lifts, drops_drop, drops_refl/
+]
+qed.
+
+fact csx_appl_theta_aux: ∀h,o,p,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → ∀V1,V2. ⬆*[1] V1 ≘ V2 →
+ ∀V,T. U = ⓓ{p}V.ⓐV2.T → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
+#h #o #p #G #L #X #H
+@(csx_ind_cpxs … H) -X #X #HVT #IHVT #V1 #V2 #HV12 #V #T #H destruct
+lapply (csx_fwd_pair_sn … HVT) #HV
+lapply (csx_fwd_bind_dx … HVT) -HVT #HVT
+@csx_intro #X #HL #H
+elim (cpx_inv_appl1 … HL) -HL *
+[ -HV #V0 #Y #HLV10 #HL #H0 destruct
+ elim (cpx_inv_abbr1 … HL) -HL *
+ [ #V3 #T3 #HV3 #HLT3 #H0 destruct
+ elim (cpx_lifts_sn … HLV10 (Ⓣ) … (L.ⓓV) … HV12) -HLV10 /3 width=1 by drops_refl, drops_drop/ #V4 #HV04 #HV24
+ elim (tdeq_dec h o (ⓓ{p}V.ⓐV2.T) (ⓓ{p}V3.ⓐV4.T3)) #H0
+ [ -IHVT -HV3 -HV24 -HLT3
+ elim (tdeq_inv_pair … H0) -H0 #_ #HV3 #H0
+ elim (tdeq_inv_pair … H0) -H0 #_ #HV24 #HT3
+ elim (tdneq_inv_pair … H) -H #H elim H -H -G -L
+ /3 width=6 by tdeq_inv_lifts_bi, tdeq_pair/
+ | -V1 @(IHVT … H0 … HV04) -o -V0 /4 width=1 by cpx_cpxs, cpx_flat, cpx_bind/
+ ]
+ | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct
+ lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0
+ lapply (csx_inv_lifts … HVT0 (Ⓣ) … L ???) -HVT0
+ /3 width=5 by csx_cpx_trans, cpx_pair_sn, drops_refl, drops_drop, lifts_flat/
+ ]
+| -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct
+| -IHVT -H #b #V0 #V3 #W0 #W1 #T0 #T1 #HLV10 #HV03 #HLW01 #HLT01 #H1 #H2 destruct
+ lapply (cpx_lifts_bi … HLV10 (Ⓣ) … (L.ⓓW0) … HV12 … HV03) -HLV10 -HV12 -HV03 /3 width=1 by drops_refl, drops_drop/ #HLV23
+ @csx_abbr /2 width=3 by csx_cpx_trans/ -HV
+ @(csx_lpx_conf … (L.ⓓW0)) /2 width=1 by lpx_pair/ -W1
+ /4 width=5 by csx_cpxs_trans, cpx_cpxs, cpx_flat/
+]
+qed-.
+
+lemma csx_appl_theta: ∀h,o,p,G,L,V,V2,T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓓ{p}V.ⓐV2.T⦄ →
+ ∀V1. ⬆*[1] V1 ≘ V2 → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV1.ⓓ{p}V.T⦄.
+/2 width=5 by csx_appl_theta_aux/ 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/rt_computation/csx_lpx.ma".
+include "basic_2/rt_computation/lpxs_lpx.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
+
+(* Properties with unbound parallel rt-computation on all entries ***********)
+
+lemma csx_lpxs_conf: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+ ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄.
+#h #o #G #L1 #L2 #T #H @(lpxs_ind_dx … H) -L2
+/3 by lpxs_step_dx, csx_lpx_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/rt_computation/fpbs_lfpxs.ma".
-include "basic_2/rt_computation/fpbg.ma".
-
-(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
-
-(* Properties with unbound parallel rt-computation on referred entries ******)
-
-(* Basic_2A1: uses: lpxs_fpbg *)
-lemma lfpxs_lfdneq_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 →
- (L1 ≛[h, o, T] L2 → ⊥) → ⦃G, L1, T⦄ >[h, o] ⦃G, L2, T⦄.
-#h #o #G #L1 #L2 #T #H #H0
-elim (lfpxs_lfdneq_inv_step_sn … H … H0) -H -H0
-/4 width=7 by fpb_lfpx, lfpxs_ffdeq_fpbs, ffdeq_intro_sn, ex2_3_intro/
-qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/rt_computation/fpbs_lpxs.ma".
+include "basic_2/rt_computation/fpbg.ma".
+
+(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
+
+(* Properties with unbound rt-computation on full local environments ********)
+
+(* Basic_2A1: uses: lpxs_fpbg *)
+lemma lpxs_lfdneq_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+ (L1 ≛[h, o, T] L2 → ⊥) → ⦃G, L1, T⦄ >[h, o] ⦃G, L2, T⦄.
+#h #o #G #L1 #L2 #T #H #H0
+elim (lpxs_lfdneq_inv_step_sn … H … H0) -H -H0
+/4 width=7 by fpb_lpx, lpxs_ffdeq_fpbs, ffdeq_intro_sn, ex2_3_intro/
+qed.
∀G1,L1,T1. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
/3 width=5 by fpbs_strap2, fpbq_ffdeq/ qed-.
-lemma tdeq_lfdeq_lfpx_fpbs: ∀h,o,T1,T2. T1 ≛[h, o] T2 → ∀L1,L0. L1 ≛[h, o, T2] L0 →
- ∀G,L2. ⦃G, L0⦄ ⊢ ⬈[h, T2] L2 → ⦃G, L1, T1⦄ ≥[h, o] ⦃G, L2, T2⦄.
-/4 width=5 by ffdeq_fpbs, fpbs_strap1, fpbq_lfpx, ffdeq_intro_dx/ qed.
+lemma tdeq_lfdeq_lpx_fpbs: ∀h,o,T1,T2. T1 ≛[h, o] T2 → ∀L1,L0. L1 ≛[h, o, T2] L0 →
+ ∀G,L2. ⦃G, L0⦄ ⊢ ⬈[h] L2 → ⦃G, L1, T1⦄ ≥[h, o] ⦃G, L2, T2⦄.
+/4 width=5 by ffdeq_fpbs, fpbs_strap1, fpbq_lpx, ffdeq_intro_dx/ qed.
(* Basic_2A1: removed theorems 3:
fpb_fpbsa_trans fpbs_fpbsa fpbsa_inv_fpbs
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "basic_2/static/ffdeq_fqus.ma".
-include "basic_2/static/ffdeq_ffdeq.ma".
-include "basic_2/rt_computation/cpxs_fqus.ma".
-include "basic_2/rt_computation/cpxs_ffdeq.ma".
-include "basic_2/rt_computation/cpxs_lfpx.ma".
-include "basic_2/rt_computation/lfpxs_ffdeq.ma".
-include "basic_2/rt_computation/fpbs_cpxs.ma".
-
-(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-
-(* Properties with unbound parallel rt-computation on referred entries ******)
-
-(* Basic_2A1: uses: lpxs_fpbs *)
-lemma lfpxs_fpbs: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄.
-#h #o #G #L1 #L2 #T #H @(lfpxs_ind_sn … H) -L2
-/3 width=5 by fpbq_lfpx, fpbs_strap1/
-qed.
-
-(* Basic_2A1: uses: fpbs_lpxs_trans *)
-lemma fpbs_lfpxs_trans: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L, T2⦄ →
- ∀L2. ⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L1 #L #T1 #T2 #H1 #L2 #H @(lfpxs_ind_sn … H) -L2
-/3 width=5 by fpbs_strap1, fpbq_lfpx/
-qed-.
-
-(* Basic_2A1: uses: lpxs_fpbs_trans *)
-lemma lfpxs_fpbs_trans: ∀h,o,G1,G2,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
- ∀L1. ⦃G1, L1⦄ ⊢ ⬈*[h, T1] L → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L #L2 #T1 #T2 #H1 #L1 #H @(lfpxs_ind_dx … H) -L1
-/3 width=5 by fpbs_strap2, fpbq_lfpx/
-qed-.
-
-(* Basic_2A1: uses: lpxs_lleq_fpbs *)
-lemma lfpxs_ffdeq_fpbs: ∀h,o,G1,L1,L,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, T1] L →
- ∀G2,L2,T2. ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-/3 width=3 by lfpxs_fpbs_trans, ffdeq_fpbs/ qed.
-
-lemma fpbs_lfpx_trans: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L, T2⦄ →
- ∀L2. ⦃G2, L⦄ ⊢ ⬈[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-/3 width=3 by fpbs_lfpxs_trans, lfpx_lfpxs/ qed-.
-
-(* Properties with star-iterated structural successor for closures **********)
-
-(* Basic_2A1: uses: fqus_lpxs_fpbs *)
-lemma fqus_lfpxs_fpbs: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L, T2⦄ →
- ∀L2. ⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-/3 width=3 by fpbs_lfpxs_trans, fqus_fpbs/ qed.
-
-(* Properties with unbound context-sensitive parallel rt-computation ********)
-
-(* Basic_2A1: uses: cpxs_fqus_lpxs_fpbs *)
-lemma cpxs_fqus_lfpxs_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
- ∀G2,L,T2. ⦃G1, L1, T⦄ ⊐* ⦃G2, L, T2⦄ →
- ∀L2.⦃G2, L⦄ ⊢ ⬈*[h, T2] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-/3 width=5 by cpxs_fqus_fpbs, fpbs_lfpxs_trans/ qed.
-
-lemma fpbs_cpxs_tdeq_fqup_lfpx_trans: ∀h,o,G1,G3,L1,L3,T1,T3. ⦃G1, L1, T1⦄ ≥ [h, o] ⦃G3, L3, T3⦄ →
- ∀T4. ⦃G3, L3⦄ ⊢ T3 ⬈*[h] T4 → ∀T5. T4 ≛[h, o] T5 →
- ∀G2,L4,T2. ⦃G3, L3, T5⦄ ⊐+ ⦃G2, L4, T2⦄ →
- ∀L2. ⦃G2, L4⦄ ⊢ ⬈[h, T2] L2 → ⦃G1, L1, T1⦄ ≥ [h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G3 #L1 #L3 #T1 #T3 #H13 #T4 #HT34 #T5 #HT45 #G2 #L4 #T2 #H34 #L2 #HL42
-@(fpbs_lfpx_trans … HL42) -L2 (**) (* full auto too slow *)
-@(fpbs_fqup_trans … H34) -G2 -L4 -T2
-/3 width=3 by fpbs_cpxs_trans, fpbs_tdeq_trans/
-qed-.
-
-(* Advanced properties ******************************************************)
-
-lemma fpbs_intro_fstar: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
- ∀G,L,T0. ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ →
- ∀L0. ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 →
- ∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ .
-/3 width=5 by cpxs_fqus_lfpxs_fpbs, fpbs_strap1, fpbq_ffdeq/ qed.
-
-(* Advanced inversion lemmas *************************************************)
-
-lemma fpbs_inv_fstar: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
- ∃∃G,L,L0,T,T0. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄
- & ⦃G, L⦄ ⊢ ⬈*[h, T0] L0 & ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1
-[ /2 width=9 by ex4_5_intro/
-| #G1 #G0 #L1 #L0 #T1 #T0 * -G0 -L0 -T0
- [ #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- elim (fquq_cpxs_trans … HT03 … H10) -T0
- /3 width=9 by fqus_strap2, ex4_5_intro/
- | #T0 #HT10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- /3 width=9 by cpxs_strap2, ex4_5_intro/
- | #L0 #HL10 #_ * #G3 #L3 #L4 #T3 #T4 #HT13 #H34 #HL34 #H42
- lapply (lfpx_cpxs_trans … HT13 … HL10) -HT13 #HT13
- lapply (lfpx_cpxs_conf … HT13 … HL10) -HL10 #HL10
- elim (lfpx_fqus_trans … H34 … HL10) -L0
- /3 width=9 by lfpxs_step_sn, cpxs_trans, ex4_5_intro/
- | #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
- elim (ffdeq_cpxs_trans … H10 … HT03) -T0 #T0 #HT10 #H03
- elim (ffdeq_fqus_trans … H03 … H34) -G0 -L0 -T3 #G0 #L0 #T3 #H03 #H34
- elim (ffdeq_lfpxs_trans … H34 … HL34) -L3 #L3 #HL03 #H34
- /3 width=13 by ffdeq_trans, ex4_5_intro/
- ]
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/static/ffdeq_lfeq.ma".
-include "basic_2/rt_computation/lfpxs_lpxs.ma".
-include "basic_2/rt_computation/fpbs_lfpxs.ma".
+include "basic_2/static/ffdeq_fqus.ma".
+include "basic_2/static/ffdeq_ffdeq.ma".
+include "basic_2/rt_computation/cpxs_fqus.ma".
+include "basic_2/rt_computation/cpxs_ffdeq.ma".
+include "basic_2/rt_computation/lpxs_ffdeq.ma".
+include "basic_2/rt_computation/lpxs_lpx.ma".
+include "basic_2/rt_computation/fpbs_fqus.ma".
+include "basic_2/rt_computation/fpbs_cpxs.ma".
(* PARALLEL RST-COMPUTATION FOR CLOSURES ************************************)
-(* Properties with unbound parallel rt-computation on local environments ****)
+(* Properties with unbound rt-computation on full local environments *******)
-(* Basic_2A1: uses: fpbs_intro_alt *)
+lemma lpxs_fpbs: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1, T⦄ ≥[h, o] ⦃G, L2, T⦄.
+#h #o #G #L1 #L2 #T #H @(lpxs_ind_dx … H) -L2
+/3 width=5 by fpbq_lpx, fpbs_strap1/
+qed.
+
+lemma fpbs_lpxs_trans: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L, T2⦄ →
+ ∀L2. ⦃G2, L⦄ ⊢ ⬈*[h] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G2 #L1 #L #T1 #T2 #H1 #L2 #H @(lpxs_ind_dx … H) -L2
+/3 width=5 by fpbs_strap1, fpbq_lpx/
+qed-.
+
+lemma lpxs_fpbs_trans: ∀h,o,G1,G2,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
+ ∀L1. ⦃G1, L1⦄ ⊢ ⬈*[h] L → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G2 #L #L2 #T1 #T2 #H1 #L1 #H @(lpxs_ind_sn … H) -L1
+/3 width=5 by fpbs_strap2, fpbq_lpx/
+qed-.
+
+(* Basic_2A1: uses: lpxs_lleq_fpbs *)
+lemma lpxs_ffdeq_fpbs: ∀h,o,G1,L1,L,T1. ⦃G1, L1⦄ ⊢ ⬈*[h] L →
+ ∀G2,L2,T2. ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+/3 width=3 by lpxs_fpbs_trans, ffdeq_fpbs/ qed.
+
+lemma fpbs_lpx_trans: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L, T2⦄ →
+ ∀L2. ⦃G2, L⦄ ⊢ ⬈[h] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+/3 width=3 by fpbs_lpxs_trans, lpx_lpxs/ qed-.
+
+(* Properties with star-iterated structural successor for closures **********)
+
+lemma fqus_lpxs_fpbs: ∀h,o,G1,G2,L1,L,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L, T2⦄ →
+ ∀L2. ⦃G2, L⦄ ⊢ ⬈*[h] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+/3 width=3 by fpbs_lpxs_trans, fqus_fpbs/ qed.
+
+(* Properties with unbound context-sensitive parallel rt-computation ********)
+
+lemma cpxs_fqus_lpxs_fpbs: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
+ ∀G2,L,T2. ⦃G1, L1, T⦄ ⊐* ⦃G2, L, T2⦄ →
+ ∀L2.⦃G2, L⦄ ⊢ ⬈*[h] L2 → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
+/3 width=5 by cpxs_fqus_fpbs, fpbs_lpxs_trans/ qed.
+
+lemma fpbs_cpxs_tdeq_fqup_lpx_trans: ∀h,o,G1,G3,L1,L3,T1,T3. ⦃G1, L1, T1⦄ ≥ [h, o] ⦃G3, L3, T3⦄ →
+ ∀T4. ⦃G3, L3⦄ ⊢ T3 ⬈*[h] T4 → ∀T5. T4 ≛[h, o] T5 →
+ ∀G2,L4,T2. ⦃G3, L3, T5⦄ ⊐+ ⦃G2, L4, T2⦄ →
+ ∀L2. ⦃G2, L4⦄ ⊢ ⬈[h] L2 → ⦃G1, L1, T1⦄ ≥ [h, o] ⦃G2, L2, T2⦄.
+#h #o #G1 #G3 #L1 #L3 #T1 #T3 #H13 #T4 #HT34 #T5 #HT45 #G2 #L4 #T2 #H34 #L2 #HL42
+@(fpbs_lpx_trans … HL42) -L2 (**) (* full auto too slow *)
+@(fpbs_fqup_trans … H34) -G2 -L4 -T2
+/3 width=3 by fpbs_cpxs_trans, fpbs_tdeq_trans/
+qed-.
+
+(* Advanced properties ******************************************************)
+
+(* Basic_2A1: uses: fpbs_intro_alt *)
lemma fpbs_intro_star: ∀h,o,G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
∀G,L,T0. ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄ →
∀L0. ⦃G, L⦄ ⊢ ⬈*[h] L0 →
∀G2,L2,T2. ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ .
-/3 width=9 by fpbs_intro_fstar, lfpxs_lpxs/ qed.
+/3 width=5 by cpxs_fqus_lpxs_fpbs, fpbs_strap1, fpbq_ffdeq/ qed.
-(* Eliminators with unbound parallel rt-computation on local environments ***)
+(* Advanced inversion lemmas *************************************************)
(* Basic_2A1: uses: fpbs_inv_alt *)
lemma fpbs_inv_star: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄ →
∃∃G,L,L0,T,T0. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T & ⦃G1, L1, T⦄ ⊐* ⦃G, L, T0⦄
& ⦃G, L⦄ ⊢ ⬈*[h] L0 & ⦃G, L0, T0⦄ ≛[h, o] ⦃G2, L2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H
-elim (fpbs_inv_fstar … H) -H #G #L #L0 #T #T0 #HT1 #H10 #HL0 #H02
-elim (lfpxs_inv_lpxs_lfeq … HL0) -HL0 #L3 #HL3 #HL30
-/3 width=11 by lfeq_lfdeq_trans, ex4_5_intro/
+#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1
+[ /2 width=9 by ex4_5_intro/
+| #G1 #G0 #L1 #L0 #T1 #T0 * -G0 -L0 -T0
+ [ #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
+ elim (fquq_cpxs_trans … HT03 … H10) -T0
+ /3 width=9 by fqus_strap2, ex4_5_intro/
+ | #T0 #HT10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
+ /3 width=9 by cpxs_strap2, ex4_5_intro/
+ | #L0 #HL10 #_ * #G3 #L3 #L4 #T3 #T4 #HT13 #H34 #HL34 #H42
+ lapply (lpx_cpxs_trans … HT13 … HL10) -HT13 #HT13
+ elim (lpx_fqus_trans … H34 … HL10) -L0
+ /3 width=9 by lpxs_step_sn, cpxs_trans, ex4_5_intro/
+ | #G0 #L0 #T0 #H10 #_ * #G3 #L3 #L4 #T3 #T4 #HT03 #H34 #HL34 #H42
+ elim (ffdeq_cpxs_trans … H10 … HT03) -T0 #T0 #HT10 #H03
+ elim (ffdeq_fqus_trans … H03 … H34) -G0 -L0 -T3 #G0 #L0 #T3 #H03 #H34
+ elim (ffdeq_lpxs_trans … H34 … HL34) -L3 #L3 #HL03 #H34
+ /3 width=13 by ffdeq_trans, ex4_5_intro/
+ ]
+]
qed-.
(* *)
(**************************************************************************)
-include "basic_2/rt_computation/lfsx_csx.ma".
+include "basic_2/rt_computation/rdsx_csx.ma".
include "basic_2/rt_computation/fpbs_cpx.ma".
include "basic_2/rt_computation/fpbs_csx.ma".
include "basic_2/rt_computation/fsb_fpbg.ma".
#G0 #L0 #T0 #IHu #H10
lapply (fpbs_csx_conf … H10) // -HT1 #HT0
generalize in match IHu; -IHu generalize in match H10; -H10
-@(lfsx_ind … (csx_lfsx … HT0)) -L0
+@(rdsx_ind … (csx_rdsx … HT0)) -L0
#L0 #_ #IHd #H10 #IHu @fsb_intro
#G2 #L2 #T2 * -G2 -L2 -T2 [ -IHd -IHc | -IHu -IHd | ]
[ /4 width=5 by fpbs_fqup_trans, fqu_fqup/
elim (fpbs_cpx_tdneq_trans … H10 … HT02 HnT02) -T0
/3 width=4 by/
| #L2 #HL02 #HnL02 @(IHd … HL02 HnL02) -IHd -HnL02 [ -IHu -IHc | ]
- [ /3 width=3 by fpbs_lfpxs_trans, lfpx_lfpxs/
+ [ /3 width=3 by fpbs_lpxs_trans, lpx_lpxs/
| #G3 #L3 #T3 #H03 #_
- elim (lfpx_fqup_trans … H03 … HL02) -L2 #L4 #T4 #HT04 #H43 #HL43
+ elim (lpx_fqup_trans … H03 … HL02) -L2 #L4 #T4 #HT04 #H43 #HL43
elim (tdeq_dec h o T0 T4) [ -IHc -HT04 #HT04 | -IHu #HnT04 ]
[ elim (tdeq_fqup_trans … H43 … HT04) -T4 #L2 #T4 #H04 #HT43 #HL24
- /4 width=7 by fsb_fpbs_trans, tdeq_lfdeq_lfpx_fpbs, fpbs_fqup_trans/
+ /4 width=7 by fsb_fpbs_trans, tdeq_lfdeq_lpx_fpbs, fpbs_fqup_trans/
| elim (cpxs_tdneq_fwd_step_sn … HT04 HnT04) -HT04 -HnT04 #T2 #T5 #HT02 #HnT02 #HT25 #HT54
elim (fpbs_cpx_tdneq_trans … H10 … HT02 HnT02) -T0 #T0 #HT10 #HnT10 #H02
- /3 width=14 by fpbs_cpxs_tdeq_fqup_lfpx_trans/
+ /3 width=14 by fpbs_cpxs_tdeq_fqup_lpx_trans/
]
]
]
-cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_ffdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
+cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_ffdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_cnx.ma cpxs_cpxs.ma
cpxs_ext.ma
lpxs.ma lpxs_length.ma lpxs_drops.ma lpxs_lfdeq.ma lpxs_ffdeq.ma lpxs_aaa.ma lpxs_lpx.ma lpxs_cpxs.ma lpxs_lpxs.ma
-csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_ffdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_fpbq.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma
+csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_ffdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lpx.ma csx_cnx.ma csx_fpbq.ma csx_cpxs.ma csx_lpxs.ma csx_csx.ma
csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma
rdsx.ma rdsx_length.ma rdsx_drops.ma rdsx_fqup.ma rdsx_lpxs.ma rdsx_csx.ma rdsx_rdsx.ma
-lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma
-fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma
-fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma
+lsubsx.ma lsubsx_rdsx.ma lsubsx_lsubsx.ma
+fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lpxs.ma fpbs_csx.ma fpbs_fpbs.ma
+fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma
fsb.ma fsb_ffdeq.ma fsb_aaa.ma fsb_csx.ma fsb_fpbg.ma
cpms.ma cpms_drops.ma cpms_lsubr.ma cpms_aaa.ma cpms_cpxs.ma
cprs.ma cprs_drops.ma
]
[ { "unbound context-sensitive parallel rst-computation" * } {
[ [ "strongly normalizing for closures" ] "fsb" + "( ≥[?,?] 𝐒⦃?,?,?⦄ )" "fsb_ffdeq" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ]
- [ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lfpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
- [ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
+ [ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
+ [ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
}
]
[ { "unbound context-sensitive parallel rt-computation" * } {
[ [ "refinement for lenvs on selected entries" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
[ [ "strongly normalizing for lenvs on referred entries" ] "rdsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "rdsx_length" + "rdsx_drops" + "rdsx_fqup" + "rdsx_cpxs" + "rdsx_csx" + "rdsx_rdsx" * ]
[ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
- [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_ffdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
- [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
+ [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_ffdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lpxs" + "csx_csx" * ]
[ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_drops" + "lpxs_lfdeq" + "lpxs_ffdeq" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ]
[ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ]
- [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_ffdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
+ [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_ffdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_cnx" + "cpxs_cpxs" * ]
}
]
}
}
]
[ { "context-sensitive parallel r-transition" * } {
- [ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" (* + "lfpr_lfpr" *) * ]
+ [ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ]
[ [ "for binders" ] "cpr_ext" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ]
[ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" + "cpr_cpr" * ]
}
class "italic" { 2 }
(*
+ [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
[ [ "for lenvs on referred entries" ]
"lfpr" + "( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
[ { "evaluation for context-sensitive rt-reduction" * } {
projects / helm.git / commitdiff