From 7e06d9d148ae04a21943377debd933a742d0c2fa Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 14 Jul 2014 20:45:56 +0000 Subject: [PATCH] some renaming and some typos corrected ... --- .../basic_2/computation/acp_aaa.ma | 2 +- .../lambdadelta/basic_2/computation/acp_cr.ma | 20 +++---- .../lambdadelta/basic_2/computation/cpre.ma | 2 +- .../basic_2/computation/cprs_cprs.ma | 2 +- .../lambdadelta/basic_2/computation/cpxe.ma | 2 +- .../basic_2/computation/cpxs_cpxs.ma | 2 +- .../basic_2/computation/cpxs_tstc.ma | 2 +- .../basic_2/computation/csx_lpx.ma | 4 +- .../basic_2/computation/csx_tstc_vector.ma | 32 +++++------ .../basic_2/computation/csx_vector.ma | 2 +- .../basic_2/computation/fsb_csx.ma | 2 +- .../basic_2/computation/lprs_drop.ma | 2 +- .../basic_2/computation/lpxs_drop.ma | 2 +- .../lambdadelta/basic_2/computation/lsubc.ma | 2 +- .../basic_2/computation/lsubc_drop.ma | 6 +-- .../basic_2/computation/lsubc_lsuba.ma | 2 +- .../lambdadelta/basic_2/dynamic/lsubsv.ma | 54 +++++++++---------- .../basic_2/dynamic/lsubsv_cpcs.ma | 2 +- .../basic_2/dynamic/lsubsv_cpds.ma | 2 +- .../basic_2/dynamic/lsubsv_lstas.ma | 4 +- .../basic_2/dynamic/lsubsv_lsuba.ma | 2 +- .../basic_2/dynamic/lsubsv_lsubd.ma | 2 +- .../lambdadelta/basic_2/dynamic/lsubsv_snv.ma | 2 +- .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma | 2 +- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 2 +- .../basic_2/dynamic/snv_lstas_lpr.ma | 2 +- .../lambdadelta/basic_2/grammar/aarity.ma | 8 +-- .../basic_2/grammar/lenv_append.ma | 2 +- .../basic_2/grammar/term_vector.ma | 12 ++--- .../lambdadelta/basic_2/multiple/cpys_lift.ma | 2 +- .../lambdadelta/basic_2/multiple/fleq.ma | 2 +- .../basic_2/multiple/lifts_vector.ma | 4 +- .../lambdadelta/basic_2/multiple/lleq.ma | 2 +- .../lambdadelta/basic_2/multiple/lleq_llor.ma | 2 +- .../lambdadelta/basic_2/multiple/llpx_sn.ma | 2 +- .../basic_2/multiple/llpx_sn_llor.ma | 2 +- .../functions/{snapplv_2.ma => snappls_2.ma} | 2 +- .../basic_2/notation/relations/lrsubeqa_3.ma | 2 +- .../basic_2/notation/relations/lrsubeqd_5.ma | 2 +- .../basic_2/notation/relations/lrsubeqv_5.ma | 2 +- .../lambdadelta/basic_2/reduction/cpr.ma | 4 +- .../lambdadelta/basic_2/reduction/cpx.ma | 6 +-- .../lambdadelta/basic_2/reduction/lpr_drop.ma | 2 +- .../lambdadelta/basic_2/reduction/lpr_lpr.ma | 6 +-- .../lambdadelta/basic_2/reduction/lpx_aaa.ma | 2 +- .../lambdadelta/basic_2/reduction/lpx_drop.ma | 2 +- .../lambdadelta/basic_2/static/lsuba.ma | 54 +++++++++---------- .../lambdadelta/basic_2/static/lsuba_aaa.ma | 4 +- .../lambdadelta/basic_2/static/lsuba_lsuba.ma | 6 +-- .../lambdadelta/basic_2/static/lsubd.ma | 54 +++++++++---------- .../lambdadelta/basic_2/static/lsubd_da.ma | 4 +- .../lambdadelta/basic_2/static/lsubd_lsubd.ma | 4 +- .../lambdadelta/basic_2/static/lsubr.ma | 12 ++--- .../lambdadelta/basic_2/static/lsubr_lsubr.ma | 12 ++--- .../lambdadelta/basic_2/static/sta_lift.ma | 2 +- .../basic_2/substitution/cpy_lift.ma | 2 +- .../lambdadelta/basic_2/substitution/drop.ma | 2 +- .../basic_2/substitution/lift_lift.ma | 2 +- .../basic_2/substitution/lift_lift_vector.ma | 2 +- .../basic_2/substitution/lpx_sn_drop.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 8 +-- .../lambdadelta/ground_2/lib/arith.ma | 2 +- 62 files changed, 200 insertions(+), 200 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/notation/functions/{snapplv_2.ma => snappls_2.ma} (97%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index 0c8ed725b..b95885d7f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -69,7 +69,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA - /3 width=5 by lsubc_abbr, drops_trans, drops_skip, lifts_trans/ + /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/ | #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct /3 width=10 by drops_nil, lifts_nil/ 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 71a02ce87..e343e96f8 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_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct + elim (lifts_inv_appls1 … 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_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_appls1 … 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_applv, lifts_flat, lifts_bind/ + @(s3 … IHA … (V0 @ V0s)) /5 width=6 by lifts_appls, lifts_flat, lifts_bind/ | #G #L #Vs #HVs #k #L0 #V0 #X #des #HB #HL0 #H - elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_appls1 … 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_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_appls1 … 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_applv/ + @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_appls/ | #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H - elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct + elim (lifts_inv_appls1 … 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_applv // + | @lifts_appls // 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_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_appls1 … 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_applv/ + @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_appls/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma index 6b998fb13..65a6146a7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma @@ -24,7 +24,7 @@ definition cpre: relation4 genv lenv term term ≝ interpretation "evaluation for context-sensitive parallel reduction (term)" 'PRedEval G L T1 T2 = (cpre G L T1 T2). -(* Basic_properties *********************************************************) +(* Basic properties *********************************************************) (* Basic_1: was just: nf2_sn3 *) lemma csx_cpre: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma index 3f2754bd5..0b9d7a021 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma @@ -91,7 +91,7 @@ lemma cprs_inv_appl1: ∀G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡* U2 → | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct lapply (cprs_strap1 … HV10 … HV02) -V0 #HV12 lapply (lsubr_cpr_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 - /5 width=5 by cprs_bind, cprs_flat_dx, cpr_cprs, lsubr_abst, ex2_3_intro, or3_intro1/ + /5 width=5 by cprs_bind, cprs_flat_dx, cpr_cprs, lsubr_beta, ex2_3_intro, or3_intro1/ | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct /5 width=10 by cprs_flat_sn, cprs_bind_dx, cprs_strap1, ex4_5_intro, or3_intro2/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma index b2e05f37e..6d1ffd2b8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma @@ -24,7 +24,7 @@ definition cpxe: ∀h. sd h → relation4 genv lenv term term ≝ interpretation "evaluation for context-sensitive extended parallel reduction (term)" 'PRedEval h g G L T1 T2 = (cpxe h g G L T1 T2). -(* Basic_properties *********************************************************) +(* Basic properties *********************************************************) lemma csx_cpxe: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] 𝐍⦃T2⦄. #h #g #G #L #T1 #H @(csx_ind … H) -T1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma index a19c92545..f5c200630 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma @@ -82,7 +82,7 @@ lemma cpxs_inv_appl1: ∀h,g,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡*[h, g] U2 | #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct lapply (cpxs_strap1 … HV10 … HV02) -V0 #HV12 lapply (lsubr_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 - /5 width=5 by cpxs_bind, cpxs_flat_dx, cpx_cpxs, lsubr_abst, ex2_3_intro, or3_intro1/ + /5 width=5 by cpxs_bind, cpxs_flat_dx, cpx_cpxs, lsubr_beta, ex2_3_intro, or3_intro1/ | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct /5 width=10 by cpxs_flat_sn, cpxs_bind_dx, cpxs_strap1, ex4_5_intro, or3_intro2/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma index 6f7bf6038..c3125bedb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma @@ -49,7 +49,7 @@ elim (cpxs_inv_appl1 … H) -H * | #b #W0 #T0 #HT0 #HU elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1 - /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_abst, or_intror/ + /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/ | #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_ elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma index 80755fc0b..0f6cb8370 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma @@ -64,10 +64,10 @@ elim (cpx_inv_appl1 … H1) -H1 * [ -HT1 #V0 #Y #HLV0 #H #H0 destruct elim (cpx_inv_abst1 … H) -H #W0 #T0 #HLW0 #HLT0 #H destruct @IHT1 -IHT1 [4: // | skip |3: #H destruct /2 width=1 by/ ] -H2 - lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_abst/ + lapply (lsubr_cpx_trans … HLT0 (L.ⓓⓝW.V) ?) -HLT0 /3 width=1 by cpx_bind, cpx_flat, lsubr_beta/ | -IHT1 -H2 #b #V0 #W0 #W2 #T0 #T2 #HLV0 #HLW02 #HLT02 #H1 #H3 destruct lapply (lsubr_cpx_trans … HLT02 (L.ⓓⓝW0.V) ?) -HLT02 - /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_abst/ + /4 width=5 by csx_cpx_trans, cpx_bind, cpx_flat, lsubr_beta/ | -HT1 -IHT1 -H2 #b #V0 #V1 #W0 #W1 #T0 #T3 #_ #_ #_ #_ #H destruct ] qed-. 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 982a915cc..765bece71 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 @@ -22,25 +22,25 @@ include "basic_2/computation/csx_vector.ma". (* Advanced properties ******************************************************) (* Basic_1: was just: sn3_appls_lref *) -lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → +lemma csx_appls_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 applv_simple/ -IHV -HV -HVs +@csx_appl_simple_tstc /2 width=1 by appls_simple/ -IHV -HV -HVs #X #H #H0 lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H elim (H0) -H0 // qed. -lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k. +lemma csx_appls_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_applv_cnx, cnx_sort, simple_atom/ ] +#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_appls_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 applv_simple, simple_atom/ -IHVs -HV -HVs +@csx_appl_simple_tstc /2 width=1 by appls_simple, simple_atom/ -IHVs -HV -HVs #X #H #H0 elim (cpxs_fwd_sort_vector … H) -H #H [ elim H0 -H0 // @@ -49,13 +49,13 @@ elim (cpxs_fwd_sort_vector … H) -H #H qed. (* Basic_1: was just: sn3_appls_beta *) -lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T → +lemma csx_appls_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 applv_simple, simple_flat/ -IHV -HV0 -H2T +@csx_appl_simple_tstc /2 width=1 by appls_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_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → +lemma csx_appls_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_applv_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 applv_simple, simple_atom/ -IHV -HV -H2T + @csx_appl_simple_tstc /2 width=1 by appls_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 // @@ -81,7 +81,7 @@ lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → qed. (* Basic_1: was just: sn3_appls_abbr *) -lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → +lemma csx_appls_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/ @@ -100,14 +100,14 @@ 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_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T → +lemma csx_appls_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 applv_simple, simple_flat/ -IHV -HV -H2W -H2T +@csx_appl_simple_tstc /2 width=1 by appls_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_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/ +| /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/ | #G #L #V1s #V2s #HV12s #a #V #T #H #HV - @(csx_applv_theta … HV12s) -HV12s + @(csx_appls_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 733666659..bd23ff8b6 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_applv: ∀h,g,G,L,T,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Ⓐ Vs.T → +lemma csx_fwd_appls: ∀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/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma index 41ba54fd3..5941916f8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -19,7 +19,7 @@ include "basic_2/computation/fsb_alt.ma". (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) -(* Advanced propreties on context-senstive extended bormalizing terms *******) +(* Advanced propreties on context-sensitive extended normalizing terms *******) lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G2, L2⦄ ⊢ ⦥[h, g] T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_drop.ma index 139017f20..f52b71147 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_drop.ma @@ -17,7 +17,7 @@ include "basic_2/computation/lprs.ma". (* SN PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS ****************************) -(* Properies on local environment slicing ***********************************) +(* Properties on local environment slicing ***********************************) lemma lprs_drop_conf: ∀G. dropable_sn (lprs G). /3 width=3 by dropable_sn_TC, lpr_drop_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_drop.ma index 1b760d856..dba41c9dd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_drop.ma @@ -17,7 +17,7 @@ include "basic_2/computation/lpxs.ma". (* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) -(* Properies on local environment slicing ***********************************) +(* Properties on local environment slicing ***********************************) lemma lpxs_drop_conf: ∀h,g,G. dropable_sn (lpxs h g G). /3 width=3 by dropable_sn_TC, lpx_drop_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma index ccc102933..f45319f67 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma @@ -21,7 +21,7 @@ include "basic_2/computation/acp_cr.ma". inductive lsubc (RP) (G): relation lenv ≝ | lsubc_atom: lsubc RP G (⋆) (⋆) | lsubc_pair: ∀I,L1,L2,V. lsubc RP G L1 L2 → lsubc RP G (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lsubc_abbr: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A → +| lsubc_beta: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A → lsubc RP G L1 L2 → lsubc RP G (L1. ⓓⓝW.V) (L2.ⓛW) . diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma index 6aa0c0117..5f75a2d9b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma @@ -34,7 +34,7 @@ lemma lsubc_drop_O1_trans: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀K2,s,e. ⇩ | #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #s #e #H elim (drop_inv_O1_pair1 … H) -H * #He #H destruct [ elim (IHL12 L2 s 0) -IHL12 // #X #H <(drop_inv_O2 … H) -H - /3 width=8 by lsubc_abbr, drop_pair, ex2_intro/ + /3 width=8 by lsubc_beta, drop_pair, ex2_intro/ | elim (IHL12 … H) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ ] ] @@ -52,7 +52,7 @@ lemma drop_lsubc_trans: ∀RR,RS,RP. elim (lsubc_inv_pair1 … H) -H * [ #K1 #HLK1 #H destruct /3 width=3 by lsubc_pair, drop_pair, ex2_intro/ | #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct - /3 width=4 by lsubc_abbr, drop_pair, ex2_intro/ + /3 width=4 by lsubc_beta, drop_pair, ex2_intro/ ] | #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, drop_drop, ex2_intro/ @@ -66,7 +66,7 @@ lemma drop_lsubc_trans: ∀RR,RS,RP. lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA lapply (s0 … HA … HV2 … HLK1 HV3) -HV2 lapply (s0 … HA … H1W2 … HLK1 HW23) -H1W2 - /4 width=11 by lsubc_abbr, aaa_lift, drop_skip, ex2_intro/ + /4 width=11 by lsubc_beta, aaa_lift, drop_skip, ex2_intro/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma index cc9011afc..06666965b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma @@ -20,7 +20,7 @@ include "basic_2/computation/acp_aaa.ma". (* properties concerning lenv refinement for atomic arity assignment ********) lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → - ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → G ⊢ L1 ⫃[RP] L2. + ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2. #RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ #L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index fa2cf6557..b2dabf77b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -22,7 +22,7 @@ inductive lsubsv (h) (g) (G): relation lenv ≝ | lsubsv_atom: lsubsv h g G (⋆) (⋆) | lsubsv_pair: ∀I,L1,L2,V. lsubsv h g G L1 L2 → lsubsv h g G (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lsubsv_abbr: ∀L1,L2,W,V,l. ⦃G, L1⦄ ⊢ W ¡[h, g] → ⦃G, L1⦄ ⊢ V ¡[h, g] → +| lsubsv_beta: ∀L1,L2,W,V,l. ⦃G, L1⦄ ⊢ W ¡[h, g] → ⦃G, L1⦄ ⊢ V ¡[h, g] → scast h g l G L1 V W → ⦃G, L2⦄ ⊢ W ¡[h, g] → ⦃G, L1⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] l → lsubsv h g G L1 L2 → lsubsv h g G (L1.ⓓⓝW.V) (L2.ⓛW) @@ -34,7 +34,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -fact lsubsv_inv_atom1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → L1 = ⋆ → L2 = ⋆. +fact lsubsv_inv_atom1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → L1 = ⋆ → L2 = ⋆. #h #g #G #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -42,16 +42,16 @@ fact lsubsv_inv_atom1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → L1 = ⋆ ] qed-. -lemma lsubsv_inv_atom1: ∀h,g,G,L2. G ⊢ ⋆ ¡⫃[h, g] L2 → L2 = ⋆. +lemma lsubsv_inv_atom1: ∀h,g,G,L2. G ⊢ ⋆ ⫃¡[h, g] L2 → L2 = ⋆. /2 width=6 by lsubsv_inv_atom1_aux/ qed-. -fact lsubsv_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → +fact lsubsv_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → - (∃∃K2. G ⊢ K1 ¡⫃[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ + (∃∃K2. G ⊢ K1 ⫃¡[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ ∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] & scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l & - G ⊢ K1 ¡⫃[h, g] K2 & + G ⊢ K1 ⫃¡[h, g] K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. #h #g #G #L1 #L2 * -L1 -L2 [ #J #K1 #X #H destruct @@ -60,16 +60,16 @@ fact lsubsv_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → ] qed-. -lemma lsubsv_inv_pair1: ∀h,g,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ¡⫃[h, g] L2 → - (∃∃K2. G ⊢ K1 ¡⫃[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ +lemma lsubsv_inv_pair1: ∀h,g,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃¡[h, g] L2 → + (∃∃K2. G ⊢ K1 ⫃¡[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ ∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] & scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l & - G ⊢ K1 ¡⫃[h, g] K2 & + G ⊢ K1 ⫃¡[h, g] K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. /2 width=3 by lsubsv_inv_pair1_aux/ qed-. -fact lsubsv_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → L2 = ⋆ → L1 = ⋆. +fact lsubsv_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → L2 = ⋆ → L1 = ⋆. #h #g #G #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -77,16 +77,16 @@ fact lsubsv_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → L2 = ⋆ ] qed-. -lemma lsubsv_inv_atom2: ∀h,g,G,L1. G ⊢ L1 ¡⫃[h, g] ⋆ → L1 = ⋆. +lemma lsubsv_inv_atom2: ∀h,g,G,L1. G ⊢ L1 ⫃¡[h, g] ⋆ → L1 = ⋆. /2 width=6 by lsubsv_inv_atom2_aux/ qed-. -fact lsubsv_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → +fact lsubsv_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W → - (∃∃K1. G ⊢ K1 ¡⫃[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ + (∃∃K1. G ⊢ K1 ⫃¡[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ ∃∃K1,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] & scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l & - G ⊢ K1 ¡⫃[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. + G ⊢ K1 ⫃¡[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. #h #g #G #L1 #L2 * -L1 -L2 [ #J #K2 #U #H destruct | #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3/ @@ -94,35 +94,35 @@ fact lsubsv_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → ] qed-. -lemma lsubsv_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ¡⫃[h, g] K2.ⓑ{I}W → - (∃∃K1. G ⊢ K1 ¡⫃[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ +lemma lsubsv_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ⫃¡[h, g] K2.ⓑ{I}W → + (∃∃K1. G ⊢ K1 ⫃¡[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ ∃∃K1,V,l. ⦃G, K1⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ¡[h, g] & scast h g l G K1 V W & ⦃G, K2⦄ ⊢ W ¡[h, g] & ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l & - G ⊢ K1 ¡⫃[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. + G ⊢ K1 ⫃¡[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. /2 width=3 by lsubsv_inv_pair2_aux/ qed-. -(* Basic_forward lemmas *****************************************************) +(* Basic forward lemmas *****************************************************) -lemma lsubsv_fwd_lsubr: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → L1 ⫃ L2. +lemma lsubsv_fwd_lsubr: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → L1 ⫃ L2. #h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ qed-. (* Basic properties *********************************************************) -lemma lsubsv_refl: ∀h,g,G,L. G ⊢ L ¡⫃[h, g] L. +lemma lsubsv_refl: ∀h,g,G,L. G ⊢ L ⫃¡[h, g] L. #h #g #G #L elim L -L // /2 width=1/ qed. -lemma lsubsv_cprs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → +lemma lsubsv_cprs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ➡* T2 → ⦃G, L1⦄ ⊢ T1 ➡* T2. /3 width=6 by lsubsv_fwd_lsubr, lsubr_cprs_trans/ qed-. (* Note: the constant 0 cannot be generalized *) -lemma lsubsv_drop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → +lemma lsubsv_drop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 → - ∃∃K2. G ⊢ K1 ¡⫃[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2. + ∃∃K2. G ⊢ K1 ⫃¡[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2. #h #g #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H @@ -136,16 +136,16 @@ lemma lsubsv_drop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → elim (drop_inv_O1_pair1 … H) -H * #He #HLK1 [ destruct elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, drop_pair, ex2_intro/ + <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/ | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/ ] ] qed-. (* Note: the constant 0 cannot be generalized *) -lemma lsubsv_drop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → +lemma lsubsv_drop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → ∀K2,s, e. ⇩[s, 0, e] L2 ≡ K2 → - ∃∃K1. G ⊢ K1 ¡⫃[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1. + ∃∃K1. G ⊢ K1 ⫃¡[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1. #h #g #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H @@ -159,7 +159,7 @@ lemma lsubsv_drop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → elim (drop_inv_O1_pair1 … H) -H * #He #HLK2 [ destruct elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_abbr, drop_pair, ex2_intro/ + <(drop_inv_O2 … H) in HL12; -H /3 width=4 by lsubsv_beta, drop_pair, ex2_intro/ | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma index e4fe12f2d..de5577ec2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpcs.ma @@ -19,7 +19,7 @@ include "basic_2/dynamic/lsubsv.ma". (* Properties on context-sensitive parallel equivalence for terms ***********) -lemma lsubsv_cpcs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → +lemma lsubsv_cpcs_trans: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → ∀T1,T2. ⦃G, L2⦄ ⊢ T1 ⬌* T2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2. /3 width=6 by lsubsv_fwd_lsubr, lsubr_cpcs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma index 2604db925..8c45457cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma @@ -19,7 +19,7 @@ include "basic_2/dynamic/lsubsv_lstas.ma". (* Properties on decomposed extended parallel computation on terms **********) lemma lsubsv_cpds_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 •*➡*[h, g] T2 → - ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → + ∀L1. G ⊢ L1 ⫃¡[h, g] L2 → ∃∃T. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] T & ⦃G, L1⦄ ⊢ T2 ➡* T. #h #g #G #L2 #T1 #T2 * #T #l1 #l2 #Hl21 #Hl1 #HT1 #HT2 #L1 #HL12 lapply (lsubsv_cprs_trans … HL12 … HT2) -HT2 #HT2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma index f0aa8c63f..0a75b3e96 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lstas.ma @@ -24,7 +24,7 @@ include "basic_2/dynamic/lsubsv_lsubd.ma". lemma lsubsv_lstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, l1] U2 → ∀l2. l1 ≤ l2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l2 → - ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → + ∀L1. G ⊢ L1 ⫃¡[h, g] L2 → ∃∃U1. ⦃G, L1⦄ ⊢ T •*[h, l1] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2. #h #g #G #L2 #T #U #l1 #H @(lstas_ind_alt … H) -G -L2 -T -U -l1 [1,2: /2 width=3 by ex2_intro/ @@ -82,7 +82,7 @@ qed-. lemma lsubsv_sta_trans: ∀h,g,G,L2,T,U2. ⦃G, L2⦄ ⊢ T •[h] U2 → ∀l. ⦃G, L2⦄ ⊢ T ▪[h, g] l+1 → - ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → + ∀L1. G ⊢ L1 ⫃¡[h, g] L2 → ∃∃U1. ⦃G, L1⦄ ⊢ T •[h] U1 & ⦃G, L1⦄ ⊢ U1 ⬌* U2. #h #g #G #L2 #T #U2 #H #l #HTl #L1 #HL12 elim (lsubsv_lstas_trans … U2 1 … HTl … HL12) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma index db5df3b4c..97c77b05d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma @@ -19,7 +19,7 @@ include "basic_2/dynamic/lsubsv.ma". (* Forward lemmas on lenv refinement for atomic arity assignment ************) -lemma lsubsv_fwd_lsuba: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → G ⊢ L1 ⁝⫃ L2. +lemma lsubsv_fwd_lsuba: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → G ⊢ L1 ⫃⁝ L2. #h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ #L1 #L2 #W #V #l #H1W #HV #HVW #H2W #H1l #_ #_ #IHL12 lapply (snv_scast … HV H1W HVW H1l) -HV -H1W -HVW -H1l #HV diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma index 86007b1f5..b7eac381a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma @@ -19,6 +19,6 @@ include "basic_2/dynamic/lsubsv.ma". (* Forward lemmas on lenv refinement for degree assignment ******************) -lemma lsubsv_fwd_lsubd: ∀h,g,G,L1,L2. G ⊢ L1 ¡⫃[h, g] L2 → G ⊢ L1 ▪⫃[h, g] L2. +lemma lsubsv_fwd_lsubd: ∀h,g,G,L1,L2. G ⊢ L1 ⫃¡[h, g] L2 → G ⊢ L1 ⫃▪[h, g] L2. #h #g #G #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma index 0a6d05204..0777e36cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma @@ -22,7 +22,7 @@ include "basic_2/dynamic/lsubsv_cpcs.ma". (* Properties concerning stratified native validity *************************) lemma lsubsv_snv_trans: ∀h,g,G,L2,T. ⦃G, L2⦄ ⊢ T ¡[h, g] → - ∀L1. G ⊢ L1 ¡⫃[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g]. + ∀L1. G ⊢ L1 ⫃¡[h, g] L2 → ⦃G, L1⦄ ⊢ T ¡[h, g]. #h #g #G #L2 #T #H elim H -G -L2 -T // [ #I #G #L2 #K2 #V #i #HLK2 #_ #IHV #L1 #HL12 elim (lsubsv_drop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma index a9a07c983..8a73365d6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma @@ -77,7 +77,7 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fqup_fpbg/ ] #Hl0 lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fqup_fpbg/ -HW lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2 - /4 width=6 by da_bind, lsubd_da_trans, lsubd_abbr/ + /4 width=6 by da_bind, lsubd_da_trans, lsubd_beta/ | #b #V #V2 #W #W2 #U1 #U2 #HV1 #HV2 #HW2 #HU12 #H1 #H2 destruct -IH3 -IH2 -V -W0 -T0 -l0 -HV1 -HVW1 elim (snv_inv_bind … HT1) -HT1 #_ lapply (da_inv_bind … Hl) -Hl 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 5e0d2bf56..754c8da4a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -87,7 +87,7 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (snv_sta_aux … IH4 … HlV2 … HV2W3) /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW3 lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/ - @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20 + @(lsubsv_beta … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW20 lapply (lstas_sta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W @(lstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) // [ /3 width=9 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_sta_fpbs/ 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 5615c0fdf..476a420f8 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 @@ -113,7 +113,7 @@ fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. @(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W3.U3)) /2 width=1 by cpr_beta/ /4 width=3 by cpcs_flat, cpcs_bind2, lpr_cpr_conf/ | -U3 - @(lsubsv_abbr … l) /3 width=7 by fqup_fpbg/ + @(lsubsv_beta … l) /3 width=7 by fqup_fpbg/ #W #W0 #l0 #Hl0 #HV2W #HW30 lapply (lstas_sta_conf_pos … HV2W4 … HV2W) -HV2W #HW4W @(lstas_cpcs_lpr_aux … IH3 IH2 IH1 … Hl0 … HW4W … Hl0 … HW30 … HW43) // diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma index 88486384a..27c775019 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma @@ -27,10 +27,10 @@ inductive aarity: Type[0] ≝ | APair: aarity → aarity → aarity (* binary aarity construction *) . -interpretation "aarity construction (atomic)" +interpretation "atomic arity construction (atomic)" 'Item0 = AAtom. -interpretation "aarity construction (binary)" +interpretation "atomic arity construction (binary)" 'SnItem2 A1 A2 = (APair A1 A2). (* Basic inversion lemmas ***************************************************) @@ -39,7 +39,7 @@ lemma discr_apair_xy_x: ∀A,B. ②B. A = B → ⊥. #A #B elim B -B [ #H destruct | #Y #X #IHY #_ #H destruct - -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destucted equality is not erased *) + -H >e0 in e1; normalize (**) (* destruct: one quality is not simplified, the destructed equality is not erased *) /2 width=1/ ] qed-. @@ -48,7 +48,7 @@ lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → ⊥. #B #A elim A -A [ #H destruct | #Y #X #_ #IHX #H destruct - -H (**) (* destruct: the destucted equality is not erased *) + -H (**) (* destruct: the destructed equality is not erased *) /2 width=1/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma index 3fdb1ad37..68b7a39fe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma @@ -120,7 +120,7 @@ lemma length_inv_pos_sn_ltail: ∀L,d. d + 1 = |L| → elim (lpair_ltail L I V) /2 width=5 by ex2_3_intro/ qed-. -(* Basic_eliminators ********************************************************) +(* Basic eliminators ********************************************************) (* Basic_1: was: c_tail_ind *) lemma lenv_ind_alt: ∀R:predicate lenv. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma index 748e5cb63..b9cc288a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_vector.ma @@ -13,22 +13,22 @@ (**************************************************************************) include "ground_2/lib/list.ma". -include "basic_2/notation/functions/snapplv_2.ma". +include "basic_2/notation/functions/snappls_2.ma". include "basic_2/grammar/term_simple.ma". (* TERMS ********************************************************************) -let rec applv Vs T on Vs ≝ +let rec appls Vs T on Vs ≝ match Vs with [ nil ⇒ T - | cons hd tl ⇒ ⓐhd. (applv tl T) + | cons hd tl ⇒ ⓐhd. (appls tl T) ]. -interpretation "application o vevtor (term)" - 'SnApplV Vs T = (applv Vs T). +interpretation "application to vector (term)" + 'SnApplStar Vs T = (appls Vs T). (* properties concerning simple terms ***************************************) -lemma applv_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄. +lemma appls_simple: ∀T,Vs. 𝐒⦃T⦄ → 𝐒⦃ⒶVs.T⦄. #T * // qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma index 3e0204b82..d69de694e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys_lift.ma @@ -44,7 +44,7 @@ lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d. @(cpys_subst … HLK … HU12) >yminus_Y_inj // qed. -(* Advanced inverion lemmas *************************************************) +(* Advanced inversion lemmas *************************************************) lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*[d, e] T2 → T2 = ⓪{I} ∨ diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/fleq.ma index b7120b85b..910dca14c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/fleq.ma @@ -26,7 +26,7 @@ interpretation "lazy equivalence (closure)" 'LazyEq d G1 L1 T1 G2 L2 T2 = (fleq d G1 L1 T1 G2 L2 T2). -(* Basic_properties *********************************************************) +(* Basic properties *********************************************************) lemma fleq_refl: ∀d. tri_reflexive … (fleq d). /2 width=1 by fleq_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma index d6878c0a1..3cb26d890 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lifts_vector.ma @@ -30,7 +30,7 @@ interpretation "generic relocation (vector)" (* Basic inversion lemmas ***************************************************) (* Basic_1: was: lifts1_flat (left to right) *) -lemma lifts_inv_applv1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 → +lemma lifts_inv_appls1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 → ∃∃V2s,U2. ⇧*[des] V1s ≡ V2s & ⇧*[des] U1 ≡ U2 & T2 = Ⓐ V2s. U2. #V1s elim V1s -V1s normalize @@ -46,7 +46,7 @@ qed-. (* Basic properties *********************************************************) (* Basic_1: was: lifts1_flat (right to left) *) -lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s → +lemma lifts_appls: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s → ∀T1,T2. ⇧*[des] T1 ≡ T2 → ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2. #V1s #V2s #des #H elim H -V1s -V2s /3 width=1 by lifts_flat/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma index 9f94ae0da..7be12035e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma @@ -153,7 +153,7 @@ lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[V, 0] L2 → L1.ⓑ{I}V ≡[T, 0] L2 L1 ≡[ⓑ{a,I}V.T, 0] L2. /2 width=1 by llpx_sn_bind_O/ qed-. -(* Advancded properties on lazy pointwise exyensions ************************) +(* Advanceded properties on lazy pointwise extensions ************************) lemma llpx_sn_lrefl: ∀R. (∀L. reflexive … (R L)) → ∀L1,L2,T,d. L1 ≡[T, d] L2 → llpx_sn R d T L1 L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma index 51c033350..df65d267a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq_llor.ma @@ -18,7 +18,7 @@ include "basic_2/multiple/lleq_alt.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) -(* Properties on poinwise union for local environments **********************) +(* Properties on pointwise union for local environments **********************) lemma llpx_sn_llor_dx: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) → ∀L1,L2,T,d. llpx_sn R d T L1 L2 → ∀L. L1 ⩖[T, d] L2 ≡ L → L2 ≡[T, d] L. diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma index 692039c11..f0d8bbcfe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma @@ -145,7 +145,7 @@ lemma llpx_sn_fwd_pair_sn: ∀R,I,L1,L2,V,T,d. llpx_sn R d (②{I}V.T) L1 L2 → #R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/ qed-. -(* Basic_properties *********************************************************) +(* Basic properties *********************************************************) lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,d. llpx_sn R d T L L. #R #HR #T #L @(f2_ind … rfw … L T) -L -T diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma index bc65d2002..e5933d4c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn_llor.ma @@ -18,7 +18,7 @@ include "basic_2/multiple/lleq_alt.ma". (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) -(* Inversion lemmas on poinwise union for local environments ****************) +(* Inversion lemmas on pointwise union for local environments ****************) lemma llpx_sn_llor_fwd_sn: ∀R. (∀L. reflexive … (R L)) → ∀L1,L2,T,d. llpx_sn R d T L1 L2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplv_2.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snappls_2.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplv_2.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/functions/snappls_2.ma index 9d721e298..c8beab968 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snapplv_2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/snappls_2.ma @@ -16,4 +16,4 @@ notation "hvbox( Ⓐ term 55 T1 . break term 55 T )" non associative with precedence 55 - for @{ 'SnApplV $T1 $T }. + for @{ 'SnApplStar $T1 $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_3.ma index 238f43331..c3b74a96a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqa_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ break term 46 L1 ⁝ ⫃ break term 46 L2 )" +notation "hvbox( G ⊢ break term 46 L1 ⫃ ⁝ break term 46 L2 )" non associative with precedence 45 for @{ 'LRSubEqA $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma index c4943b220..d90e35183 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ break term 46 L1 ▪ ⫃ break [ term 46 h, break term 46 g ] break term 46 L2 )" +notation "hvbox( G ⊢ break term 46 L1 ⫃ ▪ break [ term 46 h, break term 46 g ] break term 46 L2 )" non associative with precedence 45 for @{ 'LRSubEqD $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma index 3ed8b48b3..f6595e14d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( G ⊢ break term 46 L1 ¡ ⫃ break [ term 46 h, break term 46 g ] break term 46 L2 )" +notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ break [ term 46 h, break term 46 g ] break term 46 L2 )" non associative with precedence 45 for @{ 'LRSubEqV $h $g $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma index ad4fcb313..6db05fe53 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma @@ -54,9 +54,9 @@ lemma lsubr_cpr_trans: ∀G. lsub_trans … (cpr G) lsubr. | #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 elim (lsubr_fwd_drop2_abbr … HL12 … HLK1) -L1 * /3 width=6 by cpr_delta/ -|3,7: /4 width=1 by lsubr_bind, cpr_bind, cpr_beta/ +|3,7: /4 width=1 by lsubr_pair, cpr_bind, cpr_beta/ |4,6: /3 width=1 by cpr_flat, cpr_eps/ -|5,8: /4 width=3 by lsubr_bind, cpr_zeta, cpr_theta/ +|5,8: /4 width=3 by lsubr_pair, cpr_zeta, cpr_theta/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma index 3a495f59a..27f51b907 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma @@ -55,11 +55,11 @@ lemma lsubr_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) lsubr. [ // | /2 width=2 by cpx_st/ | #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 - elim (lsubr_fwd_drop2_bind … HL12 … HLK1) -HL12 -HLK1 * + elim (lsubr_fwd_drop2_pair … HL12 … HLK1) -HL12 -HLK1 * /4 width=7 by cpx_delta, cpx_ct/ -|4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_bind/ +|4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_pair/ |5,7,8: /3 width=1 by cpx_flat, cpx_eps, cpx_ct/ -|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsubr_bind/ +|6,10: /4 width=3 by cpx_zeta, cpx_theta, lsubr_pair/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_drop.ma index 744d2adaf..f9701a1ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_drop.ma @@ -19,7 +19,7 @@ include "basic_2/reduction/lpr.ma". (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) -(* Properies on local environment slicing ***********************************) +(* Properties on local environment slicing ***********************************) (* Basic_1: includes: wcpr0_drop *) lemma lpr_drop_conf: ∀G. dropable_sn (lpr G). diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma index 723ed5c59..2aa2810b1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma @@ -193,7 +193,7 @@ elim (cpr_inv_abst1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ #W #HW1 #HW2 elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 -lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/ (**) (* full auto not tried *) +lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ (**) (* full auto not tried *) /4 width=5 by cpr_bind, cpr_flat, cpr_beta, ex2_intro/ qed-. @@ -246,8 +246,8 @@ fact cpr_conf_lpr_beta_beta: elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2 elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 -lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_abst/ -lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/ +lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/ +lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ /4 width=5 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma index e08817066..6c1fbdbfa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma @@ -55,7 +55,7 @@ lemma cpx_lpx_aaa_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → lapply (IHV1 … HV12 … HL12) -IHV1 -HV12 #HV2 lapply (IHT1 (ⓛ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H elim (aaa_inv_abst … H) -H #B0 #A0 #HW1 #HU2 #H destruct - /5 width=6 by lsuba_aaa_trans, lsuba_abbr, aaa_abbr, aaa_cast/ + /5 width=6 by lsuba_aaa_trans, lsuba_beta, aaa_abbr, aaa_cast/ | #b #V #V2 #W1 #W2 #U1 #U2 #HV1 #HV2 #HW12 #HU12 #H1 #H2 destruct lapply (aaa_lift G L2 … B … (L2.ⓓW2) … HV2) -HV2 /2 width=2 by drop_drop/ #HV2 lapply (IHT1 (ⓓ{b}W2.U2) … HL12) -IHT1 /2 width=1 by cpx_bind/ -L1 #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma index 28e3f0e6a..27a0e473f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_drop.ma @@ -18,7 +18,7 @@ include "basic_2/reduction/lpx.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) -(* Properies on local environment slicing ***********************************) +(* Properties on local environment slicing ***********************************) lemma lpx_drop_conf: ∀h,g,G. dropable_sn (lpx h g G). /3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma index e996418dc..be8b2a38b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma @@ -21,17 +21,17 @@ include "basic_2/static/aaa.ma". inductive lsuba (G:genv): relation lenv ≝ | lsuba_atom: lsuba G (⋆) (⋆) | lsuba_pair: ∀I,L1,L2,V. lsuba G L1 L2 → lsuba G (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lsuba_abbr: ∀L1,L2,W,V,A. ⦃G, L1⦄ ⊢ ⓝW.V ⁝ A → ⦃G, L2⦄ ⊢ W ⁝ A → +| lsuba_beta: ∀L1,L2,W,V,A. ⦃G, L1⦄ ⊢ ⓝW.V ⁝ A → ⦃G, L2⦄ ⊢ W ⁝ A → lsuba G L1 L2 → lsuba G (L1.ⓓⓝW.V) (L2.ⓛW) . interpretation - "local environment refinement (atomic arity assigment)" + "local environment refinement (atomic arity assignment)" 'LRSubEqA G L1 L2 = (lsuba G L1 L2). (* Basic inversion lemmas ***************************************************) -fact lsuba_inv_atom1_aux: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → L1 = ⋆ → L2 = ⋆. +fact lsuba_inv_atom1_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L1 = ⋆ → L2 = ⋆. #G #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -39,13 +39,13 @@ fact lsuba_inv_atom1_aux: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → L1 = ⋆ → L2 = ] qed-. -lemma lsuba_inv_atom1: ∀G,L2. G ⊢ ⋆ ⁝⫃ L2 → L2 = ⋆. +lemma lsuba_inv_atom1: ∀G,L2. G ⊢ ⋆ ⫃⁝ L2 → L2 = ⋆. /2 width=4 by lsuba_inv_atom1_aux/ qed-. -fact lsuba_inv_pair1_aux: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → - (∃∃K2. G ⊢ K1 ⁝⫃ K2 & L2 = K2.ⓑ{I}X) ∨ +fact lsuba_inv_pair1_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → + (∃∃K2. G ⊢ K1 ⫃⁝ K2 & L2 = K2.ⓑ{I}X) ∨ ∃∃K2,W,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & - G ⊢ K1 ⁝⫃ K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. + G ⊢ K1 ⫃⁝ K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. #G #L1 #L2 * -L1 -L2 [ #J #K1 #X #H destruct | #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3 by ex2_intro, or_introl/ @@ -53,13 +53,13 @@ fact lsuba_inv_pair1_aux: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → ∀I,K1,X. L1 = K1. ] qed-. -lemma lsuba_inv_pair1: ∀I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⁝⫃ L2 → - (∃∃K2. G ⊢ K1 ⁝⫃ K2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃K2,W,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⁝⫃ K2 & +lemma lsuba_inv_pair1: ∀I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃⁝ L2 → + (∃∃K2. G ⊢ K1 ⫃⁝ K2 & L2 = K2.ⓑ{I}X) ∨ + ∃∃K2,W,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⫃⁝ K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. /2 width=3 by lsuba_inv_pair1_aux/ qed-. -fact lsuba_inv_atom2_aux: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → L2 = ⋆ → L1 = ⋆. +fact lsuba_inv_atom2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L2 = ⋆ → L1 = ⋆. #G #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -67,13 +67,13 @@ fact lsuba_inv_atom2_aux: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → L2 = ⋆ → L1 = ] qed-. -lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⁝⫃ ⋆ → L1 = ⋆. +lemma lsubc_inv_atom2: ∀G,L1. G ⊢ L1 ⫃⁝ ⋆ → L1 = ⋆. /2 width=4 by lsuba_inv_atom2_aux/ qed-. -fact lsuba_inv_pair2_aux: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W → - (∃∃K1. G ⊢ K1 ⁝⫃ K2 & L1 = K1.ⓑ{I}W) ∨ +fact lsuba_inv_pair2_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W → + (∃∃K1. G ⊢ K1 ⫃⁝ K2 & L1 = K1.ⓑ{I}W) ∨ ∃∃K1,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & - G ⊢ K1 ⁝⫃ K2 & I = Abst & L1 = K1.ⓓⓝW.V. + G ⊢ K1 ⫃⁝ K2 & I = Abst & L1 = K1.ⓓⓝW.V. #G #L1 #L2 * -L1 -L2 [ #J #K2 #U #H destruct | #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3 by ex2_intro, or_introl/ @@ -81,27 +81,27 @@ fact lsuba_inv_pair2_aux: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → ∀I,K2,W. L2 = K2. ] qed-. -lemma lsuba_inv_pair2: ∀I,G,L1,K2,W. G ⊢ L1 ⁝⫃ K2.ⓑ{I}W → - (∃∃K1. G ⊢ K1 ⁝⫃ K2 & L1 = K1.ⓑ{I}W) ∨ - ∃∃K1,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⁝⫃ K2 & +lemma lsuba_inv_pair2: ∀I,G,L1,K2,W. G ⊢ L1 ⫃⁝ K2.ⓑ{I}W → + (∃∃K1. G ⊢ K1 ⫃⁝ K2 & L1 = K1.ⓑ{I}W) ∨ + ∃∃K1,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⫃⁝ K2 & I = Abst & L1 = K1.ⓓⓝW.V. /2 width=3 by lsuba_inv_pair2_aux/ qed-. (* Basic forward lemmas *****************************************************) -lemma lsuba_fwd_lsubr: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → L1 ⫃ L2. -#G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_abst/ +lemma lsuba_fwd_lsubr: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → L1 ⫃ L2. +#G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/ qed-. (* Basic properties *********************************************************) -lemma lsuba_refl: ∀G,L. G ⊢ L ⁝⫃ L. +lemma lsuba_refl: ∀G,L. G ⊢ L ⫃⁝ L. #G #L elim L -L /2 width=1 by lsuba_atom, lsuba_pair/ qed. (* Note: the constant 0 cannot be generalized *) -lemma lsuba_drop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 → - ∃∃K2. G ⊢ K1 ⁝⫃ K2 & ⇩[s, 0, e] L2 ≡ K2. +lemma lsuba_drop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 → + ∃∃K2. G ⊢ K1 ⫃⁝ K2 & ⇩[s, 0, e] L2 ≡ K2. #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H @@ -115,15 +115,15 @@ lemma lsuba_drop_O1_conf: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → ∀K1,s,e. ⇩[s, 0 elim (drop_inv_O1_pair1 … H) -H * #He #HLK1 [ destruct elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_abbr, drop_pair, ex2_intro/ + <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/ | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/ ] ] qed-. (* Note: the constant 0 cannot be generalized *) -lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 → - ∃∃K1. G ⊢ K1 ⁝⫃ K2 & ⇩[s, 0, e] L1 ≡ K1. +lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 → + ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⇩[s, 0, e] L1 ≡ K1. #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H @@ -137,7 +137,7 @@ lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⁝⫃ L2 → ∀K2,s,e. ⇩[s, elim (drop_inv_O1_pair1 … H) -H * #He #HLK2 [ destruct elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_abbr, drop_pair, ex2_intro/ + <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsuba_beta, drop_pair, ex2_intro/ | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma index 7588e5cc7..6f8e00c84 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma @@ -20,7 +20,7 @@ include "basic_2/static/lsuba.ma". (* Properties concerning atomic arity assignment ****************************) lemma lsuba_aaa_conf: ∀G,L1,V,A. ⦃G, L1⦄ ⊢ V ⁝ A → - ∀L2. G ⊢ L1 ⁝⫃ L2 → ⦃G, L2⦄ ⊢ V ⁝ A. + ∀L2. G ⊢ L1 ⫃⁝ L2 → ⦃G, L2⦄ ⊢ V ⁝ A. #G #L1 #V #A #H elim H -G -L1 -V -A [ // | #I #G #L1 #K1 #V #A #i #HLK1 #HV #IHV #L2 #HL12 @@ -38,7 +38,7 @@ lemma lsuba_aaa_conf: ∀G,L1,V,A. ⦃G, L1⦄ ⊢ V ⁝ A → qed-. lemma lsuba_aaa_trans: ∀G,L2,V,A. ⦃G, L2⦄ ⊢ V ⁝ A → - ∀L1. G ⊢ L1 ⁝⫃ L2 → ⦃G, L1⦄ ⊢ V ⁝ A. + ∀L1. G ⊢ L1 ⫃⁝ L2 → ⦃G, L1⦄ ⊢ V ⁝ A. #G #L2 #V #A #H elim H -G -L2 -V -A [ // | #I #G #L2 #K2 #V #A #i #HLK2 #H1V #IHV #L1 #HL12 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma index e14012c45..cc4af1670 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma @@ -18,18 +18,18 @@ include "basic_2/static/lsuba_aaa.ma". (* Main properties **********************************************************) -theorem lsuba_trans: ∀G,L1,L. G ⊢ L1 ⁝⫃ L → ∀L2. G ⊢ L ⁝⫃ L2 → G ⊢ L1 ⁝⫃ L2. +theorem lsuba_trans: ∀G,L1,L. G ⊢ L1 ⫃⁝ L → ∀L2. G ⊢ L ⫃⁝ L2 → G ⊢ L1 ⫃⁝ L2. #G #L1 #L #H elim H -L1 -L [ #X #H >(lsuba_inv_atom1 … H) -H // | #I #L1 #L #Y #HL1 #IHL1 #X #H elim (lsuba_inv_pair1 … H) -H * #L2 [ #HL2 #H destruct /3 width=1/ | #W #V #A #HV #HW #HL2 #H1 #H2 #H3 destruct - /3 width=3 by lsuba_abbr, lsuba_aaa_trans/ + /3 width=3 by lsuba_beta, lsuba_aaa_trans/ ] | #L1 #L #W #V #A #HV #HW #HL1 #IHL1 #X #H elim (lsuba_inv_pair1 … H) -H * #L2 - [ #HL2 #H destruct /3 width=5 by lsuba_abbr, lsuba_aaa_conf/ + [ #HL2 #H destruct /3 width=5 by lsuba_beta, lsuba_aaa_conf/ | #W0 #V0 #A0 #_ #_ #_ #H destruct ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd.ma index abbe1b062..3dec42104 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd.ma @@ -22,7 +22,7 @@ inductive lsubd (h) (g) (G): relation lenv ≝ | lsubd_atom: lsubd h g G (⋆) (⋆) | lsubd_pair: ∀I,L1,L2,V. lsubd h g G L1 L2 → lsubd h g G (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lsubd_abbr: ∀L1,L2,W,V,l. ⦃G, L1⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] l → +| lsubd_beta: ∀L1,L2,W,V,l. ⦃G, L1⦄ ⊢ V ▪[h, g] l+1 → ⦃G, L2⦄ ⊢ W ▪[h, g] l → lsubd h g G L1 L2 → lsubd h g G (L1.ⓓⓝW.V) (L2.ⓛW) . @@ -30,15 +30,15 @@ interpretation "local environment refinement (degree assignment)" 'LRSubEqD h g G L1 L2 = (lsubd h g G L1 L2). -(* Basic_forward lemmas *****************************************************) +(* Basic forward lemmas *****************************************************) -lemma lsubd_fwd_lsubr: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → L1 ⫃ L2. -#h #g #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_bind, lsubr_abst/ +lemma lsubd_fwd_lsubr: ∀h,g,G,L1,L2. G ⊢ L1 ⫃▪[h, g] L2 → L1 ⫃ L2. +#h #g #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/ qed-. (* Basic inversion lemmas ***************************************************) -fact lsubd_inv_atom1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → L1 = ⋆ → L2 = ⋆. +fact lsubd_inv_atom1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃▪[h, g] L2 → L1 = ⋆ → L2 = ⋆. #h #g #G #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -46,14 +46,14 @@ fact lsubd_inv_atom1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → L1 = ⋆ ] qed-. -lemma lsubd_inv_atom1: ∀h,g,G,L2. G ⊢ ⋆ ▪⫃[h, g] L2 → L2 = ⋆. +lemma lsubd_inv_atom1: ∀h,g,G,L2. G ⊢ ⋆ ⫃▪[h, g] L2 → L2 = ⋆. /2 width=6 by lsubd_inv_atom1_aux/ qed-. -fact lsubd_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → +fact lsubd_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃▪[h, g] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → - (∃∃K2. G ⊢ K1 ▪⫃[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ + (∃∃K2. G ⊢ K1 ⫃▪[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ ∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l & - G ⊢ K1 ▪⫃[h, g] K2 & + G ⊢ K1 ⫃▪[h, g] K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. #h #g #G #L1 #L2 * -L1 -L2 [ #J #K1 #X #H destruct @@ -62,14 +62,14 @@ fact lsubd_inv_pair1_aux: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → ] qed-. -lemma lsubd_inv_pair1: ∀h,g,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ▪⫃[h, g] L2 → - (∃∃K2. G ⊢ K1 ▪⫃[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ +lemma lsubd_inv_pair1: ∀h,g,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃▪[h, g] L2 → + (∃∃K2. G ⊢ K1 ⫃▪[h, g] K2 & L2 = K2.ⓑ{I}X) ∨ ∃∃K2,W,V,l. ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l & - G ⊢ K1 ▪⫃[h, g] K2 & + G ⊢ K1 ⫃▪[h, g] K2 & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V. /2 width=3 by lsubd_inv_pair1_aux/ qed-. -fact lsubd_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → L2 = ⋆ → L1 = ⋆. +fact lsubd_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃▪[h, g] L2 → L2 = ⋆ → L1 = ⋆. #h #g #G #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct @@ -77,14 +77,14 @@ fact lsubd_inv_atom2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → L2 = ⋆ ] qed-. -lemma lsubd_inv_atom2: ∀h,g,G,L1. G ⊢ L1 ▪⫃[h, g] ⋆ → L1 = ⋆. +lemma lsubd_inv_atom2: ∀h,g,G,L1. G ⊢ L1 ⫃▪[h, g] ⋆ → L1 = ⋆. /2 width=6 by lsubd_inv_atom2_aux/ qed-. -fact lsubd_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → +fact lsubd_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ⫃▪[h, g] L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W → - (∃∃K1. G ⊢ K1 ▪⫃[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ + (∃∃K1. G ⊢ K1 ⫃▪[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ ∃∃K1,V,l. ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l & - G ⊢ K1 ▪⫃[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. + G ⊢ K1 ⫃▪[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. #h #g #G #L1 #L2 * -L1 -L2 [ #J #K2 #U #H destruct | #I #L1 #L2 #V #HL12 #J #K2 #U #H destruct /3 width=3 by ex2_intro, or_introl/ @@ -92,22 +92,22 @@ fact lsubd_inv_pair2_aux: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → ] qed-. -lemma lsubd_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ▪⫃[h, g] K2.ⓑ{I}W → - (∃∃K1. G ⊢ K1 ▪⫃[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ +lemma lsubd_inv_pair2: ∀h,g,I,G,L1,K2,W. G ⊢ L1 ⫃▪[h, g] K2.ⓑ{I}W → + (∃∃K1. G ⊢ K1 ⫃▪[h, g] K2 & L1 = K1.ⓑ{I}W) ∨ ∃∃K1,V,l. ⦃G, K1⦄ ⊢ V ▪[h, g] l+1 & ⦃G, K2⦄ ⊢ W ▪[h, g] l & - G ⊢ K1 ▪⫃[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. + G ⊢ K1 ⫃▪[h, g] K2 & I = Abst & L1 = K1. ⓓⓝW.V. /2 width=3 by lsubd_inv_pair2_aux/ qed-. (* Basic properties *********************************************************) -lemma lsubd_refl: ∀h,g,G,L. G ⊢ L ▪⫃[h, g] L. +lemma lsubd_refl: ∀h,g,G,L. G ⊢ L ⫃▪[h, g] L. #h #g #G #L elim L -L /2 width=1 by lsubd_pair/ qed. (* Note: the constant 0 cannot be generalized *) -lemma lsubd_drop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → +lemma lsubd_drop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ⫃▪[h, g] L2 → ∀K1,s,e. ⇩[s, 0, e] L1 ≡ K1 → - ∃∃K2. G ⊢ K1 ▪⫃[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2. + ∃∃K2. G ⊢ K1 ⫃▪[h, g] K2 & ⇩[s, 0, e] L2 ≡ K2. #h #g #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #V #_ #IHL12 #K1 #s #e #H @@ -121,16 +121,16 @@ lemma lsubd_drop_O1_conf: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → elim (drop_inv_O1_pair1 … H) -H * #He #HLK1 [ destruct elim (IHL12 L1 s 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubd_abbr, drop_pair, ex2_intro/ + <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubd_beta, drop_pair, ex2_intro/ | elim (IHL12 … HLK1) -L1 /3 width=3 by drop_drop_lt, ex2_intro/ ] ] qed-. (* Note: the constant 0 cannot be generalized *) -lemma lsubd_drop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → +lemma lsubd_drop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ⫃▪[h, g] L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 → - ∃∃K1. G ⊢ K1 ▪⫃[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1. + ∃∃K1. G ⊢ K1 ⫃▪[h, g] K2 & ⇩[s, 0, e] L1 ≡ K1. #h #g #G #L1 #L2 #H elim H -L1 -L2 [ /2 width=3 by ex2_intro/ | #I #L1 #L2 #V #_ #IHL12 #K2 #s #e #H @@ -144,7 +144,7 @@ lemma lsubd_drop_O1_trans: ∀h,g,G,L1,L2. G ⊢ L1 ▪⫃[h, g] L2 → elim (drop_inv_O1_pair1 … H) -H * #He #HLK2 [ destruct elim (IHL12 L2 s 0) -IHL12 // #X #HL12 #H - <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubd_abbr, drop_pair, ex2_intro/ + <(drop_inv_O2 … H) in HL12; -H /3 width=3 by lsubd_beta, drop_pair, ex2_intro/ | elim (IHL12 … HLK2) -L2 /3 width=3 by drop_drop_lt, ex2_intro/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma index 935cd6252..2ccf11bad 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma @@ -20,7 +20,7 @@ include "basic_2/static/lsubd.ma". (* Properties on degree assignment ******************************************) lemma lsubd_da_trans: ∀h,g,G,L2,T,l. ⦃G, L2⦄ ⊢ T ▪[h, g] l → - ∀L1. G ⊢ L1 ▪⫃[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] l. + ∀L1. G ⊢ L1 ⫃▪[h, g] L2 → ⦃G, L1⦄ ⊢ T ▪[h, g] l. #h #g #G #L2 #T #l #H elim H -G -L2 -T -l [ /2 width=1/ | #G #L2 #K2 #V #i #l #HLK2 #_ #IHV #L1 #HL12 @@ -42,7 +42,7 @@ lemma lsubd_da_trans: ∀h,g,G,L2,T,l. ⦃G, L2⦄ ⊢ T ▪[h, g] l → qed-. lemma lsubd_da_conf: ∀h,g,G,L1,T,l. ⦃G, L1⦄ ⊢ T ▪[h, g] l → - ∀L2. G ⊢ L1 ▪⫃[h, g] L2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l. + ∀L2. G ⊢ L1 ⫃▪[h, g] L2 → ⦃G, L2⦄ ⊢ T ▪[h, g] l. #h #g #G #L1 #T #l #H elim H -G -L1 -T -l [ /2 width=1/ | #G #L1 #K1 #V #i #l #HLK1 #HV #IHV #L2 #HL12 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma index 8e1244ee8..15704de44 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma @@ -25,11 +25,11 @@ theorem lsubd_trans: ∀h,g,G. Transitive … (lsubd h g G). elim (lsubd_inv_pair1 … H) -H * #L2 [ #HL2 #H destruct /3 width=1/ | #W #V #l #HV #HW #HL2 #H1 #H2 #H3 destruct - /3 width=3 by lsubd_abbr, lsubd_da_trans/ + /3 width=3 by lsubd_beta, lsubd_da_trans/ ] | #L1 #L #W #V #l #HV #HW #HL1 #IHL1 #X #H elim (lsubd_inv_pair1 … H) -H * #L2 - [ #HL2 #H destruct /3 width=5 by lsubd_abbr, lsubd_da_conf/ + [ #HL2 #H destruct /3 width=5 by lsubd_beta, lsubd_da_conf/ | #W0 #V0 #l0 #_ #_ #_ #H destruct ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma index ab498fc63..4aeecb118 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma @@ -18,9 +18,9 @@ include "basic_2/substitution/drop.ma". (* RESTRICTED LOCAL ENVIRONMENT REFINEMENT **********************************) inductive lsubr: relation lenv ≝ -| lsubr_sort: ∀L. lsubr L (⋆) -| lsubr_bind: ∀I,L1,L2,V. lsubr L1 L2 → lsubr (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lsubr_abst: ∀L1,L2,V,W. lsubr L1 L2 → lsubr (L1.ⓓⓝW.V) (L2.ⓛW) +| lsubr_atom: ∀L. lsubr L (⋆) +| lsubr_pair: ∀I,L1,L2,V. lsubr L1 L2 → lsubr (L1.ⓑ{I}V) (L2.ⓑ{I}V) +| lsubr_beta: ∀L1,L2,V,W. lsubr L1 L2 → lsubr (L1.ⓓⓝW.V) (L2.ⓛW) . interpretation @@ -30,7 +30,7 @@ interpretation (* Basic properties *********************************************************) lemma lsubr_refl: ∀L. L ⫃ L. -#L elim L -L /2 width=1 by lsubr_sort, lsubr_bind/ +#L elim L -L /2 width=1 by lsubr_atom, lsubr_pair/ qed. (* Basic inversion lemmas ***************************************************) @@ -77,7 +77,7 @@ lemma lsubr_fwd_length: ∀L1,L2. L1 ⫃ L2 → |L2| ≤ |L1|. #L1 #L2 #H elim H -L1 -L2 /2 width=1 by monotonic_le_plus_l/ qed-. -lemma lsubr_fwd_drop2_bind: ∀L1,L2. L1 ⫃ L2 → +lemma lsubr_fwd_drop2_pair: ∀L1,L2. L1 ⫃ L2 → ∀I,K2,W,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓑ{I}W → (∃∃K1. K1 ⫃ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓑ{I}W) ∨ ∃∃K1,V. K1 ⫃ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓⓝW.V & I = Abst. @@ -102,6 +102,6 @@ qed-. lemma lsubr_fwd_drop2_abbr: ∀L1,L2. L1 ⫃ L2 → ∀K2,V,s,i. ⇩[s, 0, i] L2 ≡ K2.ⓓV → ∃∃K1. K1 ⫃ K2 & ⇩[s, 0, i] L1 ≡ K1.ⓓV. -#L1 #L2 #HL12 #K2 #V #s #i #HLK2 elim (lsubr_fwd_drop2_bind … HL12 … HLK2) -L2 // * +#L1 #L2 #HL12 #K2 #V #s #i #HLK2 elim (lsubr_fwd_drop2_pair … HL12 … HLK2) -L2 // * #K1 #W #_ #_ #H destruct qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_lsubr.ma index 937f6f78c..f0e171e0b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr_lsubr.ma @@ -18,7 +18,7 @@ include "basic_2/static/lsubr.ma". (* Auxiliary inversion lemmas ***********************************************) -fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → +fact lsubr_inv_pair1_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → ∨∨ L2 = ⋆ | ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓑ{I}X | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW & @@ -30,12 +30,12 @@ fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → ] qed-. -lemma lsubr_inv_bind1: ∀I,K1,L2,X. K1.ⓑ{I}X ⫃ L2 → +lemma lsubr_inv_pair1: ∀I,K1,L2,X. K1.ⓑ{I}X ⫃ L2 → ∨∨ L2 = ⋆ | ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓑ{I}X | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW & I = Abbr & X = ⓝW.V. -/2 width=3 by lsubr_inv_bind1_aux/ qed-. +/2 width=3 by lsubr_inv_pair1_aux/ qed-. (* Main properties **********************************************************) @@ -44,10 +44,10 @@ theorem lsubr_trans: Transitive … lsubr. [ #L1 #X #H lapply (lsubr_inv_atom1 … H) -H // | #I #L1 #L #V #_ #IHL1 #X #H - elim (lsubr_inv_bind1 … H) -H // * - #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1 by lsubr_bind, lsubr_abst/ + elim (lsubr_inv_pair1 … H) -H // * + #L2 [2: #V2 #W2 ] #HL2 #H1 [ #H2 #H3 ] destruct /3 width=1 by lsubr_pair, lsubr_beta/ | #L1 #L #V1 #W #_ #IHL1 #X #H elim (lsubr_inv_abst1 … H) -H // * - #L2 #HL2 #H destruct /3 width=1 by lsubr_abst/ + #L2 #HL2 #H destruct /3 width=1 by lsubr_beta/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sta_lift.ma index 89868cfc3..4d342878f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/sta_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/sta_lift.ma @@ -94,7 +94,7 @@ lemma sta_inv_lift1: ∀h,G. l_deliftable_sn (sta h G). ] qed-. -(* Advanced forvard lemmas **************************************************) +(* Advanced forward lemmas **************************************************) (* Basic_1: was: sty0_correct *) lemma sta_fwd_correct: ∀h,G,L,T,U. ⦃G, L⦄ ⊢ T •[h] U → ∃T0. ⦃G, L⦄ ⊢ U •[h] T0. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma index dcc1cba83..78318917b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_lift.ma @@ -212,7 +212,7 @@ lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → ] qed-. -(* Advancd inversion lemmas on relocation ***********************************) +(* Advanced inversion lemmas on relocation ***********************************) lemma cpy_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶[dt, et] U2 → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/drop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/drop.ma index 12f9a45c9..32b00b4bc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/drop.ma @@ -321,7 +321,7 @@ lemma l_deliftable_sn_llstar: ∀R. l_deliftable_sn R → ] qed-. -(* Basic forvard lemmas *****************************************************) +(* Basic forward lemmas *****************************************************) (* Basic_1: was: drop_S *) lemma drop_fwd_drop2: ∀L1,I2,K2,V2,s,e. ⇩[s, O, e] L1 ≡ K2. ⓑ{I2} V2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma index 46b257efe..17aff3a81 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift.ma @@ -16,7 +16,7 @@ include "basic_2/substitution/lift.ma". (* BASIC TERM RELOCATION ****************************************************) -(* Main properies ***********************************************************) +(* Main properties ***********************************************************) (* Basic_1: was: lift_inj *) theorem lift_inj: ∀d,e,T1,U. ⇧[d,e] T1 ≡ U → ∀T2. ⇧[d,e] T2 ≡ U → T1 = T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma index cdc11129d..d285750a4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lift_lift_vector.ma @@ -17,7 +17,7 @@ include "basic_2/substitution/lift_vector.ma". (* BASIC TERM VECTOR RELOCATION *********************************************) -(* Main properies ***********************************************************) +(* Main properties ***********************************************************) theorem liftv_mono: ∀Ts,U1s,d,e. ⇧[d,e] Ts ≡ U1s → ∀U2s:list term. ⇧[d,e] Ts ≡ U2s → U1s = U2s. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma index b16f8288d..22e058f26 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma @@ -17,7 +17,7 @@ include "basic_2/substitution/lpx_sn.ma". (* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) -(* Properies on dropping ****************************************************) +(* Properties on dropping ****************************************************) lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1,i. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → 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 7ff91fa2d..f95fc0600 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 @@ -47,7 +47,7 @@ table { ] *) [ { "local env. ref. for stratified native validity" * } { - [ "lsubsv ( ? ⊢ ? ¡⫃[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ] + [ "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ] } ] [ { "stratified native validity" * } { @@ -185,7 +185,7 @@ table { class "grass" [ { "static typing" * } { [ { "local env. ref. for degree assignment" * } { - [ "lsubd ( ? ⊢ ? ▪⫃ ? )" "lsubd_da" + "lsubd_lsubd" * ] + [ "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ] } ] [ { "degree assignment" * } { @@ -201,7 +201,7 @@ table { } ] [ { "local env. ref. for atomic arity assignment" * } { - [ "lsuba ( ? ⊢ ? ⁝⫃ ? )" "lsuba_aaa" + "lsuba_lsuba" * ] + [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_aaa" + "lsuba_lsuba" * ] } ] [ { "atomic arity assignment" * } { @@ -273,7 +273,7 @@ table { } ] [ { "local env. ref. for extended substitution" * } { - [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ] + [ "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ] } ] [ { "pointwise extension of a relation" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 557957bea..066d9a1f0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -140,7 +140,7 @@ lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥. (* Iterators ****************************************************************) -(* Note: see also: lib/arithemetcs/bigops.ma *) +(* Note: see also: lib/arithemetics/bigops.ma *) let rec iter (n:nat) (B:Type[0]) (op: B → B) (nil: B) ≝ match n with [ O ⇒ nil -- 2.39.2