From cead5946e630e5357fb26141252e10868c96a14d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 20 Mar 2018 18:18:41 +0100 Subject: [PATCH] update in basic_2 + fpbg completed --- .../basic_2/rt_computation/fpbg_lfpxs.ma | 18 +++++++++++------- .../basic_2/rt_computation/fpbs_lfpxs.ma | 5 ++--- .../basic_2/rt_computation/partial.txt | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 4 files changed, 15 insertions(+), 12 deletions(-) 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 index bbed2be86..d4c447c81 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg_lfpxs.ma @@ -12,13 +12,17 @@ (* *) (**************************************************************************) -include "basic_2/computation/lpxs_ffdeq.ma". -include "basic_2/computation/fpbg_ffdeq.ma". +include "basic_2/rt_computation/fpbs_lfpxs.ma". +include "basic_2/rt_computation/fpbg.ma". -(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES **************************) +(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************) -lemma lpxs_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → - (L1 ≡[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ >≛[h, o] ⦃G, L2, T⦄. -#h #o #G #L1 #L2 #T #H #H0 elim (lpxs_nlleq_inv_step_sn … H … H0) -H -H0 -/4 width=5 by fpb_lpx, lpxs_lleq_fpbs, ex2_3_intro/ +(* Properties with uncounted 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/fpbs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma index c95e8bf9c..3c0e8e372 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbs_lfpxs.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/static/ffdeq_fqup.ma". include "basic_2/static/ffdeq_fqus.ma". include "basic_2/static/ffdeq_ffdeq.ma". include "basic_2/rt_computation/cpxs_fqus.ma". @@ -46,8 +45,8 @@ lemma lfpxs_fpbs_trans: ∀h,o,G1,G2,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, o] ⦃G2 qed-. (* Basic_2A1: uses: lpxs_lleq_fpbs *) -lemma lpxs_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⦄. +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. (* Properties with star-iterated structural successor for closures **********) 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 09efad79b..10c38172d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -7,4 +7,4 @@ csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.ma lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lfpxs.ma fpbs_csx.ma fpbs_fpbs.ma -fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma +fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lfpxs.ma fpbg_fpbs.ma fpbg_fpbg.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 9bf043c34..7ec7cd11c 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 @@ -101,7 +101,7 @@ table { ] *) [ { "uncounted context-sensitive parallel rst-computation" * } { - [ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_fpbs" + "fpbg_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_fpb" + "fpbs_cpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ] } ] -- 2.39.2