From: Ferruccio Guidi Date: Tue, 29 May 2018 19:23:00 +0000 (+0200) Subject: commit completed in basic_2 X-Git-Tag: make_still_working~314 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=a40dbe4ef22688b1e9d8b31a7f10150bfc28e111 commit completed in basic_2 + fpbs, fpbg, fsb reconstructed --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/cpxs_lfpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/cpxs_lfpx.etc new file mode 100644 index 000000000..063e9d8b2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/cpxs_lfpx.etc @@ -0,0 +1,83 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/csx_lfpx.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/csx_lfpx.etc new file mode 100644 index 000000000..ca3d59727 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/csx_lfpx.etc @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/csx_lfpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/csx_lfpxs.etc new file mode 100644 index 000000000..e9fdd7241 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/csx_lfpxs.etc @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/fpbg_lfpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/fpbg_lfpxs.etc new file mode 100644 index 000000000..1cfc428ff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/fpbg_lfpxs.etc @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/fpbs_lfpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/fpbs_lfpxs.etc new file mode 100644 index 000000000..87818e45b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/fpbs_lfpxs.etc @@ -0,0 +1,114 @@ +(**************************************************************************) +(* ___ *) +(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma index 9f27d5fe4..b69f83a24 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_aaa.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -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 **************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma index 3460879b1..c6206f82f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma @@ -54,6 +54,7 @@ lemma fqus_cpxs_trans: ∀h,b,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h] U2 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⦄. @@ -86,6 +87,7 @@ lemma fqu_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ] 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⦄. @@ -96,6 +98,7 @@ lemma fquq_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ] 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⦄. @@ -108,6 +111,7 @@ lemma fqup_cpxs_trans_tdneq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b ] 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⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma deleted file mode 100644 index ed187cce6..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma +++ /dev/null @@ -1,97 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma index 5e17096f6..f5cefda3a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lpx.ma @@ -12,13 +12,14 @@ (* *) (**************************************************************************) -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 @@ -40,3 +41,43 @@ qed-. 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma index 4235b4e30..ae05d817e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_theq.ma @@ -15,7 +15,7 @@ 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 **************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma index e8d85a309..90480a605 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -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 ************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma index d618a2437..30f35f70f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx_vector.ma @@ -15,7 +15,7 @@ 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 *****) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma index b238a54d0..022a4d381 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fpbq.ma @@ -15,7 +15,7 @@ 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 ************) @@ -25,5 +25,5 @@ include "basic_2/rt_computation/csx_lfpx.ma". 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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma deleted file mode 100644 index 353f9b84f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma +++ /dev/null @@ -1,99 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpxs.ma deleted file mode 100644 index 9f286eef3..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpxs.ma +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma new file mode 100644 index 000000000..9192f4fa5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpx.ma @@ -0,0 +1,99 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma new file mode 100644 index 000000000..cc9ae833d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lpxs.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma deleted file mode 100644 index 1cfc428ff..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma new file mode 100644 index 000000000..b33d67dea --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lpxs.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma index 82c5eb62a..78c6b2ef7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs.ma @@ -67,9 +67,9 @@ lemma ffdeq_fpbs_trans: ∀h,o,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, o] ⦃G2, L2 ∀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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma deleted file mode 100644 index 87818e45b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma +++ /dev/null @@ -1,114 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma index 6f1c51695..97ff31565 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lpxs.ma @@ -12,29 +12,100 @@ (* *) (**************************************************************************) -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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma index 6d25d649b..d1cc73d89 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fsb_csx.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -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". @@ -34,7 +34,7 @@ lemma csx_fsb_fpbs: ∀h,o,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ #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/ @@ -42,15 +42,15 @@ generalize in match IHu; -IHu generalize in match H10; -H10 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/ ] ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 4092f79d3..1708bccc6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,12 +1,12 @@ -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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index f40c15814..40c116a41 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -85,19 +85,18 @@ table { ] [ { "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" * ] } ] } @@ -110,7 +109,7 @@ table { } ] [ { "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" * ] } @@ -290,6 +289,7 @@ class "capitalize italic" { 0 1 } 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" * } {