From: Ferruccio Guidi Date: Thu, 30 Mar 2017 11:30:39 +0000 (+0000) Subject: - csx_cnx_vector.ma completed X-Git-Tag: make_still_working~471 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c3832abc23bb0907df2deb6751f4a46d213675b7;p=helm.git - csx_cnx_vector.ma completed - refactoring --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma index a28b01e54..0340000b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_etc.ma @@ -5,21 +5,6 @@ include "basic_2/rt_computation/cpxs_cpxs.ma". (* Properties on sn extended parallel reduction for local environments ******) -lemma lpx_cpx_trans: ∀h,G. b_c_transitive … (cpx h G) (λ_.lpx h G). -#h #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2 -[ /2 width=3 by/ -| /3 width=2 by cpx_cpxs, cpx_st/ -| #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12 - elim (lpx_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H - elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct - /4 width=7 by cpxs_delta, cpxs_strap2/ -|4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/ -|5,7,8: /3 width=1 by cpxs_flat, cpxs_ct, cpxs_eps/ -| /4 width=3 by cpxs_zeta, lpx_pair/ -| /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/ -] -qed-. - lemma cpx_bind2: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈[h, o] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. @@ -27,10 +12,6 @@ lemma cpx_bind2: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → (* Advanced properties ******************************************************) -lemma lpx_cpxs_trans: ∀h,o,G. b_rs_transitive … (cpx h o G) (λ_.lpx h o G). -#h #o #G @b_c_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *) -qed-. - lemma cpxs_bind2_dx: ∀h,o,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h, o] V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h, o] T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ⬈*[h, o] ⓑ{a,I}V2.T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma index 5fe697558..c7e8e3dd3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx.ma @@ -45,19 +45,6 @@ lemma csx_intro: ∀h,o,G,L,T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄. /4 width=1 by SN_intro/ qed. -lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃⋆s⦄. -#h #o #G #L #s elim (deg_total h o s) -#d generalize in match s; -s elim d -d -[ #s1 #Hs1 @csx_intro #X #H #HX elim HX -HX - elim (cpx_inv_sort1 … H) -H #H destruct // - /3 width=3 by tdeq_sort, deg_next/ -| #d #IH #s #Hsd lapply (deg_next_SO … Hsd) -Hsd - #Hsd @csx_intro #X #H #HX - elim (cpx_inv_sort1 … H) -H #H destruct /2 width=1 by/ - elim HX // -] -qed. - (* Basic forward lemmas *****************************************************) fact csx_fwd_pair_sn_aux: ∀h,o,G,L,U. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃U⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma index 8f9268fab..ea34597b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx.ma @@ -22,3 +22,16 @@ include "basic_2/rt_computation/csx.ma". (* Basic_1: was just: sn3_nf2 *) lemma cnx_csx: ∀h,o,G,L,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. /2 width=1 by NF_to_SN/ qed. + +(* Advanced properties ******************************************************) + +lemma csx_sort: ∀h,o,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃⋆s⦄. +#h #o #G #L #s elim (deg_total h o s) +#d generalize in match s; -s elim d -d +[ /3 width=3 by cnx_csx, cnx_sort/ +| #d #IH #s #Hsd lapply (deg_next_SO … Hsd) -Hsd + #Hsd @csx_intro #X #H #HX + elim (cpx_inv_sort1 … H) -H #H destruct /2 width=1 by/ + elim HX -HX // +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma new file mode 100644 index 000000000..ef3d1c20b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* STRONGLY NORMALIZING TERM VECTORS FOR UNCOUNTED 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_cnx.ma". +include "basic_2/rt_computation/csx_cpxs.ma". +include "basic_2/rt_computation/csx_vector.ma". + +(* Properties with normal terms for uncounted parallel rt-transition ********) + +(* Basic_1: was just: sn3_appls_lref *) +lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃T⦄ → + ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.T⦄. +#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs +[ #_ normalize in ⊢ (?????%); /2 width=1/ +| #V #Vs #IHV #H + elim (csxv_inv_cons … H) -H #HV #HVs + @csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs + #X #H #H0 + lapply (cpxs_fwd_cnx_vector … o … H) -H // -H1T -H2T #H + elim (H0) -H0 // +] +qed. + +(* Advanced properties ******************************************************) + +lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Vs⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⒶVs.⋆s⦄. +#h #o #G #L #s elim (deg_total h o s) +#d generalize in match s; -s elim d -d +[ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ +| #d #IHd #s #Hd #Vs elim Vs -Vs /2 width=1 by/ + #V #Vs #IHVs #HVVs + elim (csxv_inv_cons … HVVs) #HV #HVs + @csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ + #X #H #H0 + elim (cpxs_fwd_sort_vector … o … H) -H #H + [ elim H0 -H0 // + | -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s))) + /3 width=1 by cpxs_flat_dx, deg_next_SO/ + ] +] +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 index 0c2f894b1..2cfbc1a3f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_lfpx.ma @@ -13,12 +13,11 @@ (**************************************************************************) include "basic_2/rt_computation/cpxs_lfpx.ma". -include "basic_2/rt_computation/csx_drops.ma". include "basic_2/rt_computation/csx_cpxs.ma". (* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) -(* Advanced properties ******************************************************) +(* Properties with uncounted 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⦄ → @@ -27,6 +26,8 @@ lemma csx_lfpx_conf: ∀h,o,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma new file mode 100644 index 000000000..83c8fd43e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_simple_theq.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/theq_simple.ma". +include "basic_2/syntax/theq_theq.ma". +include "basic_2/rt_transition/cpx_simple.ma". +include "basic_2/rt_computation/cpxs.ma". +include "basic_2/rt_computation/csx_csx.ma". + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) + +(* Properties with head equivalence for terms *******************************) + +(* Basic_1: was just: sn3_appl_appl *) +(* Basic_2A1: was: csx_appl_simple_tsts *) +lemma csx_appl_simple_theq: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) → + 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T1⦄. +#h #o #G #L #V #H @(csx_ind … H) -V +#V #_ #IHV #T1 #H @(csx_ind … H) -T1 +#T1 #H1T1 #IHT1 #H2T1 #H3T1 +@csx_intro #X #HL #H +elim (cpx_inv_appl1_simple … HL) -HL // +#V0 #T0 #HLV0 #HLT10 #H0 destruct +elim (tdneq_inv_pair … H) -H +[ #H elim H -H // +| -IHT1 #HV0 + @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 + @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ +| -IHV -H1T1 #H1T10 + @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0 + elim (theq_dec h o T1 T0) #H2T10 + [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, theq_canc_sn, simple_theq_repl_dx/ + | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ + ] +] +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma deleted file mode 100644 index 83c8fd43e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq.ma +++ /dev/null @@ -1,48 +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/syntax/theq_simple.ma". -include "basic_2/syntax/theq_theq.ma". -include "basic_2/rt_transition/cpx_simple.ma". -include "basic_2/rt_computation/cpxs.ma". -include "basic_2/rt_computation/csx_csx.ma". - -(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) - -(* Properties with head equivalence for terms *******************************) - -(* Basic_1: was just: sn3_appl_appl *) -(* Basic_2A1: was: csx_appl_simple_tsts *) -lemma csx_appl_simple_theq: ∀h,o,G,L,V. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃V⦄ → ∀T1. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ⩳[h, o] T2 → ⊥) → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T2⦄) → - 𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃ⓐV.T1⦄. -#h #o #G #L #V #H @(csx_ind … H) -V -#V #_ #IHV #T1 #H @(csx_ind … H) -T1 -#T1 #H1T1 #IHT1 #H2T1 #H3T1 -@csx_intro #X #HL #H -elim (cpx_inv_appl1_simple … HL) -HL // -#V0 #T0 #HLV0 #HLT10 #H0 destruct -elim (tdneq_inv_pair … H) -H -[ #H elim H -H // -| -IHT1 #HV0 - @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10 - @IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/ -| -IHV -H1T1 #H1T10 - @(csx_cpx_trans … (ⓐV.T0)) /2 width=1 by cpx_flat/ -HLV0 - elim (theq_dec h o T1 T0) #H2T10 - [ @IHT1 -IHT1 /4 width=5 by cpxs_strap2, cpxs_strap1, theq_canc_sn, simple_theq_repl_dx/ - | -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma index 2c8dda2dc..55146e3c2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_theq_vector.ma @@ -11,46 +11,25 @@ (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) - +(* include "basic_2/computation/gcp_cr.ma". -include "basic_2/computation/cpxs_theq_vector.ma". -include "basic_2/computation/csx_lpx.ma". -include "basic_2/computation/csx_vector.ma". - -(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************) +*) +include "basic_2/rt_computation/cpxs_theq_vector.ma". +include "basic_2/rt_computation/csx_vector.ma". +include "basic_2/rt_computation/csx_theq.ma". +include "basic_2/rt_computation/csx_lfpx.ma". -(* Advanced properties ******************************************************) - -(* Basic_1: was just: sn3_appls_lref *) -lemma csx_applv_cnx: ∀h,o,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → - ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.T. -#h #o #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) -#V #Vs #IHV #H -elim (csxv_inv_cons … H) -H #HV #HVs -@csx_appl_simple_theq /2 width=1 by applv_simple/ -IHV -HV -HVs -#X #H #H0 -lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H -elim (H0) -H0 // -qed. +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) -lemma csx_applv_sort: ∀h,o,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] Vs → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.⋆s. -#h #o #G #L #s elim (deg_total h o s) -#d generalize in match s; -s @(nat_ind_plus … d) -d [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ] -#d #IHd #s #Hkd lapply (deg_next_SO … Hkd) -Hkd -#Hkd #Vs elim Vs -Vs /2 width=1 by/ -#V #Vs #IHVs #HVVs -elim (csxv_inv_cons … HVVs) #HV #HVs -@csx_appl_simple_theq /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs -#X #H #H0 -elim (cpxs_fwd_sort_vector … H) -H #H -[ elim H0 -H0 // -| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h s))) /2 width=1 by cpxs_flat_dx/ -] -qed. +(* Vector form of properties with head equivalence for terms ****************) +(* +*) +(* +*) (* Basic_1: was just: sn3_appls_beta *) -lemma csx_applv_beta: ∀h,o,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓓ{a}ⓝW.V.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs. ⓐV.ⓛ{a}W.T. +lemma csx_applv_beta: ∀h,o,p,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs.ⓓ{p}ⓝW.V.T → + ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs. ⓐV.ⓛ{p}W.T. #h #o #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ #V0 #Vs #IHV #V #W #T #H1T lapply (csx_fwd_pair_sn … H1T) #HV0 @@ -65,7 +44,7 @@ qed. lemma csx_applv_delta: ∀h,o,I,G,L,K,V1,i. ⬇[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⬆[0, i + 1] V1 ≡ V2 → - ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, o] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, o] (ⒶVs.#i). + ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h, o] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬈*[h, o] (ⒶVs.#i). #h #o #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs [ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/ | #V #Vs #IHV #H1T @@ -82,8 +61,8 @@ qed. (* Basic_1: was just: sn3_appls_abbr *) lemma csx_applv_theta: ∀h,o,a,G,L,V1b,V2b. ⬆[0, 1] V1b ≡ V2b → - ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⓓ{a}V.ⒶV2b.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶV1b.ⓓ{a}V.T. + ∀V,T. ⦃G, L⦄ ⊢ ⬈*[h, o] ⓓ{a}V.ⒶV2b.T → + ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶV1b.ⓓ{a}V.T. #h #o #a #G #L #V1b #V2b * -V1b -V2b /2 width=1 by/ #V1b #V2b #V1 #V2 #HV12 #H generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1 @@ -100,8 +79,8 @@ elim (cpxs_fwd_theta_vector … (V2@V2b) … H1) -H1 /2 width=1 by liftv_cons/ - qed. (* Basic_1: was just: sn3_appls_cast *) -lemma csx_applv_cast: ∀h,o,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.T → - ⦃G, L⦄ ⊢ ⬊*[h, o] ⒶVs.ⓝW.T. +lemma csx_applv_cast: ∀h,o,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs.W → ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs.T → + ⦃G, L⦄ ⊢ ⬈*[h, o] ⒶVs.ⓝW.T. #h #o #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ #V #Vs #IHV #W #T #H1W #H1T lapply (csx_fwd_pair_sn … H1W) #HV 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 5fa047a73..6c76c4bc8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,4 +1,4 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma -csx.ma csx_simple.ma csx_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma -csx_vector.ma +csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma +csx_vector.ma csx_cnx_vector.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 8dafdbd32..d2d7a0e35 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 @@ -113,8 +113,8 @@ table { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] }