From 5902d6da146ca78b0ed5d062e3968f52868147c5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 6 Aug 2014 18:52:13 +0000 Subject: [PATCH 1/1] - some renaming and minor updates --- matita/matita/contribs/lambdadelta/Makefile | 2 +- .../lambdadelta/basic_2/computation/acp_cr.ma | 20 +-- .../lambdadelta/basic_2/computation/cprs.ma | 2 +- .../basic_2/computation/cpxs_tstc_vector.ma | 28 ++-- .../lambdadelta/basic_2/computation/csx.ma | 2 +- .../basic_2/computation/csx_tstc_vector.ma | 40 +++--- .../basic_2/computation/csx_vector.ma | 2 +- .../basic_2/computation/{cpds.ma => scpds.ma} | 36 ++--- .../computation/{cpds_aaa.ma => scpds_aaa.ma} | 6 +- .../{cpds_lift.ma => scpds_lift.ma} | 8 +- .../{cpds_cpds.ma => scpds_scpds.ma} | 42 +++--- .../lambdadelta/basic_2/dynamic/lsubsv.ma | 2 +- .../basic_2/dynamic/lsubsv_lstas.ma | 6 +- .../basic_2/dynamic/lsubsv_lsuba.ma | 6 +- .../{lsubsv_cpds.ma => lsubsv_scpds.ma} | 6 +- .../lambdadelta/basic_2/dynamic/lsubsv_snv.ma | 12 +- .../basic_2/dynamic/{hsnv.ma => shnv.ma} | 24 ++-- .../dynamic/{hsnv_aaa.ma => shnv_aaa.ma} | 10 +- .../lambdadelta/basic_2/dynamic/snv.ma | 2 +- .../lambdadelta/basic_2/dynamic/snv_aaa.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_lift.ma | 14 +- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 42 +++--- .../lambdadelta/basic_2/dynamic/snv_lstas.ma | 6 +- .../basic_2/dynamic/snv_lstas_lpr.ma | 14 +- .../basic_2/dynamic/snv_preserve.ma | 6 + .../dynamic/{snv_cpes.ma => snv_scpes.ma} | 134 +++++++++--------- .../basic_2/equivalence/cpes_cpes.ma | 62 -------- .../basic_2/equivalence/{cpes.ma => scpes.ma} | 32 ++--- .../equivalence/{cpes_aaa.ma => scpes_aaa.ma} | 14 +- .../{cpes_cpcs.ma => scpes_cpcs.ma} | 22 +-- .../basic_2/equivalence/scpes_scpes.ma | 62 ++++++++ .../lambdadelta/basic_2/etc/snv_preserve.etc | 6 - .../basic_2/grammar/term_vector.ma | 10 +- .../basic_2/grammar/tstc_vector.ma | 2 +- .../basic_2/multiple/lifts_vector.ma | 4 +- .../{snappls_2.ma => snapplvector_2.ma} | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 12 +- 38 files changed, 358 insertions(+), 358 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/computation/{cpds.ma => scpds.ma} (53%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{cpds_aaa.ma => scpds_aaa.ma} (87%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{cpds_lift.ma => scpds_lift.ma} (87%) rename matita/matita/contribs/lambdadelta/basic_2/computation/{cpds_cpds.ma => scpds_scpds.ma} (61%) rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{lsubsv_cpds.ma => lsubsv_scpds.ma} (85%) rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{hsnv.ma => shnv.ma} (74%) rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{hsnv_aaa.ma => shnv_aaa.ma} (82%) rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{snv_cpes.ma => snv_scpes.ma} (60%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpes.ma rename matita/matita/contribs/lambdadelta/basic_2/equivalence/{cpes.ma => scpes.ma} (52%) rename matita/matita/contribs/lambdadelta/basic_2/equivalence/{cpes_aaa.ma => scpes_aaa.ma} (75%) rename matita/matita/contribs/lambdadelta/basic_2/equivalence/{cpes_cpcs.ma => scpes_cpcs.ma} (66%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma rename matita/matita/contribs/lambdadelta/basic_2/notation/functions/{snappls_2.ma => snapplvector_2.ma} (97%) diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 15c38d009..5dc025fc3 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -247,7 +247,7 @@ trim: $(TRIMS:%=%.trimmed) # contrib #################################################################### contrib: - @echo " TAR -czf $(CONTRIB).tar.gz root *.ma" + @echo " TAR -czf $(CONTRIB).tar.gz root $(XPACKAGES)" $(H)tar -czf $(CONTRIB).tar.gz root $(XMAS) ############################################################################## diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index a7281d511..f5b3f6a05 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -124,22 +124,22 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) | #H @(cp2 … H1RP … k) @(s1 … IHA) // ] | #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H - elim (lifts_inv_appls1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct + elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct lapply (s1 … IHB … HB) #HV0 @(s2 … IHA … (V0 @ V0s)) /3 width=14 by rp_liftsv_all, acp_lifts, cp0, lifts_simple_dx, conj/ | #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H - elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct - @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_appls, lifts_flat, lifts_bind/ + @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/ | #G #L #Vs #HVs #k #L0 #V0 #X #des #HB #HL0 #H - elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct >(lifts_inv_sort1 … HY) -Y lapply (s1 … IHB … HB) #HV0 @(s4 … IHA … (V0 @ V0s)) /3 width=7 by rp_liftsv_all, conj/ | #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H - elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0 >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02 @@ -147,23 +147,23 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) elim (lift_total W1 0 (i0 + 1)) #W2 #HW12 elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2 >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2 - @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_appls/ + @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/ | #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H - elim (lifts_inv_appls1 … H) -H #V10s #Y #HV10s #HY #H destruct + elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct elim (lift_total V10 0 1) #V20 #HV120 elim (liftv_total 0 1 V10s) #V20s #HV120s @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/ @(HA … (des + 1)) /2 width=2 by drops_skip/ [ @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/ - | @lifts_appls // + | @lifts_applv // elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s >(liftv_mono … HV12s … HV10s) -V1s // ] | #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H - elim (lifts_inv_appls1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct - @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_appls/ + @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index e4c5460d0..a8eb52ab5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -140,5 +140,5 @@ qed-. pr1_head_1 pr1_head_2 pr1_comp clear_pr3_trans pr3_cflat pr3_gen_bind pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12 - pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind + pr3_iso_appl_bind pr3_iso_applv_appl_bind pr3_iso_applv_bind *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma index 425a7f82a..bb225f6c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma @@ -20,7 +20,7 @@ include "basic_2/computation/cpxs_tstc.ma". (* Vector form of forward lemmas involving same top term constructor ********) -(* Basic_1: was just: nf2_iso_appls_lref *) +(* Basic_1: was just: nf2_iso_applv_lref *) lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≂ U. #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) @@ -29,10 +29,10 @@ elim (cpxs_inv_appl1 … H) -H * [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair/ | #a #W0 #T0 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tstc_inv_bind_appls_simple … HT0) // + elim (tstc_inv_bind_applv_simple … HT0) // | #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU lapply (IHVs … HT0) -IHVs -HT0 #HT0 - elim (tstc_inv_bind_appls_simple … HT0) // + elim (tstc_inv_bind_applv_simple … HT0) // ] qed-. @@ -44,14 +44,14 @@ elim (cpxs_inv_appl1 … H) -H * [ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ | #a #W1 #T1 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_appls_simple … HT1) // + [ elim (tstc_inv_bind_applv_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ ] | #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_appls_simple … HT1) // + [ elim (tstc_inv_bind_applv_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ @@ -60,7 +60,7 @@ elim (cpxs_inv_appl1 … H) -H * qed-. -(* Basic_1: was just: pr3_iso_appls_beta *) +(* Basic_1: was just: pr3_iso_applv_beta *) lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U → ⒶVs. ⓐV. ⓛ{a}W. T ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[h, g] U. #h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ @@ -69,14 +69,14 @@ elim (cpxs_inv_appl1 … H) -H * [ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ | #b #W1 #T1 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_appls_simple … HT1) // + [ elim (tstc_inv_bind_applv_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ ] | #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU elim (IHVs … HT1) -IHVs -HT1 #HT1 - [ elim (tstc_inv_bind_appls_simple … HT1) // + [ elim (tstc_inv_bind_applv_simple … HT1) // | @or_intror (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ @@ -94,14 +94,14 @@ elim (cpxs_inv_appl1 … H) -H * [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/ | #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_appls_simple … HT0) // + [ elim (tstc_inv_bind_applv_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/ ] | #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_appls_simple … HT0) // + [ elim (tstc_inv_bind_applv_simple … HT0) // | @or_intror -i (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/ @@ -109,7 +109,7 @@ elim (cpxs_inv_appl1 … H) -H * ] qed-. -(* Basic_1: was just: pr3_iso_appls_abbr *) +(* Basic_1: was just: pr3_iso_applv_abbr *) lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U → ⒶV1s. ⓓ{a}V. T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U. @@ -158,7 +158,7 @@ elim (cpxs_inv_appl1 … H) -H * ] qed-. -(* Basic_1: was just: pr3_iso_appls_cast *) +(* Basic_1: was just: pr3_iso_applv_cast *) lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U → ∨∨ ⒶVs. ⓝW. T ≂ U | ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U @@ -168,7 +168,7 @@ lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡ elim (cpxs_inv_appl1 … H) -H * [ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/ | #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_appls_simple … HT0) // + [ elim (tstc_inv_bind_applv_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/ @@ -178,7 +178,7 @@ elim (cpxs_inv_appl1 … H) -H * ] | #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0 - [ elim (tstc_inv_bind_appls_simple … HT0) // + [ elim (tstc_inv_bind_applv_simple … HT0) // | @or3_intro1 -W (**) (* explicit constructor *) @(cpxs_trans … HU) -U @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma index cd28a524b..426ae47fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma @@ -129,5 +129,5 @@ lemma csx_fwd_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T → sn3_cdelta sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr - sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind + sn3_appl_applv sn3_bind sn3_appl_bind sn3_applv_bind *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma index 765bece71..736b21f3b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma @@ -21,26 +21,26 @@ include "basic_2/computation/csx_vector.ma". (* Advanced properties ******************************************************) -(* Basic_1: was just: sn3_appls_lref *) -lemma csx_appls_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → +(* Basic_1: was just: sn3_applv_lref *) +lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T. #h #g #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_tstc /2 width=1 by appls_simple/ -IHV -HV -HVs +@csx_appl_simple_tstc /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. -lemma csx_appls_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k. +lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k. #h #g #G #L #k elim (deg_total h g k) -#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_appls_cnx, cnx_sort, simple_atom/ ] +#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ] #l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl #Hkl #Vs elim Vs -Vs /2 width=1 by/ #V #Vs #IHVs #HVVs elim (csxv_inv_cons … HVVs) #HV #HVs -@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_atom/ -IHVs -HV -HVs +@csx_appl_simple_tstc /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 // @@ -48,14 +48,14 @@ elim (cpxs_fwd_sort_vector … H) -H #H ] qed. -(* Basic_1: was just: sn3_appls_beta *) -lemma csx_appls_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T → +(* Basic_1: was just: sn3_applv_beta *) +lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T. #h #g #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 lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_flat/ -IHV -HV0 -H2T +@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T #X #H #H0 elim (cpxs_fwd_beta_vector … H) -H #H [ -H1T elim H0 -H0 // @@ -63,7 +63,7 @@ elim (cpxs_fwd_beta_vector … H) -H #H ] qed. -lemma csx_appls_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → +lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → ∀V2. ⇧[0, i + 1] V1 ≡ V2 → ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i). #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs @@ -71,7 +71,7 @@ lemma csx_appls_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → | #V #Vs #IHV #H1T lapply (csx_fwd_pair_sn … H1T) #HV lapply (csx_fwd_flat_dx … H1T) #H2T - @csx_appl_simple_tstc /2 width=1 by appls_simple, simple_atom/ -IHV -HV -H2T + @csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T #X #H #H0 elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H [ -H1T elim H0 -H0 // @@ -80,8 +80,8 @@ lemma csx_appls_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → ] qed. -(* Basic_1: was just: sn3_appls_abbr *) -lemma csx_appls_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → +(* Basic_1: was just: sn3_applv_abbr *) +lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T. #h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/ @@ -99,15 +99,15 @@ elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ - ] qed. -(* Basic_1: was just: sn3_appls_cast *) -lemma csx_appls_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T → +(* Basic_1: was just: sn3_applv_cast *) +lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T. #h #g #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 lapply (csx_fwd_flat_dx … H1W) #H2W lapply (csx_fwd_flat_dx … H1T) #H2T -@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_flat/ -IHV -HV -H2W -H2T +@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T #X #H #H0 elim (cpxs_fwd_cast_vector … H) -H #H [ -H1W -H1T elim H0 -H0 // @@ -119,11 +119,11 @@ qed. theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T). #h #g @mk_acr // [ /2 width=8 by csx_lift/ -| /3 width=1 by csx_appls_cnx/ -|3,4,7: /2 width=1 by csx_appls_beta, csx_appls_sort, csx_appls_cast/ -| /2 width=7 by csx_appls_delta/ +| /3 width=1 by csx_applv_cnx/ +|3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ +| /2 width=7 by csx_applv_delta/ | #G #L #V1s #V2s #HV12s #a #V #T #H #HV - @(csx_appls_theta … HV12s) -HV12s + @(csx_applv_theta … HV12s) -HV12s @csx_abbr // ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma index bd23ff8b6..733666659 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_vector.ma @@ -32,7 +32,7 @@ normalize // qed-. (* Basic forward lemmas *****************************************************) -lemma csx_fwd_appls: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T → +lemma csx_fwd_applv: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T → ⦃G, L⦄ ⊢ ⬊*[h, g] Vs ∧ ⦃G, L⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #T #Vs elim Vs -Vs /2 width=1/ #V #Vs #IHVs #HVs diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds.ma similarity index 53% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/scpds.ma index a2eb23483..29a942fec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds.ma @@ -17,41 +17,41 @@ include "basic_2/static/da.ma". include "basic_2/unfold/lstas.ma". include "basic_2/computation/cprs.ma". -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) +(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************) -definition cpds: ∀h. sd h → nat → relation4 genv lenv term term ≝ - λh,g,l2,G,L,T1,T2. - ∃∃T,l1. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ➡* T2. +definition scpds: ∀h. sd h → nat → relation4 genv lenv term term ≝ + λh,g,l2,G,L,T1,T2. + ∃∃T,l1. l2 ≤ l1 & ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 & ⦃G, L⦄ ⊢ T1 •*[h, l2] T & ⦃G, L⦄ ⊢ T ➡* T2. -interpretation "decomposed extended parallel computation (term)" - 'DPRedStar h g l G L T1 T2 = (cpds h g l G L T1 T2). +interpretation "stratified decomposed parallel computation (term)" + 'DPRedStar h g l G L T1 T2 = (scpds h g l G L T1 T2). (* Basic properties *********************************************************) -lemma sta_cprs_cpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T → - ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 1] T2. +lemma sta_cprs_scpds: ∀h,g,G,L,T1,T,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h] T → + ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 1] T2. /3 width=6 by sta_lstas, ex4_2_intro/ qed. -lemma lstas_cpds: ∀h,g,G,L,T1,T2,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → - ∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l2] T2. +lemma lstas_scpds: ∀h,g,G,L,T1,T2,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → + ∀l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l2] T2. /2 width=6 by ex4_2_intro/ qed. -lemma cprs_cpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 → - ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2. +lemma cprs_scpds: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l → ⦃G, L⦄ ⊢ T1 ➡* T2 → + ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2. /2 width=6 by lstar_O, ex4_2_intro/ qed. -lemma cpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g, 0] T. -/2 width=2 by cprs_cpds/ qed. +lemma scpds_refl: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ T •*➡*[h, g, 0] T. +/2 width=2 by cprs_scpds/ qed. -lemma cpds_strap1: ∀h,g,G,L,T1,T,T2,l. - ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2. +lemma scpds_strap1: ∀h,g,G,L,T1,T,T2,l. + ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l] T2. #h #g #G #L #T1 #T #T2 #l * /3 width=8 by cprs_strap1, ex4_2_intro/ qed. (* Basic forward lemmas *****************************************************) -lemma cpds_fwd_cprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2 → - ⦃G, L⦄ ⊢ T1 ➡* T2. +lemma scpds_fwd_cprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, 0] T2 → + ⦃G, L⦄ ⊢ T1 ➡* T2. #h #g #G #L #T1 #T2 * #T #l #_ #_ #H lapply (lstas_inv_O … H) -l -H #H destruct // diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_aaa.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/scpds_aaa.ma index 8cc7d146e..ad534204f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_aaa.ma @@ -14,12 +14,12 @@ include "basic_2/unfold/lstas_aaa.ma". include "basic_2/computation/cpxs_aaa.ma". -include "basic_2/computation/cpds.ma". +include "basic_2/computation/scpds.ma". -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) +(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************) (* Properties on atomic arity assignment for terms **************************) -lemma cpds_aaa_conf: ∀h,g,G,L,l. Conf3 … (aaa G L) (cpds h g l G L). +lemma scpds_aaa_conf: ∀h,g,G,L,l. Conf3 … (aaa G L) (scpds h g l G L). #h #g #G #L #l #A #T #HT #U * /3 width=6 by lstas_aaa_conf, cprs_aaa_conf/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_lift.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/scpds_lift.ma index ad37046ed..794e5c60e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_lift.ma @@ -15,19 +15,19 @@ include "basic_2/static/da_lift.ma". include "basic_2/unfold/lstas_lift.ma". include "basic_2/computation/cprs_lift.ma". -include "basic_2/computation/cpds.ma". +include "basic_2/computation/scpds.ma". -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) +(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************) (* Relocation properties ****************************************************) -lemma cpds_lift: ∀h,g,G,l. l_liftable (cpds h g l G). +lemma scpds_lift: ∀h,g,G,l. l_liftable (scpds h g l G). #h #g #G #l2 #K #T1 #T2 * #T #l1 #Hl21 #Hl1 #HT1 #HT2 #L #s #d #e elim (lift_total T d e) /3 width=15 by cprs_lift, da_lift, lstas_lift, ex4_2_intro/ qed. -lemma cpds_inv_lift1: ∀h,g,G,l. l_deliftable_sn (cpds h g l G). +lemma scpds_inv_lift1: ∀h,g,G,l. l_deliftable_sn (scpds h g l G). #h #g #G #l2 #L #U1 #U2 * #U #l1 #Hl21 #Hl1 #HU1 #HU2 #K #s #d #e #HLK #T1 #HTU1 lapply (da_inv_lift … Hl1 … HLK … HTU1) -Hl1 #Hl1 elim (lstas_inv_lift1 … HU1 … HLK … HTU1) -U1 #T #HTU #HT1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma similarity index 61% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma index d09fe1ebb..1acbf9398 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/scpds_scpds.ma @@ -15,15 +15,15 @@ include "basic_2/unfold/lstas_lstas.ma". include "basic_2/computation/lprs_cprs.ma". include "basic_2/computation/cpxs_cpxs.ma". -include "basic_2/computation/cpds.ma". +include "basic_2/computation/scpds.ma". -(* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) +(* STRATIFIED DECOMPOSED PARALLEL COMPUTATION ON TERMS **********************) (* Advanced properties ******************************************************) -lemma cpds_strap2: ∀h,g,G,L,T1,T,T2,l1,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1+1 → - ⦃G, L⦄ ⊢ T1 •[h] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] T2 → - ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l+1] T2. +lemma scpds_strap2: ∀h,g,G,L,T1,T,T2,l1,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1+1 → + ⦃G, L⦄ ⊢ T1 •[h] T → ⦃G, L⦄ ⊢ T •*➡*[h, g, l] T2 → + ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l+1] T2. #h #g #G #L #T1 #T #T2 #l1 #l #Hl1 #HT1 * #T0 #l0 #Hl0 #HTl0 #HT0 #HT02 lapply (da_sta_conf … HT1 … Hl1) (plus_minus_m_m l1 1) in Hl1; // -H1 #Hl1 lapply (IH1 … HV1 … Hl1 … HV12 … HL12) -HV1 -Hl1 -HV12 [ /2 by fqup_fpbg/ ] lapply (IH1 … Hl0 … HW2 … HL12) -Hl0 /2 width=1 by fqup_fpbg/ -HW diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma index d8fb8d161..b0f1f88f4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/multiple/fqus_alt.ma". -include "basic_2/computation/cpds_lift.ma". +include "basic_2/computation/scpds_lift.ma". include "basic_2/dynamic/snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -40,12 +40,12 @@ lemma snv_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ T ¡[h, g] → ∀L,s,d,e. ⇩[s, d elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct elim (lift_total W0 d e) #W1 #HW01 elim (lift_total U0 (d+1) e) #U1 #HU01 - @(snv_appl … a … W1 … U1 l) [1,2,3: /2 width=10 by cpds_lift/ ] -IHV -IHT - @(cpds_lift … HTU0 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typechecker failure *) + @(snv_appl … a … W1 … U1 l) [1,2,3: /2 width=10 by scpds_lift/ ] -IHV -IHT + @(scpds_lift … HTU0 … HLK … HTU) /2 width=1 by lift_bind/ (**) (* full auto raises typechecker failure *) | #G #K #V #T #U0 #_ #_ #HVU0 #HTU0 #IHV #IHT #L #s #d #e #HLK #X #H elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct elim (lift_total U0 d e) - /3 width=12 by snv_cast, cprs_lift, cpds_lift/ + /3 width=12 by snv_cast, cprs_lift, scpds_lift/ ] qed. @@ -66,15 +66,15 @@ lemma snv_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ U ¡[h, g] → ∀K,s,d,e. ⇩[ /4 width=5 by snv_bind, drop_skip/ | #a #G #L #W #W1 #U #U1 #l #_ #_ #HW1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct - elim (cpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0 - elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0 + elim (scpds_inv_lift1 … HW1 … HLK … HVW) -HW1 #W0 #HW01 #HVW0 + elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #H #HTU0 elim (lift_inv_bind2 … H) -H #Y #U0 #HY #HU01 #H destruct lapply (lift_inj … HY … HW01) -HY #H destruct /3 width=6 by snv_appl/ | #G #L #W #U #U1 #_ #_ #HWU1 #HU1 #IHW #IHU #K #s #d #e #HLK #X #H elim (lift_inv_flat2 … H) -H #V #T #HVW #HTU #H destruct elim (cprs_inv_lift1 … HWU1 … HLK … HVW) -HWU1 #U0 #HU01 #HVU0 - elim (cpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0 + elim (scpds_inv_lift1 … HU1 … HLK … HTU) -HU1 #X #HX #HTU0 lapply (lift_inj … HX … HU01) -HX #H destruct /3 width=5 by snv_cast/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma index 3c93fd3fc..9eefdba8e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -14,7 +14,7 @@ include "basic_2/dynamic/snv_lift.ma". include "basic_2/dynamic/snv_aaa.ma". -include "basic_2/dynamic/snv_cpes.ma". +include "basic_2/dynamic/snv_scpes.ma". include "basic_2/dynamic/lsubsv_snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -56,50 +56,50 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2 - elim (cpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 -HV12 #XV #HVW2 #HXV - elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HTU1 -HT12 #X #HTU2 #H + elim (scpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 -HV12 #XV #HVW2 #HXV + elim (scpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HTU1 -HT12 #X #HTU2 #H elim (cprs_inv_abst1 … H) -H #XW #U2 #HXW #_ #H destruct -IH1 -IH3 -IH2 -L1 elim (cprs_conf … HXV … HXW) -W1 #W2 #HXV #HXW - lapply (cpds_cprs_trans … HVW2 … HXV) -XV - lapply (cpds_cprs_trans … (ⓛ{a}W2.U2) … HTU2 ?) + lapply (scpds_cprs_trans … HVW2 … HXV) -XV + lapply (scpds_cprs_trans … (ⓛ{a}W2.U2) … HTU2 ?) /2 width=7 by snv_appl, cprs_bind/ | #b #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct elim (snv_inv_bind … HT1) -HT1 #HW10 #HT10 - elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30 -l0 + elim (scpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30 -l0 elim (snv_fwd_da … HV1) #l #HV1l elim (snv_fwd_da … HW10) #l0 #HW10l - lapply (cpds_div … W10 … 0 … HVW1) /2 width=2 by cprs_cpds/ -W30 #HVW10 - elim (da_cpes_aux … IH4 IH1 IH2 … HW10l … HV1l … HVW10) /2 width=1 by fqup_fpbg/ + lapply (scpds_div … W10 … 0 … HVW1) /2 width=2 by cprs_scpds/ -W30 #HVW10 + elim (da_scpes_aux … IH4 IH1 IH2 … HW10l … HV1l … HVW10) /2 width=1 by fqup_fpbg/ #_ #Hl (plus_minus_m_m l 1) in HV1l; // -Hl #HV1l - lapply (cpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20 + lapply (scpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20 lapply (IH2 … HV1l … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1l #HV2l lapply (IH2 … HW10l … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10l #HW20l lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10 #HW20 lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 #HT20 - @snv_bind /2 width=1 by snv_cast_cpes/ + @snv_bind /2 width=1 by snv_cast_scpes/ @(lsubsv_snv_trans … HT20) -HT20 @(lsubsv_beta … (l-1)) // - @hsnv_cast [1,2: // ] #l0 #Hl0 - lapply (cpes_le_aux … IH4 IH1 IH2 IH3 … HW20l … HV2l … l0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20l -HV2l -HVW20 + @shnv_cast [1,2: // ] #l0 #Hl0 + lapply (scpes_le_aux … IH4 IH1 IH2 IH3 … HW20l … HV2l … l0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20l -HV2l -HVW20 /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/ | #b #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HV02 #HW02 #HT02 #H1 #H2 destruct -IH4 elim (snv_inv_bind … HT1) -HT1 #HW0 #HT0 - elim (cpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct + elim (scpds_inv_abbr_abst … HTU1) -HTU1 #X #HTU0 #HX #H destruct elim (lift_inv_bind1 … HX) -HX #W3 #U3 #HW13 #_ #H destruct - elim (cpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 #XV #HXV0 #HXVW1 - elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HXT2 #H + elim (scpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 #XV #HXV0 #HXVW1 + elim (scpds_cpr_lpr_aux … IH2 IH3 … HTU0 … HT02 (L2.ⓓW2)) /2 width=1 by fqup_fpbg, lpr_pair/ -HTU0 #X #HXT2 #H elim (cprs_inv_abst1 … H) -H #W #U2 #HW3 #_ #H destruct -U3 lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2 lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0 lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2 lapply (snv_lift … HV0 (L2.ⓓW2) (Ⓕ) … HV02) /2 width=1 by drop_drop/ -HV0 #HV2 elim (lift_total XV 0 1) #XW #HXVW - lapply (cpds_lift … HXV0 (L2.ⓓW2) (Ⓕ) … HV02 … HXVW) /2 width=1 by drop_drop/ -V0 #HXWV2 + lapply (scpds_lift … HXV0 (L2.ⓓW2) (Ⓕ) … HV02 … HXVW) /2 width=1 by drop_drop/ -V0 #HXWV2 lapply (cprs_lift … HXVW1 (L2.ⓓW2) (Ⓕ) … HW13 … HXVW) /2 width=1 by drop_drop/ -W1 -XV #HXW3 elim (cprs_conf … HXW3 … HW3) -W3 #W3 #HXW3 #HW3 - lapply (cpds_cprs_trans … HXWV2 … HXW3) -XW - lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) … HXT2 ?) /2 width=1 by cprs_bind/ -W + lapply (scpds_cprs_trans … HXWV2 … HXW3) -XW + lapply (scpds_cprs_trans … (ⓛ{a}W3.U2) … HXT2 ?) /2 width=1 by cprs_bind/ -W /3 width=6 by snv_appl, snv_bind/ ] | #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 @@ -107,11 +107,11 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (cpr_inv_cast1 … H2) -H2 [ * #W2 #T2 #HW12 #HT12 #H destruct elim (snv_fwd_da … HW1) #l #HW1l - lapply (cpds_div … W1 … 0 … HTU1) /2 width=2 by cprs_cpds/ -U1 -l #HWT1 - lapply (cpes_cpr_lpr_aux … IH2 IH3 … HWT1 … HW12 … HT12 … HL12) /2 width=1 by fqup_fpbg/ + lapply (scpds_div … W1 … 0 … HTU1) /2 width=2 by cprs_scpds/ -U1 -l #HWT1 + lapply (scpes_cpr_lpr_aux … IH2 IH3 … HWT1 … HW12 … HT12 … HL12) /2 width=1 by fqup_fpbg/ lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -L1 - /2 width=1 by snv_cast_cpes/ + /2 width=1 by snv_cast_scpes/ | #H -IH3 -IH2 -HW1 -U1 lapply (IH1 … H … HL12) /2 width=1 by fqup_fpbg/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma index 4213293b8..45c861402 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/dynamic/snv_lift.ma". -include "basic_2/dynamic/snv_cpes.ma". +include "basic_2/dynamic/snv_scpes.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -49,8 +49,8 @@ fact snv_lstas_aux: ∀h,g,G0,L0,T0. lapply (da_inv_flat … Hl1) -Hl1 #Hl1 elim (lstas_inv_appl1 … H2) -H2 #T0 #HT10 #H destruct lapply (IH1 … HT1 … Hl1 … HT10) /2 width=1 by fqup_fpbg/ #HT0 - lapply (lstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HT10 … HTU1) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #H - elim (cpes_inv_abst2 … H) -H /3 width=6 by snv_appl, cpds_cprs_trans/ + lapply (lstas_scpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HT10 … HTU1) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #H + elim (scpes_inv_abst2 … H) -H /3 width=6 by snv_appl, scpds_cprs_trans/ | #U1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 [ lapply (lstas_inv_O … H2) -H2 #H destruct // ] elim (snv_inv_cast … H1) -H1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma index a974f248f..388cf2ba4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas_lpr.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/dynamic/snv_aaa.ma". -include "basic_2/dynamic/snv_cpes.ma". +include "basic_2/dynamic/snv_scpes.ma". include "basic_2/dynamic/lsubsv_lstas.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -86,13 +86,13 @@ fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2 lapply (da_inv_bind … Hl1) -Hl1 #Hl1 elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct - elim (cpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -l0 + elim (scpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -l0 elim (snv_fwd_da … HW2) #l0 #HW2l - lapply (cpds_div … W2 … 0 … HVW1) /2 width=3 by cprs_cpds/ -W0 #H21 + lapply (scpds_div … W2 … 0 … HVW1) /2 width=3 by cprs_scpds/ -W0 #H21 elim (snv_fwd_da … HV1) #l #HV1l - elim (da_cpes_aux … IH4 IH3 IH2 … HW2l … HV1l … H21) /2 width=1 by fqup_fpbg/ #_ #H + elim (da_scpes_aux … IH4 IH3 IH2 … HW2l … HV1l … H21) /2 width=1 by fqup_fpbg/ #_ #H (plus_minus_m_m l 1) in HV1l; // -H #HV1l - lapply (cpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32 + lapply (scpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32 lapply (IH3 … HW23 … HL12) /2 width=1 by fqup_fpbg/ #HW3 lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 lapply (IH2 … HW2l … HW23 … HL12) /2 width=1 by fqup_fpbg/ -HW2 -HW2l #HW3l @@ -106,8 +106,8 @@ fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/ | -U3 @(lsubsv_beta … (l-1)) /3 width=7 by fqup_fpbg/ - @hsnv_cast [1,2: // ] #l0 #Hl0 - lapply (cpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32 + @shnv_cast [1,2: // ] #l0 #Hl0 + lapply (scpes_le_aux … IH4 IH3 IH2 IH1 … HW3l … HV2l … l0 … H32) -IH4 -IH3 -IH2 -IH1 -HW3l -HV2l -H32 /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/ | -IH1 -IH3 -IH4 /3 width=9 by fqup_fpbg, lpr_pair/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma index 1ee74e64a..5f76fea80 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma @@ -53,3 +53,9 @@ theorem lstas_cpr_lpr: ∀h,g,G,L,T. IH_lstas_cpr_lpr h g G L T. qed-. (* Advanced preservation properties *****************************************) + +lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. +#h #g #G #L1 #T1 #HT1 #T2 #H +@(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma similarity index 60% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpes.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma index 6db1060e3..5ee696600 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpes.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_scpes.ma @@ -14,8 +14,8 @@ include "basic_2/computation/fpbs_lift.ma". include "basic_2/computation/fpbg_fleq.ma". -include "basic_2/equivalence/cpes_cpcs.ma". -include "basic_2/equivalence/cpes_cpes.ma". +include "basic_2/equivalence/scpes_cpcs.ma". +include "basic_2/equivalence/scpes_scpes.ma". include "basic_2/dynamic/snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -64,14 +64,14 @@ fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0. @(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/ qed-. -fact da_cpds_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l1. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → - ∀T2,l2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - l2 ≤ l1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, g] l1-l2. +fact da_scpds_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l1. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → + ∀T2,l2. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l2] T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + l2 ≤ l1 ∧ ⦃G, L2⦄ ⊢ T2 ▪[h, g] l1-l2. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l1 #Hl1 #T2 #l2 * #T #l0 #Hl20 #H #HT1 #HT2 #L2 #HL12 lapply (da_mono … H … Hl1) -H #H destruct lapply (lstas_da_conf … HT1 … Hl1) #Hl12 @@ -79,18 +79,18 @@ lapply (da_cprs_lpr_aux … IH2 IH1 … Hl12 … HT2 … HL12) -IH2 -IH1 -HT2 -H /3 width=8 by fpbg_fpbs_trans, lstas_fpbs, conj/ qed-. -fact da_cpes_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → - ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 → - ∀l21,l22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → - ∧∧ l21 ≤ l11 & l22 ≤ l12 & l11 - l21 = l12 - l22. +fact da_scpes_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → + ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 → + ∀l21,l22. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → + ∧∧ l21 ≤ l11 & l22 ≤ l12 & l11 - l21 = l12 - l22. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l11 #Hl11 #l12 #Hl12 #l21 #l22 * #T #HT1 #HT2 -elim (da_cpds_lpr_aux … IH3 IH2 IH1 … Hl11 … HT1 … L) -Hl11 -HT1 // -elim (da_cpds_lpr_aux … IH3 IH2 IH1 … Hl12 … HT2 … L) -Hl12 -HT2 // +elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hl11 … HT1 … L) -Hl11 -HT1 // +elim (da_scpds_lpr_aux … IH3 IH2 IH1 … Hl12 … HT2 … L) -Hl12 -HT2 // /3 width=7 by da_mono, and3_intro/ qed-. @@ -115,13 +115,13 @@ elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 /4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ qed-. -fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀U1,l. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g, l] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. +fact scpds_cpr_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀U1,l. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g, l] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g, l] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #U1 #l2 * #W1 #l1 #Hl21 #HTl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 elim (IH1 … H01 … HTW1 … HT12 … HL12) -IH1 // #W2 #HTW2 #HW12 lapply (IH2 … H01 … HTl1 … HT12 … HL12) -L0 -T0 // -T1 @@ -130,29 +130,29 @@ lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/ qed-. -fact cpes_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → - ∀l1,l2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 → - ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ⦃G, L2⦄ ⊢ U1 •*⬌*[h, g, l1, l2] U2. +fact scpes_cpr_lpr_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → + ∀l1,l2. ⦃G, L1⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2 → + ∀U1. ⦃G, L1⦄ ⊢ T1 ➡ U1 → ∀U2. ⦃G, L1⦄ ⊢ T2 ➡ U2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ⦃G, L2⦄ ⊢ U1 •*⬌*[h, g, l1, l2] U2. #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #T2 #HT02 #HT2 #l1 #l2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12 -elim (cpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1 -elim (cpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2 +elim (scpds_cpr_lpr_aux … IH2 IH1 … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1 +elim (scpds_cpr_lpr_aux … IH2 IH1 … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2 elim (cprs_conf … H1 … H2) -T0 -/3 width=5 by cpds_div, cpds_cprs_trans/ +/3 width=5 by scpds_div, scpds_cprs_trans/ qed-. -fact lstas_cpds_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → - ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → - ∀l,l1. l1 ≤ l → ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀T1. ⦃G, L⦄ ⊢ T •*[h, l1] T1 → - ∀T2,l2. ⦃G, L⦄ ⊢ T •*➡*[h, g, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l2-l1, l1-l2] T2. +fact lstas_scpds_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → + ∀G,L,T. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → + ∀l,l1. l1 ≤ l → ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀T1. ⦃G, L⦄ ⊢ T •*[h, l1] T1 → + ∀T2,l2. ⦃G, L⦄ ⊢ T •*➡*[h, g, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l2-l1, l1-l2] T2. #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T #H0 #HT #l #l1 #Hl1 #HTl #T1 #HT1 #T2 #l2 * #X #l0 #Hl20 #H #HTX #HXT2 lapply (da_mono … H … HTl) -H #H destruct lapply (lstas_da_conf … HT1 … HTl) #HTl1 @@ -160,40 +160,40 @@ lapply (lstas_da_conf … HTX … HTl) #HXl lapply (da_cprs_lpr_aux … IH3 IH2 … HXl … HXT2 L ?) [1,2,3: /3 width=8 by fpbg_fpbs_trans, lstas_fpbs/ ] #HTl2 elim (le_or_ge l1 l2) #Hl12 >(eq_minus_O … Hl12) -[ /5 width=3 by cpds_refl, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro, ex2_intro/ +[ /5 width=3 by scpds_refl, lstas_conf_le, monotonic_le_minus_l, ex4_2_intro, ex2_intro/ | lapply (lstas_conf_le … HTX … HT1) // #HXT1 -HT1 elim (lstas_cprs_lpr_aux … IH3 IH2 IH1 … HXl … HXT1 … HXT2 L) -IH3 -IH2 -IH1 -HXl -HXT1 -HXT2 - /3 width=8 by cpcs_cpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l/ + /3 width=8 by cpcs_scpes, fpbg_fpbs_trans, lstas_fpbs, monotonic_le_minus_l/ ] qed-. -fact cpes_le_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → - ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 → - ∀l21,l22,l. l21 + l ≤ l11 → l22 + l ≤ l12 → - ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21+l, l22+l] T2. +fact scpes_le_aux: ∀h,g,G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_lstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → + ∀l11. ⦃G, L⦄ ⊢ T1 ▪[h, g] l11 → ∀l12. ⦃G, L⦄ ⊢ T2 ▪[h, g] l12 → + ∀l21,l22,l. l21 + l ≤ l11 → l22 + l ≤ l12 → + ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21, l22] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l21+l, l22+l] T2. #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G #L #T1 #H01 #HT1 #T2 #H02 #HT2 #l11 #Hl11 #Hl12 #Hl12 #l21 #l22 #l #H1 #H2 * #T0 #HT10 #HT20 elim (da_inv_sta … Hl11) #X1 #HTX1 elim (lstas_total … HTX1 (l21+l)) -X1 #X1 #HTX1 elim (da_inv_sta … Hl12) #X2 #HTX2 elim (lstas_total … HTX2 (l22+l)) -X2 #X2 #HTX2 -lapply (lstas_cpds_aux … IH4 IH3 IH2 IH1 … Hl11 … HTX1 … HT10) -HT10 +lapply (lstas_scpds_aux … IH4 IH3 IH2 IH1 … Hl11 … HTX1 … HT10) -HT10 [1,2,3: // | >eq_minus_O [2: // ] eq_minus_O [2: // ]