From a0462cc68401e561a041f1e567dec40cd522cab8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 25 Oct 2017 19:44:02 +0000 Subject: [PATCH] - exclusion binder in local environments portions updated of: cpxs, lfpxs --- .../basic_2/rt_computation/cpxs_drops.ma | 26 +++++++++---------- .../basic_2/rt_computation/cpxs_lfpx.ma | 6 ++--- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +-- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma index 99a6e3670..172dcc3fb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma @@ -30,9 +30,9 @@ lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 → ] qed. -lemma cpxs_lref: ∀h,I,G,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T → - ∀U. ⬆*[1] T ≡ U → ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈*[h] U. -#h #I #G #K #V #T #i #H @(cpxs_ind … H) -T +lemma cpxs_lref: ∀h,I,G,K,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T → + ∀U. ⬆*[1] T ≡ U → ⦃G, K.ⓘ{I}⦄ ⊢ #⫯i ⬈*[h] U. +#h #I #G #K #T #i #H @(cpxs_ind … H) -T [ /3 width=3 by cpx_cpxs, cpx_lref/ | #T0 #T #_ #HT2 #IH #U #HTU elim (lifts_total T0 (𝐔❴1❵)) @@ -71,15 +71,15 @@ qed-. lemma cpxs_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈*[h] T2 → T2 = #(⫯i) ∨ - ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ⬈*[h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V. + ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈*[h] T & ⬆*[1] T ≡ T2 & L = K.ⓘ{I}. #h #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ #T #T2 #_ #HT2 * [ #H destruct elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ - * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ -| * #I #K #V1 #T1 #Hi #HT1 #H destruct + * /4 width=6 by cpx_cpxs, ex3_3_intro, or_intror/ +| * #I #K #T1 #Hi #HT1 #H destruct elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T - /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/ + /4 width=6 by cpxs_strap1, drops_refl, drops_drop, ex3_3_intro, or_intror/ ] qed-. @@ -103,17 +103,17 @@ qed-. (* Properties with generic relocation ***************************************) (* Basic_2A1: includes: cpxs_lift *) -lemma cpxs_lifts_sn: ∀h,G. d_liftable2_sn (cpxs h G). +lemma cpxs_lifts_sn: ∀h,G. d_liftable2_sn … lifts (cpxs h G). /3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_LTC/ qed-. -lemma cpxs_lifts_bi: ∀h,G. d_liftable2_bi (cpxs h G). -/3 width=9 by cpxs_lifts_sn, d_liftable2_sn_bi/ qed-. +lemma cpxs_lifts_bi: ∀h,G. d_liftable2_bi … lifts (cpxs h G). +/3 width=12 by cpxs_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-. (* Inversion lemmas with generic relocation *********************************) (* Basic_2A1: includes: cpxs_inv_lift1 *) -lemma cpxs_inv_lifts_sn: ∀h,G. d_deliftable2_sn (cpxs h G). +lemma cpxs_inv_lifts_sn: ∀h,G. d_deliftable2_sn … lifts (cpxs h G). /3 width=6 by d2_deliftable_sn_LTC, cpx_inv_lifts_sn/ qed-. -lemma cpxs_inv_lifts_bi: ∀h,G. d_deliftable2_bi (cpxs h G). -/3 width=9 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi/ qed-. +lemma cpxs_inv_lifts_bi: ∀h,G. d_deliftable2_bi … lifts (cpxs h G). +/3 width=12 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi, lifts_inj/ qed-. 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 index 66196f726..73cee4537 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/rt_transition/lfpx_fqup.ma". -include "basic_2/rt_transition/lfpx_lfpx.ma". +include "basic_2/rt_transition/lfpx_cpx.ma". include "basic_2/rt_computation/cpxs_drops.ma". include "basic_2/rt_computation/cpxs_cpxs.ma". @@ -30,8 +30,8 @@ lemma lfpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpx h G). | #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/ -| #I #G #L2 #V #V2 #W2 #i #_ #IH #HVW2 #Y1 #H - elim (lfpx_inv_lref_pair_dx … H) -H #L1 #V1 #HL1 #HV1 +| #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/ 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 c8a9f2774..561a9980b 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 @@ -71,7 +71,6 @@ table { ] } ] -(* class "sky" [ { "rt-computation" * } { (* @@ -114,16 +113,17 @@ table { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) +(* [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] +*) [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } ] -*) class "cyan" [ { "rt-transition" * } { [ { "uncounted rst-transition" * } { -- 2.39.2