From: Ferruccio Guidi Date: Wed, 8 Oct 2014 20:22:55 +0000 (+0000) Subject: - some consequences of preservation added X-Git-Tag: make_still_working~822 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d867d4f21d89308c02d06db83005b91241bc6171;p=helm.git - some consequences of preservation added - some renaming and some notation updated --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma index b4b7fb223..71ed202d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fleq.ma @@ -61,9 +61,9 @@ qed-. (* Advanced properties of "qrst" parallel computation on closures ***********) -lemma fpbs_fpbu_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ → - ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → - ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄. +lemma fpbs_fpb_trans: ∀h,g,F1,F2,K1,K2,T1,T2. ⦃F1, K1, T1⦄ ≥[h, g] ⦃F2, K2, T2⦄ → + ∀G2,L2,U2. ⦃F2, K2, T2⦄ ≻[h, g] ⦃G2, L2, U2⦄ → + ∃∃G1,L1,U1. ⦃F1, K1, T1⦄ ≻[h, g] ⦃G1, L1, U1⦄ & ⦃G1, L1, U1⦄ ≥[h, g] ⦃G2, L2, U2⦄. #h #g #F1 #F2 #K1 #K2 #T1 #T2 #H elim (fpbs_fpbg … H) -H [ #H12 #G2 #L2 #U2 #H2 elim (fleq_fpb_trans … H12 … H2) -F2 -K2 -T2 /3 width=5 by fleq_fpbs, ex2_3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index 4d44edb46..c8359a549 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -31,17 +31,17 @@ interpretation (* Basic eliminators ********************************************************) lemma fsb_ind_alt: ∀h,g. ∀R: relation3 …. ( - ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h,g] T1 → ( + ∀G1,L1,T1. ⦥[h,g] ⦃G1, L1, T1⦄ → ( ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2 ) → R G1 L1 T1 ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → R G L T. + ∀G,L,T. ⦥[h, g] ⦃G, L, T⦄ → R G L T. #h #g #R #IH #G #L #T #H elim H -G -L -T /4 width=1 by fsb_intro/ qed-. (* Basic inversion lemmas ***************************************************) -lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +lemma fsb_inv_csx: ∀h,g,G,L,T. ⦥[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpb_cpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma index f8928c298..6dff4c048 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma @@ -21,34 +21,34 @@ include "basic_2/computation/fsb_csx.ma". (* Main properties **********************************************************) (* Note: this is the "big tree" theorem ("RST" version) *) -theorem aaa_fsb: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥[h, g] T. +theorem aaa_fsb: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦥[h, g] ⦃G, L, T⦄. /3 width=2 by aaa_csx, csx_fsb/ qed. (* Note: this is the "big tree" theorem ("QRST" version) *) -theorem aaa_fsba: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥⦥[h, g] T. +theorem aaa_fsba: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦥⦥[h, g] ⦃G, L, T⦄. /3 width=2 by fsb_fsba, aaa_fsb/ qed. (* Advanced eliminators on atomica arity assignment for terms ***************) -fact aaa_ind_fpbu_aux: ∀h,g. ∀R:relation3 genv lenv term. - (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. -#h #g #R #IH #G #L #T #H @(csx_ind_fpbu … H) -G -L -T +fact aaa_ind_fpb_aux: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ∀A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. +#h #g #R #IH #G #L #T #H @(csx_ind_fpb … H) -G -L -T #G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // #G2 #L2 #T2 #H12 elim (fpbs_aaa_conf h g … G2 … L2 … T2 … HTA1) -A1 /2 width=2 by fpb_fpbs/ qed-. -lemma aaa_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term. - (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → - ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. -/4 width=4 by aaa_ind_fpbu_aux, aaa_csx/ qed-. +lemma aaa_ind_fpb: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → R G L T. +/4 width=4 by aaa_ind_fpb_aux, aaa_csx/ qed-. fact aaa_ind_fpbg_aux: ∀h,g. ∀R:relation3 genv lenv term. (∀G1,L1,T1,A. ⦃G1, L1⦄ ⊢ T1 ⁝ A → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma index cf966232a..00fe4a67e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma @@ -31,26 +31,26 @@ interpretation (* Basic eliminators ********************************************************) lemma fsba_ind_alt: ∀h,g. ∀R: relation3 …. ( - ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥⦥[h,g] T1 → ( + ∀G1,L1,T1. ⦥⦥[h,g] ⦃G1, L1, T1⦄ → ( ∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2 ) → R G1 L1 T1 ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → R G L T. + ∀G,L,T. ⦥⦥[h, g] ⦃G, L, T⦄ → R G L T. #h #g #R #IH #G #L #T #H elim H -G -L -T /4 width=1 by fsba_intro/ qed-. (* Basic properties *********************************************************) -lemma fsba_fpbs_trans: ∀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. +lemma fsba_fpbs_trans: ∀h,g,G1,L1,T1. ⦥⦥[h, g] ⦃G1, L1, T1⦄ → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦥⦥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #L1 #T1 #H @(fsba_ind_alt … H) -G1 -L1 -T1 /4 width=5 by fsba_intro, fpbs_fpbg_trans/ qed-. (* Main properties **********************************************************) -theorem fsb_fsba: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥⦥[h, g] T. +theorem fsb_fsba: ∀h,g,G,L,T. ⦥[h, g] ⦃G, L, T⦄ → ⦥⦥[h, g] ⦃G, L, T⦄. #h #g #G #L #T #H @(fsb_ind_alt … H) -G -L -T #G1 #L1 #T1 #_ #IH @fsba_intro #G2 #L2 #T2 * /3 width=5 by fsba_fpbs_trans/ @@ -58,25 +58,25 @@ qed. (* Main inversion lemmas ****************************************************) -theorem fsba_inv_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. +theorem fsba_inv_fsb: ∀h,g,G,L,T. ⦥⦥[h, g] ⦃G, L, T⦄ → ⦥[h, g] ⦃G, L, T⦄. #h #g #G #L #T #H @(fsba_ind_alt … H) -G -L -T /4 width=1 by fsb_intro, fpb_fpbg/ qed-. (* Advanced properties ******************************************************) -lemma fsb_fpbs_trans: ∀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. +lemma fsb_fpbs_trans: ∀h,g,G1,L1,T1. ⦥[h, g] ⦃G1, L1, T1⦄ → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦥[h, g] ⦃G2, L2, T2⦄. /4 width=5 by fsba_inv_fsb, fsb_fsba, fsba_fpbs_trans/ qed-. (* Advanced eliminators *****************************************************) lemma fsb_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term. - (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → + (∀G1,L1,T1. ⦥[h, g] ⦃G1, L1, T1⦄ → (∀G2,L2,T2. ⦃G1, L1, T1⦄ >≡[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → R G1 L1 T1 ) → - ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → R G1 L1 T1. + ∀G1,L1,T1. ⦥[h, g] ⦃G1, L1, T1⦄ → R G1 L1 T1. #h #g #R #IH #G1 #L1 #T1 #H @(fsba_ind_alt h g … G1 L1 T1) /3 width=1 by fsba_inv_fsb, fsb_fsba/ qed-. 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 38cbe5c16..54284a0b1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -23,7 +23,7 @@ include "basic_2/computation/fsb_alt.ma". (* 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. + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #L1 #T1 #H @(csx_ind … H) -T1 #T1 #HT1 #IHc #G2 #L2 #T2 @(fqup_wf_ind … G2 L2 T2) -G2 -L2 -T2 #G0 #L0 #T0 #IHu #H10 lapply (csx_fpbs_conf … H10) // -HT1 @@ -48,17 +48,17 @@ lemma csx_fsb_fpbs: ∀h,g,G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → ] qed. -lemma csx_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. +lemma csx_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦥[h, g] ⦃G, L, T⦄. /2 width=5 by csx_fsb_fpbs/ qed. (* Advanced eliminators *****************************************************) -lemma csx_ind_fpbu: ∀h,g. ∀R:relation3 genv lenv term. - (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → - R G1 L1 T1 - ) → - ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T. +lemma csx_ind_fpb: ∀h,g. ∀R:relation3 genv lenv term. + (∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + R G1 L1 T1 + ) → + ∀G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → R G L T. /4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-. lemma csx_ind_fpbg: ∀h,g. ∀R:relation3 genv lenv term. 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 5f76fea80..8376ac4c1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_preserve.ma @@ -59,3 +59,36 @@ lemma snv_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → #h #g #G #L1 #T1 #HT1 #T2 #H @(cprs_ind … H) -T2 /3 width=5 by snv_cpr_lpr/ qed-. + +lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. +#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H +@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/ +qed-. + +lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → + ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → + ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H +@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ] +#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 +elim (IHT1 L1) // -IHT1 #U #HTU #HU1 +elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2 +[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1 +/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ +qed-. + +lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 → + ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] → + ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 → + ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. +#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12 +elim (cpcs_inv_cprs … H) -H #T #H1 #H2 +elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1 +elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2 +lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc index 578937f4c..8da0347aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/snv_preserve.etc @@ -1,10 +1,3 @@ -lemma da_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. -#h #g #G #L1 #T1 #HT1 #l #Hl #T2 #H -@(cprs_ind … H) -T2 /3 width=6 by snv_cprs_lpr, da_cpr_lpr/ -qed-. - lemma da_cpcs: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ T1 ¡[h, g] → ∀T2. ⦃G, L⦄ ⊢ T2 ¡[h, g] → ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 → @@ -23,32 +16,6 @@ elim (lstas_cpr_lpr … 1 … Hl U1 … HT12 … HL12) -Hl -HT12 -HL12 /3 width=3 by lstas_inv_SO, sta_lstas, ex2_intro/ qed-. -lemma lstas_cprs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l1,l2. l2 ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → - ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l2] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → - ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G #L1 #T1 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H -@(cprs_ind … H) -T2 [ /2 width=10 by lstas_cpr_lpr/ ] -#T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 -elim (IHT1 L1) // -IHT1 #U #HTU #HU1 -elim (lstas_cpr_lpr … g … Hl21 … HTU … HTT2 … HL12) -HTU -HTT2 -[2,3: /2 width=7 by snv_cprs_lpr, da_cprs_lpr/ ] -T1 -T -l1 -/4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ -qed-. - -lemma lstas_cpcs_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → - ∀l,l1. l ≤ l1 → ⦃G, L1⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •*[h, l] U1 → - ∀T2. ⦃G, L1⦄ ⊢ T2 ¡[h, g] → - ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, l] U2 → - ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. -#h #g #G #L1 #T1 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12 -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (lstas_cprs_lpr … HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 #W1 #H1 #HUW1 -elim (lstas_cprs_lpr … HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 #W2 #H2 #HUW2 -lapply (lstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ -qed-. - lemma snv_sta: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ T ¡[h, g] → ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ∀U. ⦃G, L⦄ ⊢ T •[h] U → ⦃G, L⦄ ⊢ U ¡[h, g]. @@ -82,3 +49,30 @@ lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H elim (cpcs_inv_cprs … H) -H /3 width=7 by ex4_3_intro, ex2_intro/ qed-. + +(* Note: missing da_scpds_lpr, da_scpes *) + +lemma scpds_cpr_lpr: ∀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 #G #L1 #T1 #HT1 #U1 #l2 * #W1 #l1 #Hl21 #HTl1 #HTW1 #HWU1 #T2 #HT12 #L2 #HL12 +elim (lstas_cpr_lpr … HTl1 … HTW1 … HT12 … HL12) // #W2 #HTW2 #HW12 +lapply (da_cpr_lpr … HTl1 … HT12 … HL12) // -T1 +lapply (lpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 +lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H +elim (cpcs_inv_cprs … H) -H /3 width=6 by ex4_2_intro, ex2_intro/ +qed-. + +lemma scpes_cpr_lpr: ∀h,g,G,L1,T1. ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + ∀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 #G #L1 #T1 #HT1 #T2 #HT2 #l1 #l2 * #T0 #HT10 #HT20 #U1 #HTU1 #U2 #HTU2 #L2 #HL12 +elim (scpds_cpr_lpr … HT10 … HTU1 … HL12) -HT10 -HTU1 // #X1 #HUX1 #H1 +elim (scpds_cpr_lpr … HT20 … HTU2 … HL12) -HT20 -HTU2 // #X2 #HUX2 #H2 +elim (cprs_conf … H1 … H2) -T0 /3 width=5 by scpds_div, scpds_cprs_trans/ +qed-. + +(* Note: missing lstas_scpds, scpes_le *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma index d6c4f4259..207ba13bf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⦥ break [ term 46 h , break term 46 g ] break term 46 T )" +notation "hvbox( ⦥ [ term 46 h, break term 46 g ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )" non associative with precedence 45 for @{ 'BTSN $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma index 44976571b..7c6d69120 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⦥ ⦥ break [ term 46 h , break term 46 g ] break term 46 T )" +notation "hvbox( ⦥ ⦥ [ term 46 h, break term 46 g ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )" non associative with precedence 45 for @{ 'BTSNAlt $h $g $G $L $T }. 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 9ac05c7b6..1723a0005 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 @@ -88,7 +88,7 @@ table { } ] [ { "strongly normalizing qrst-computation" * } { - [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_aaa" + "fsb_csx" * ] + [ "fsb ( ⦥[?,?] ⦃?,?,?⦄ )" "fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )" "fsb_aaa" + "fsb_csx" * ] } ] [ { "strongly normalizing rt-computation" * } {