From: Ferruccio Guidi Date: Sat, 12 Oct 2013 17:38:16 +0000 (+0000) Subject: some renaming ... X-Git-Tag: make_still_working~1083 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ad8c044ab33ea0f2aebb1c40fa20340d7f2f3eb;p=helm.git some renaming ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma index 182043d3b..8028270d6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/fsups_fsups.ma". +include "basic_2/substitution/fqus_fqus.ma". include "basic_2/unfold/lsstas_lift.ma". include "basic_2/reduction/cpx_lift.ma". include "basic_2/computation/cpxs.ma". @@ -71,47 +71,47 @@ qed-. (* Properties on supclosure *************************************************) -lemma fsupq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → - ∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. +lemma fquq_cpxs_trans: ∀h,g,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → + ∀T1. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. #h #g #G1 #G2 #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 -[ /3 width=3 by fsupq_fsups, ex2_intro/ +[ /3 width=3 by fquq_fqus, ex2_intro/ | #T #T2 #HT2 #_ #IHTU2 #T1 #HT1 - elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2 + elim (fquq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2 elim (IHTU2 … HT2) -T2 /3 width=3 by cpxs_strap2, ex2_intro/ ] qed-. -lemma fsupq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → - ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. -/3 width=5 by fsupq_cpxs_trans, lsstas_cpxs/ qed-. +lemma fquq_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → + ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. +/3 width=5 by fquq_cpxs_trans, lsstas_cpxs/ qed-. -lemma fsups_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 +lemma fqus_cpxs_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 [ /2 width=3 by ex2_intro/ | #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 - elim (fsupq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2 - elim (IHT1 … HT2) -T /3 width=7 by fsups_trans, ex2_intro/ + elim (fquq_cpxs_trans … HTU2 … HT2) -T2 #T2 #HT2 #HTU2 + elim (IHT1 … HT2) -T /3 width=7 by fqus_trans, ex2_intro/ ] qed-. -lemma fsups_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → - ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. -/3 width=7 by fsups_cpxs_trans, lsstas_cpxs/ qed-. +lemma fqus_lsstas_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀U2,l1. ⦃G2, L2⦄ ⊢ T2 •*[h, g, l1] U2 → + ∀l2. ⦃G2, L2⦄ ⊢ T2 ▪ [h, g] l2 → l1 ≤ l2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. +/3 width=7 by fqus_cpxs_trans, lsstas_cpxs/ qed-. -lemma fsups_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 +lemma fqus_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h, g] U2 → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊃* ⦃G2, L2, U2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 [ /2 width=3 by ex2_intro/ | #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 - elim (fsupq_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2 - elim (IHT1 … HT2) -T /3 width=7 by fsups_strap1, ex2_intro/ + elim (fquq_cpx_trans … HT2 … HTU2) -T2 #T2 #HT2 #HTU2 + elim (IHT1 … HT2) -T /3 width=7 by fqus_strap1, ex2_intro/ ] -qed-. \ No newline at end of file +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index 5a7e77736..f400f5c43 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstarproper_8.ma". -include "basic_2/substitution/fsupp.ma". +include "basic_2/substitution/fqup.ma". include "basic_2/reduction/fpbc.ma". include "basic_2/computation/fpbs.ma". @@ -68,9 +68,9 @@ lemma fpbs_fpbg_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L /3 width=5 by fpbg_strap2/ qed-. -lemma fsupp_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 -/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fsup, fpb_fsupq, fsup_fsupq/ +lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … L2 T2 H) -G2 -L2 -T2 +/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fqu, fpb_fquq, fqu_fquq/ qed. lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index 00f4a93aa..8d42f50bf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstar_8.ma". -include "basic_2/substitution/fsups.ma". +include "basic_2/substitution/fqus.ma". include "basic_2/reduction/fpb.ma". include "basic_2/computation/cpxs.ma". include "basic_2/computation/lpxs.ma". @@ -55,10 +55,10 @@ lemma fpbs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. /2 width=5 by tri_TC_strap/ qed-. -lemma fsups_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … L2 T2 H) -G2 -L2 -T2 -/3 width=5 by fpb_fsupq, tri_step/ +lemma fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … L2 T2 H) -G2 -L2 -T2 +/3 width=5 by fpb_fquq, tri_step/ qed. lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma index 1b0471ddb..9e5336c04 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma @@ -34,11 +34,11 @@ lemma fpb_fpbsa_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L ∀G2,L2,T2. ⦃G, L, T⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #L1 #L #T1 #T * -G -L -T [ #G #L #T #HG1 | #T #HT1 | #L #HL1 ] #G2 #L2 #T2 * #L0 #T0 #HT0 #HG2 #HL02 -[ elim (fsupq_cpxs_trans … HT0 … HG1) -T - /3 width=7 by fsups_trans, ex3_2_intro/ +[ elim (fquq_cpxs_trans … HT0 … HG1) -T + /3 width=7 by fqus_trans, ex3_2_intro/ | /3 width=5 by cpxs_strap2, ex3_2_intro/ | lapply (lpx_cpxs_trans … HT0 … HL1) -HT0 - elim (lpx_fsups_trans … HG2 … HL1) -L + elim (lpx_fqus_trans … HG2 … HL1) -L /3 width=7 by lpxs_strap2, cpxs_trans, ex3_2_intro/ ] qed-. @@ -56,5 +56,5 @@ qed. theorem fpbsa_inv_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -/4 width=5 by fpbs_trans, fsups_fpbs, cpxs_fpbs, lpxs_fpbs/ +/4 width=5 by fpbs_trans, fqus_fpbs, cpxs_fpbs, lpxs_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma index 7330188e9..2d197c95b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma @@ -89,34 +89,34 @@ lemma lpxs_pair2: ∀h,g,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (* Properties on supclosure *************************************************) -lemma lpxs_fsupq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. +lemma lpxs_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #HT12 #K1 #H @(lpxs_ind_dx … H) -K1 [ /2 width=5 by ex3_2_intro/ | #K1 #K #HK1 #_ * #L #T #HT1 #HT2 #HL2 -HT12 lapply (lpx_cpxs_trans … HT1 … HK1) -HT1 - elim (lpx_fsupq_trans … HT2 … HK1) -K + elim (lpx_fquq_trans … HT2 … HK1) -K /3 width=7 by lpxs_strap2, cpxs_strap1, ex3_2_intro/ ] qed-. -lemma lpxs_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ +lemma lpxs_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 -#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fsupq_trans … H2 … HL0) -L -#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpxs_trans … HT0 … HT3) -T -/3 width=7 by cpxs_trans, fsups_strap1, ex3_2_intro/ +#L0 #T0 #HT10 #HT0 #HL0 elim (lpxs_fquq_trans … H2 … HL0) -L +#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT0 … HT3) -T +/3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/ qed-. -lemma lpx_fsups_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → - ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ +lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /2 width=5 by ex3_2_intro/ #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 -#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fsupq_trans … H2 … HL0) -L -#L #T3 #HT3 #HT32 #HL2 elim (fsups_cpx_trans … HT0 … HT3) -T -/3 width=7 by cpxs_strap1, fsups_strap1, ex3_2_intro/ +#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L +#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T +/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/ qed-. 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 71c688c21..d1363a3cf 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 @@ -36,17 +36,17 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (ldrop_mono … H … HLK1) -H #H destruct elim (cpr_inv_lref1 … H3) -H3 [1,3: #H destruct - lapply (fsupp_lref … G1 … HLK1) + lapply (fqup_lref … G1 … HLK1) elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - /4 width=10 by da_ldef, da_ldec, fsupp_fpbg/ + /4 width=10 by da_ldef, da_ldec, fqup_fpbg/ |2,4: * #K0 #V0 #W0 #H #HVW0 #HW0 lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (fsupp_lref … G1 … HLK1) + lapply (fqup_lref … G1 … HLK1) elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct lapply (ldrop_fwd_ldrop2 … HLK2) -V2 - /4 width=7 by da_lift, fsupp_fpbg/ + /4 width=7 by da_lift, fqup_fpbg/ ] | #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) @@ -55,15 +55,15 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (da_inv_bind … H2) -H2 elim (cpr_inv_bind1 … H3) -H3 * [ #V2 #T2 #HV12 #HT12 #H destruct - /4 width=9 by da_bind, fsupp_fpbg, lpr_pair/ + /4 width=9 by da_bind, fqup_fpbg, lpr_pair/ | #T2 #HT12 #HT2 #H1 #H2 destruct - /4 width=11 by da_inv_lift, fsupp_fpbg, lpr_pair, ldrop_ldrop/ + /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_ldrop/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10 lapply (da_inv_flat … H2) -H2 #Hl elim (cpr_inv_appl1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fsupp_fpbg/ + [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbg/ | #b #V2 #W #W2 #U1 #U2 #HV12 #HW2 #HU12 #H1 #H2 destruct elim (snv_inv_bind … HT1) -HT1 #HW #HU1 lapply (da_inv_bind … Hl) -Hl #Hl @@ -71,24 +71,24 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (cprs_div … HW3 … HW10) -W3 #HWW1 lapply (ssta_da_conf … HVW1 … Hl0) (plus_minus_m_m e 1) /2 width=3 by fqu_drop/ +qed. + +lemma fqu_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄. +/3 width=3 by fqu_drop, ldrop_ldrop, lift_lref_ge_minus/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma fqu_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // +#G #L #K #T #U #e #HLK #HTU +lapply (ldrop_fwd_lw_lt … HLK ?) -HLK // #HKL +lapply (lift_fwd_tw … HTU) -e #H +normalize in ⊢ (?%%); /2 width=1 by lt_minus_to_plus/ +qed-. + +fact fqu_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + ∀i. T1 = #i → |L2| < |L1|. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[1: normalize // +|3: #a +|5: /2 width=4 by ldrop_fwd_length_lt4/ +] #I #G #L #V #T #j #H destruct +qed-. + +lemma fqu_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃ ⦃G2, L2, T2⦄ → |L2| < |L1|. +/2 width=7 by fqu_fwd_length_lref1_aux/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma new file mode 100644 index 000000000..de000da70 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/suptermopt_6.ma". +include "basic_2/relocation/fqu.ma". + +(* OPTIONAL SUPCLOSURE ******************************************************) + +(* activate genv *) +inductive fquq: tri_relation genv lenv term ≝ +| fquq_lref_O : ∀I,G,L,V. fquq G (L.ⓑ{I}V) (#0) G L V +| fquq_pair_sn: ∀I,G,L,V,T. fquq G L (②{I}V.T) G L V +| fquq_bind_dx: ∀a,I,G,L,V,T. fquq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T +| fquq_flat_dx: ∀I,G, L,V,T. fquq G L (ⓕ{I}V.T) G L T +| fquq_drop : ∀G,L,K,T,U,e. + ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fquq G L U G K T +. + +interpretation + "optional structural successor (closure)" + 'SupTermOpt G1 L1 T1 G2 L2 T2 = (fquq G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma fquq_refl: tri_reflexive … fquq. +/2 width=3 by fquq_drop/ qed. + +lemma fqu_fquq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=3 by fquq_drop/ +qed. + +(* Basic forward lemmas *****************************************************) + +lemma fquq_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /2 width=1 by lt_to_le/ +#G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 +lapply (ldrop_fwd_lw … HLK1) -HLK1 +lapply (lift_fwd_tw … HTU1) -HTU1 +/2 width=1 by le_plus, le_n/ +qed-. + +fact fquq_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ∀i. T1 = #i → |L2| ≤ |L1|. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // +[ #a #I #G #L #V #T #j #H destruct +| #G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #i #H destruct + /2 width=3 by ldrop_fwd_length_le4/ +] +qed-. + +lemma fquq_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃⸮ ⦃G2, L2, T2⦄ → |L2| ≤ |L1|. +/2 width=7 by fquq_fwd_length_lref1_aux/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma new file mode 100644 index 000000000..1d770dcc4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_alt.ma @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/suptermoptalt_6.ma". +include "basic_2/relocation/fquq.ma". + +(* OPTIONAL SUPCLOSURE ******************************************************) + +(* alternative definition of fquq *) +definition fquqa: tri_relation genv lenv term ≝ tri_RC … fqu. + +interpretation + "optional structural successor (closure) alternative" + 'SupTermOptAlt G1 L1 T1 G2 L2 T2 = (fquqa G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma fquqa_refl: tri_reflexive … fquqa. +// qed. + +lemma fquqa_drop: ∀G,L,K,T,U,e. + ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄. +#G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e) +/3 width=5 by fqu_drop_lt, or_introl/ #H destruct +>(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T // +qed. + +(* Main properties **********************************************************) + +theorem fquq_fquqa: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/2 width=3 by fquqa_drop, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, or_introl/ +qed. + +(* Main inversion properties ************************************************) + +theorem fquqa_inv_fquq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1 by fqu_fquq/ +* #H1 #H2 #H3 destruct // +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma fquq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2). +#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fquq_fquqa … H) -H [| * ] +/2 width=1 by or_introl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma deleted file mode 100644 index 9719b4992..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsup.ma +++ /dev/null @@ -1,67 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/supterm_6.ma". -include "basic_2/grammar/cl_weight.ma". -include "basic_2/relocation/ldrop.ma". - -(* SUPCLOSURE ***************************************************************) - -(* activate genv *) -inductive fsup: tri_relation genv lenv term ≝ -| fsup_lref_O : ∀I,G,L,V. fsup G (L.ⓑ{I}V) (#0) G L V -| fsup_pair_sn: ∀I,G,L,V,T. fsup G L (②{I}V.T) G L V -| fsup_bind_dx: ∀a,I,G,L,V,T. fsup G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T -| fsup_flat_dx: ∀I,G,L,V,T. fsup G L (ⓕ{I}V.T) G L T -| fsup_drop : ∀G,L,K,T,U,e. - ⇩[0, e+1] L ≡ K → ⇧[0, e+1] T ≡ U → fsup G L U G K T -. - -interpretation - "structural successor (closure)" - 'SupTerm G1 L1 T1 G2 L2 T2 = (fsup G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma fsup_drop_lt: ∀G,L,K,T,U,e. 0 < e → - ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsup G L U G K T. -#G #L #K #T #U #e #He >(plus_minus_m_m e 1) /2 width=3 by fsup_drop/ -qed. - -lemma fsup_lref_S_lt: ∀I,G,L,V,i. 0 < i → ⦃G, L.ⓑ{I}V, #i⦄ ⊃ ⦃G, L, #(i-1)⦄. -/3 width=3 by fsup_drop, ldrop_ldrop, lift_lref_ge_minus/ -qed. - -(* Basic forward lemmas *****************************************************) - -lemma fsup_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // -#G #L #K #T #U #e #HLK #HTU -lapply (ldrop_fwd_lw_lt … HLK ?) -HLK // #HKL -lapply (lift_fwd_tw … HTU) -e #H -normalize in ⊢ (?%%); /2 width=1 by lt_minus_to_plus/ -qed-. - -fact fsup_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀i. T1 = #i → |L2| < |L1|. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[1: normalize // -|3: #a -|5: /2 width=4 by ldrop_fwd_length_lt4/ -] #I #G #L #V #T #j #H destruct -qed-. - -lemma fsup_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃ ⦃G2, L2, T2⦄ → |L2| < |L1|. -/2 width=7 by fsup_fwd_length_lref1_aux/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma deleted file mode 100644 index 0a48ca02a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq.ma +++ /dev/null @@ -1,64 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/suptermopt_6.ma". -include "basic_2/relocation/fsup.ma". - -(* OPTIONAL SUPCLOSURE ******************************************************) - -(* activate genv *) -inductive fsupq: tri_relation genv lenv term ≝ -| fsupq_lref_O : ∀I,G,L,V. fsupq G (L.ⓑ{I}V) (#0) G L V -| fsupq_pair_sn: ∀I,G,L,V,T. fsupq G L (②{I}V.T) G L V -| fsupq_bind_dx: ∀a,I,G,L,V,T. fsupq G L (ⓑ{a,I}V.T) G (L.ⓑ{I}V) T -| fsupq_flat_dx: ∀I,G, L,V,T. fsupq G L (ⓕ{I}V.T) G L T -| fsupq_drop : ∀G,L,K,T,U,e. - ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → fsupq G L U G K T -. - -interpretation - "optional structural successor (closure)" - 'SupTermOpt G1 L1 T1 G2 L2 T2 = (fsupq G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma fsupq_refl: tri_reflexive … fsupq. -/2 width=3 by fsupq_drop/ qed. - -lemma fsup_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 // /2 width=3 by fsupq_drop/ -qed. - -(* Basic forward lemmas *****************************************************) - -lemma fsupq_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /2 width=1 by lt_to_le/ -#G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 -lapply (ldrop_fwd_lw … HLK1) -HLK1 -lapply (lift_fwd_tw … HTU1) -HTU1 -/2 width=1 by le_plus, le_n/ -qed-. - -fact fsupq_fwd_length_lref1_aux: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀i. T1 = #i → |L2| ≤ |L1|. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // -[ #a #I #G #L #V #T #j #H destruct -| #G1 #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #i #H destruct - /2 width=3 by ldrop_fwd_length_le4/ -] -qed-. - -lemma fsupq_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃⸮ ⦃G2, L2, T2⦄ → |L2| ≤ |L1|. -/2 width=7 by fsupq_fwd_length_lref1_aux/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma deleted file mode 100644 index cfbca8693..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma +++ /dev/null @@ -1,59 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/suptermoptalt_6.ma". -include "basic_2/relocation/fsupq.ma". - -(* OPTIONAL SUPCLOSURE ******************************************************) - -(* alternative definition of fsupq *) -definition fsupqa: tri_relation genv lenv term ≝ tri_RC … fsup. - -interpretation - "optional structural successor (closure) alternative" - 'SupTermOptAlt G1 L1 T1 G2 L2 T2 = (fsupqa G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma fsupqa_refl: tri_reflexive … fsupqa. -// qed. - -lemma fsupqa_drop: ∀G,L,K,T,U,e. - ⇩[0, e] L ≡ K → ⇧[0, e] T ≡ U → ⦃G, L, U⦄ ⊃⊃⸮ ⦃G, K, T⦄. -#G #L #K #T #U #e #HLK #HTU elim (eq_or_gt e) -/3 width=5 by fsup_drop_lt, or_introl/ #H destruct ->(ldrop_inv_O2 … HLK) -L >(lift_inv_O2 … HTU) -T // -qed. - -(* Main properties **********************************************************) - -theorem fsupq_fsupqa: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/2 width=3 by fsupqa_drop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/ -qed. - -(* Main inversion properties ************************************************) - -theorem fsupqa_inv_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1 by fsup_fsupq/ -* #H1 #H2 #H3 destruct // -qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma fsupq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → -⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2). -#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fsupq_fsupqa … H) -H [| * ] -/2 width=1 by or_introl/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma new file mode 100644 index 000000000..c4c26fde2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma @@ -0,0 +1,102 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/suptermplus_6.ma". +include "basic_2/relocation/fqu.ma". + +(* PLUS-ITERATED SUPCLOSURE *************************************************) + +definition fqup: tri_relation genv lenv term ≝ tri_TC … fqu. + +interpretation "plus-iterated structural successor (closure)" + 'SupTermPlus G1 L1 T1 G2 L2 T2 = (fqup G1 L1 T1 G2 L2 T2). + +(* Basic properties *********************************************************) + +lemma fqu_fqup: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. +/2 width=1 by tri_inj/ qed. + +lemma fqup_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. +/2 width=5 by tri_step/ qed. + +lemma fqup_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. + ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. +/2 width=5 by tri_TC_strap/ qed. + +lemma fqup_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → + ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄. +#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct +[ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 // +| /3 width=5 by fqup_strap2, fqu_drop_lt/ +] +qed-. + +lemma fqup_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄. +/3 width=6 by fqu_lref_O, fqu_fqup, lift_lref_ge, fqup_ldrop/ qed. + +lemma fqup_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄. +/2 width=1 by fqu_pair_sn, fqu_fqup/ qed. + +lemma fqup_bind_dx: ∀a,I,G,L,V,T. ⦃G, L, ⓑ{a,I}V.T⦄ ⊃+ ⦃G, L.ⓑ{I}V, T⦄. +/2 width=1 by fqu_bind_dx, fqu_fqup/ qed. + +lemma fqup_flat_dx: ∀I,G,L,V,T. ⦃G, L, ⓕ{I}V.T⦄ ⊃+ ⦃G, L, T⦄. +/2 width=1 by fqu_flat_dx, fqu_fqup/ qed. + +lemma fqup_flat_dx_pair_sn: ∀I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃G, L, V2⦄. +/2 width=5 by fqu_pair_sn, fqup_strap1/ qed. + +lemma fqup_bind_dx_flat_dx: ∀a,G,I1,I2,L,V1,V2,T. ⦃G, L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I1}V1, T⦄. +/2 width=5 by fqu_flat_dx, fqup_strap1/ qed. + +lemma fqup_flat_dx_bind_dx: ∀a,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I2}V2, T⦄. +/2 width=5 by fqu_bind_dx, fqup_strap1/ qed. + +(* Basic eliminators ********************************************************) + +lemma fqup_ind: ∀G1,L1,T1. ∀R:relation3 …. + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2. +#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H +@(tri_TC_ind … IH1 IH2 G2 L2 T2 H) +qed-. + +lemma fqup_ind_dx: ∀G2,L2,T2. ∀R:relation3 …. + (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G1 L1 T1) → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G1 L1 T1. +#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H +@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H) +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma fqup_fwd_fw: ∀G1,G2,L1,L2,T1,T2. + ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}. +#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/3 width=3 by fqu_fwd_fw, transitive_lt/ +qed-. + +(* Advanced eliminators *****************************************************) + +lemma fqup_wf_ind: ∀R:relation3 …. ( + ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2) → + ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2 + ) → ∀G1,L1,T1. R G1 L1 T1. +#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=7 by fqup_fwd_fw/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma new file mode 100644 index 000000000..a6bff5ede --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_fqup.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/fqup.ma". + +(* PLUS-ITERATED SUPCLOSURE *************************************************) + +(* Main propertis ***********************************************************) + +theorem fqup_trans: tri_transitive … fqup. +/2 width=5 by tri_TC_transitive/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma new file mode 100644 index 000000000..ef5af3100 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/suptermstar_6.ma". +include "basic_2/relocation/fquq.ma". + +(* STAR-ITERATED SUPCLOSURE *************************************************) + +definition fqus: tri_relation genv lenv term ≝ tri_TC … fquq. + +interpretation "star-iterated structural successor (closure)" + 'SupTermStar G1 L1 T1 G2 L2 T2 = (fqus G1 L1 T1 G2 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma fqus_ind: ∀G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 → + (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2. +#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H +@(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) // +qed-. + +lemma fqus_ind_dx: ∀G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G1 L1 T1. +#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H +@(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) // +qed-. + +(* Basic properties *********************************************************) + +lemma fqus_refl: tri_reflexive … fqus. +/2 width=1 by tri_inj/ qed. + +lemma fquq_fqus: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. +/2 width=1 by tri_inj/ qed. + +lemma fqus_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. +/2 width=5 by tri_step/ qed. + +lemma fqus_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. +/2 width=5 by tri_TC_strap/ qed. + +lemma fqus_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ → + ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → + ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄. +#G1 #G2 #K1 #K2 #T1 #T2 #H @(fqus_ind … H) -G2 -K2 -T2 +/3 width=5 by fqus_strap1, fquq_fqus, fquq_drop/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma fqus_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}. +#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -L2 -T2 +/3 width=3 by fquq_fwd_fw, transitive_le/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma new file mode 100644 index 000000000..295d45b17 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_fqus.ma @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/fqus.ma". + +(* STAR-ITERATED SUPCLOSURE *************************************************) + +(* Main properties **********************************************************) + +theorem fqus_trans: tri_transitive … fqus. +/2 width=5 by tri_TC_transitive/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma deleted file mode 100644 index 3c8da530a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp.ma +++ /dev/null @@ -1,102 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/suptermplus_6.ma". -include "basic_2/relocation/fsup.ma". - -(* PLUS-ITERATED SUPCLOSURE *************************************************) - -definition fsupp: tri_relation genv lenv term ≝ tri_TC … fsup. - -interpretation "plus-iterated structural successor (closure)" - 'SupTermPlus G1 L1 T1 G2 L2 T2 = (fsupp G1 L1 T1 G2 L2 T2). - -(* Basic properties *********************************************************) - -lemma fsup_fsupp: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. -/2 width=1 by tri_inj/ qed. - -lemma fsupp_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. -/2 width=5 by tri_step/ qed. - -lemma fsupp_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. - ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. -/2 width=5 by tri_TC_strap/ qed. - -lemma fsupp_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → - ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄. -#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct -[ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 // -| /3 width=5 by fsupp_strap2, fsup_drop_lt/ -] -qed-. - -lemma fsupp_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄. -/3 width=6 by fsup_lref_O, fsup_fsupp, lift_lref_ge, fsupp_ldrop/ qed. - -lemma fsupp_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄. -/2 width=1 by fsup_pair_sn, fsup_fsupp/ qed. - -lemma fsupp_bind_dx: ∀a,I,G,L,V,T. ⦃G, L, ⓑ{a,I}V.T⦄ ⊃+ ⦃G, L.ⓑ{I}V, T⦄. -/2 width=1 by fsup_bind_dx, fsup_fsupp/ qed. - -lemma fsupp_flat_dx: ∀I,G,L,V,T. ⦃G, L, ⓕ{I}V.T⦄ ⊃+ ⦃G, L, T⦄. -/2 width=1 by fsup_flat_dx, fsup_fsupp/ qed. - -lemma fsupp_flat_dx_pair_sn: ∀I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃G, L, V2⦄. -/2 width=5 by fsup_pair_sn, fsupp_strap1/ qed. - -lemma fsupp_bind_dx_flat_dx: ∀a,G,I1,I2,L,V1,V2,T. ⦃G, L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I1}V1, T⦄. -/2 width=5 by fsup_flat_dx, fsupp_strap1/ qed. - -lemma fsupp_flat_dx_bind_dx: ∀a,I1,I2,G,L,V1,V2,T. ⦃G, L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃G, L.ⓑ{I2}V2, T⦄. -/2 width=5 by fsup_bind_dx, fsupp_strap1/ qed. - -(* Basic eliminators ********************************************************) - -lemma fsupp_ind: ∀G1,L1,T1. ∀R:relation3 …. - (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G2 L2 T2) → - (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2. -#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H -@(tri_TC_ind … IH1 IH2 G2 L2 T2 H) -qed-. - -lemma fsupp_ind_dx: ∀G2,L2,T2. ∀R:relation3 …. - (∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → R G1 L1 T1) → - (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃+ ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G1 L1 T1. -#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H -@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H) -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma fsupp_fwd_fw: ∀G1,G2,L1,L2,T1,T2. - ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} < ♯{G1, L1, T1}. -#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … H) -G2 -L2 -T2 -/3 width=3 by fsup_fwd_fw, transitive_lt/ -qed-. - -(* Advanced eliminators *****************************************************) - -lemma fsupp_wf_ind: ∀R:relation3 …. ( - ∀G1,L1,T1. (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → R G2 L2 T2) → - ∀G2,L2,T2. G1 = G2 → L1 = L2 → T1 = T2 → R G2 L2 T2 - ) → ∀G1,L1,T1. R G1 L1 T1. -#R #HR @(f3_ind … fw) #n #IHn #G1 #L1 #T1 #H destruct /4 width=7 by fsupp_fwd_fw/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma deleted file mode 100644 index a8422e6eb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsupp_fsupp.ma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/substitution/fsupp.ma". - -(* PLUS-ITERATED SUPCLOSURE *************************************************) - -(* Main propertis ***********************************************************) - -theorem fsupp_trans: tri_transitive … fsupp. -/2 width=5 by tri_TC_transitive/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma deleted file mode 100644 index acc34d75c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups.ma +++ /dev/null @@ -1,69 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/suptermstar_6.ma". -include "basic_2/relocation/fsupq.ma". - -(* STAR-ITERATED SUPCLOSURE *************************************************) - -definition fsups: tri_relation genv lenv term ≝ tri_TC … fsupq. - -interpretation "star-iterated structural successor (closure)" - 'SupTermStar G1 L1 T1 G2 L2 T2 = (fsups G1 L1 T1 G2 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma fsups_ind: ∀G1,L1,T1. ∀R:relation3 …. R G1 L1 T1 → - (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G2 L2 T2. -#G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H -@(tri_TC_star_ind … IH1 IH2 G2 L2 T2 H) // -qed-. - -lemma fsups_ind_dx: ∀G2,L2,T2. ∀R:relation3 …. R G2 L2 T2 → - (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → - ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → R G1 L1 T1. -#G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H -@(tri_TC_star_ind_dx … IH1 IH2 G1 L1 T1 H) // -qed-. - -(* Basic properties *********************************************************) - -lemma fsups_refl: tri_reflexive … fsups. -/2 width=1 by tri_inj/ qed. - -lemma fsupq_fsups: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. -/2 width=1 by tri_inj/ qed. - -lemma fsups_strap1: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. -/2 width=5 by tri_step/ qed. - -lemma fsups_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. -/2 width=5 by tri_TC_strap/ qed. - -lemma fsups_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ → - ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 → - ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄. -#G1 #G2 #K1 #K2 #T1 #T2 #H @(fsups_ind … H) -G2 -K2 -T2 -/3 width=5 by fsups_strap1, fsupq_fsups, fsupq_drop/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma fsups_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ♯{G2, L2, T2} ≤ ♯{G1, L1, T1}. -#G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … H) -L2 -T2 -/3 width=3 by fsupq_fwd_fw, transitive_le/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma deleted file mode 100644 index fdee74619..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fsups_fsups.ma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/substitution/fsups.ma". - -(* STAR-ITERATED SUPCLOSURE *************************************************) - -(* Main properties **********************************************************) - -theorem fsups_trans: tri_transitive … fsups. -/2 width=5 by tri_TC_transitive/ qed-. 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 c5f04455d..c43385009 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 @@ -203,8 +203,8 @@ table { } ] [ { "iterated structural successor for closures" * } { - [ "fsups ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fsups_fsups" * ] - [ "fsupp ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fsupp_fsupp" * ] + [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_fqus" * ] + [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ] } ] [ { "generic local env. slicing" * } { @@ -225,7 +225,7 @@ table { class "orange" [ { "relocation" * } { [ { "structural successor for closures" * } { - [ "fsup ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fsupq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fsupq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ] + [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ] } ] [ { "global env. slicing" * } {