From 06d5ff2316426acfb16a9cc9784d40ce19351771 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 4 Oct 2013 15:02:46 +0000 Subject: [PATCH] lenv refinement for native validity removed from big tree reduction --- .../basic_2/{dynamic => computation}/ygt.ma | 24 +++++++++---------- .../{dynamic => computation}/ygt_lift.ma | 2 +- .../{dynamic => computation}/ygt_ygt.ma | 2 +- .../basic_2/{dynamic => computation}/yprs.ma | 23 +++++++++--------- .../{dynamic => computation}/yprs_lift.ma | 2 +- .../{dynamic => computation}/yprs_yprs.ma | 4 ++-- .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 5 ++-- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 2 +- .../basic_2/dynamic/snv_lsstas_lpr.ma | 2 +- .../basic_2/{dynamic => reduction}/ypr.ma | 5 ++-- .../basic_2/{dynamic => reduction}/ysc.ma | 14 +++++------ .../lambdadelta/basic_2/web/basic_2_src.tbl | 18 +++++++------- 12 files changed, 51 insertions(+), 52 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic => computation}/ygt.ma (87%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic => computation}/ygt_lift.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic => computation}/ygt_ygt.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic => computation}/yprs.ma (90%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic => computation}/yprs_lift.ma (97%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic => computation}/yprs_yprs.ma (95%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic => reduction}/ypr.ma (93%) rename matita/matita/contribs/lambdadelta/basic_2/{dynamic => reduction}/ysc.ma (84%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma index 43cc6d055..03678e4a8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma @@ -13,8 +13,8 @@ (**************************************************************************) include "basic_2/notation/relations/btpredstarproper_8.ma". -include "basic_2/dynamic/ysc.ma". -include "basic_2/dynamic/yprs.ma". +include "basic_2/reduction/ysc.ma". +include "basic_2/computation/yprs.ma". (* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************) @@ -39,35 +39,37 @@ qed-. lemma ysc_ygt: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -/3 width=5/ qed. +/3 width=5 by ygt_inj, ygt_step/ qed. lemma ygt_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 lapply (ygt_fwd_yprs … H1) #H0 -elim (ypr_inv_ysc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] /2 width=5/ +elim (ypr_inv_ysc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] +/2 width=5 by ygt_inj, ygt_step/ qed-. lemma ygt_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -G2 -L2 -T2 -[ /3 width=5 by ygt_inj, yprs_strap2/ | /2 width=3/ ] +/3 width=5 by ygt_step, ygt_inj, yprs_strap2/ qed-. lemma ygt_yprs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -G2 -L2 -T2 // +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -G2 -L2 -T2 /2 width=5 by ygt_strap1/ qed-. lemma yprs_ygt_trans: ∀h,g,G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ∀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 #HT1 @(yprs_ind … HT1) -G -L -T // +#h #g #G1 #G #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -G -L -T /3 width=5 by ygt_strap2/ qed-. lemma fsupp_ygt: ∀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 /3 width=1/ /3 width=5/ +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 +/3 width=5 by fsupp_yprs, ysc_fsup, ysc_ygt, ygt_inj/ qed. lemma cprs_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → @@ -78,11 +80,7 @@ lemma cprs_ygt: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥ elim (term_eq_dec T1 T) #H destruct [ -IHT1 /4 width=1/ | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1 - @(ygt_strap1 … HT1) -HT1 /2 width=1/ + @(ygt_strap1 … HT1) -HT1 /2 width=1 by ypr_cpr/ ] ] qed. - -lemma lsubsv_ygt: ∀h,g,G,L1,L2,T. G ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → - ⦃G, L1, T⦄ >[h, g] ⦃G, L2, T⦄. -/4 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma similarity index 98% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma index 19c15be07..6b713bc91 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lift.ma". -include "basic_2/dynamic/ygt.ma". +include "basic_2/computation/ygt.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma index 443dbcbf0..5910f81ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/dynamic/ygt.ma". +include "basic_2/computation/ygt.ma". (* "BIG TREE" ORDER FOR CLOSURES ********************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma index c94852540..d3260bc65 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma @@ -14,8 +14,9 @@ include "basic_2/notation/relations/btpredstar_8.ma". include "basic_2/substitution/fsupp.ma". +include "basic_2/reduction/ypr.ma". +include "basic_2/computation/cprs.ma". include "basic_2/computation/lprs.ma". -include "basic_2/dynamic/ypr.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) @@ -40,37 +41,37 @@ lemma yprs_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 genv lenv term. R G2 L2 T2 (* Basic properties *********************************************************) lemma yprs_refl: ∀h,g. tri_reflexive … (yprs h g). -/2 width=1/ qed. +/2 width=1 by tri_inj/ qed. lemma ypr_yprs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -/2 width=1/ qed. +/2 width=1 by tri_inj/ qed. lemma yprs_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -/2 width=5/ qed-. +/2 width=5 by tri_step/ qed-. lemma yprs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -/2 width=5/ qed-. +/2 width=5 by tri_TC_strap/ qed-. (* Note: this is a general property of bi_TC *) lemma fsupp_yprs: ∀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 /3 width=1/ /3 width=5/ +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2 +/3 width=5 by ypr_fsup, tri_step, ypr_yprs/ qed. lemma cprs_yprs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. -#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=5 by ypr_cpr, yprs_strap1/ +#h #g #G #L #T1 #T2 #H @(cprs_ind … H) -T2 +/3 width=5 by ypr_cpr, yprs_strap1/ qed. lemma lprs_yprs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. -#h #g #G #L1 #L2 #T #H @(lprs_ind … H) -L2 // /3 width=5 by ypr_lpr, yprs_strap1/ +#h #g #G #L1 #L2 #T #H @(lprs_ind … H) -L2 +/3 width=5 by ypr_lpr, yprs_strap1/ qed. -lemma lsubsv_yprs: ∀h,g,G,L1,L2,T. G ⊢ L2 ¡⊑[h, g] L1 → ⦃G, L1, T⦄ ≥[h, g] ⦃G, L2, T⦄. -/3 width=1/ qed. - lemma cpr_lpr_yprs: ∀h,g,G,L1,L2,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, T2⦄. /4 width=5 by yprs_strap1, ypr_lpr, ypr_cpr/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_lift.ma similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/yprs_lift.ma index 60bf07b48..2743f9c68 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_lift.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lift.ma". -include "basic_2/dynamic/yprs.ma". +include "basic_2/computation/yprs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma similarity index 95% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma index d2e994216..f28153053 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma @@ -12,14 +12,14 @@ (* *) (**************************************************************************) -include "basic_2/dynamic/yprs.ma". +include "basic_2/computation/yprs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) (* Main properties **********************************************************) theorem yprs_trans: ∀h,g. tri_transitive … (yprs h g). -/2 width=5/ qed-. +/2 width=5 by tri_TC_transitive/ qed-. (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma index a49ab5419..28aa4a7a0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -13,9 +13,10 @@ (**************************************************************************) include "basic_2/unfold/lsstas_lsstas.ma". +include "basic_2/computation/yprs_lift.ma". +include "basic_2/computation/ygt.ma". include "basic_2/equivalence/cpes_cpds.ma". -include "basic_2/dynamic/yprs_lift.ma". -include "basic_2/dynamic/ygt.ma". +include "basic_2/dynamic/snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) 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 e35537937..a69b20043 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma @@ -12,10 +12,10 @@ (* *) (**************************************************************************) +include "basic_2/computation/yprs_yprs.ma". include "basic_2/dynamic/snv_lift.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_snv.ma". -include "basic_2/dynamic/yprs_yprs.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma index d19c92bbf..a9dd6ebd2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma @@ -13,10 +13,10 @@ (**************************************************************************) include "basic_2/computation/cpds_cpds.ma". +include "basic_2/computation/yprs_yprs.ma". include "basic_2/dynamic/snv_aaa.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_lsstas.ma". -include "basic_2/dynamic/yprs_yprs.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/ypr.ma similarity index 93% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/ypr.ma index c08c984f2..308f30095 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/ypr.ma @@ -14,8 +14,8 @@ include "basic_2/notation/relations/btpred_8.ma". include "basic_2/relocation/fsup.ma". +include "basic_2/static/ssta.ma". include "basic_2/reduction/lpr.ma". -include "basic_2/dynamic/lsubsv.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) @@ -24,7 +24,6 @@ inductive ypr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ | ypr_lpr : ∀L2. ⦃G1, L1⦄ ⊢ ➡ L2 → ypr h g G1 L1 T1 G1 L2 T1 | ypr_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → ypr h g G1 L1 T1 G1 L1 T2 | ypr_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G1, L1⦄ ⊢ T1 •[h, g] T2 → ypr h g G1 L1 T1 G1 L1 T2 -| ypr_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → ypr h g G1 L1 T1 G1 L2 T1 . interpretation @@ -34,4 +33,4 @@ interpretation (* Basic properties *********************************************************) lemma ypr_refl: ∀h,g. tri_reflexive … (ypr h g). -/2 width=1/ qed. +/2 width=1 by ypr_cpr/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma similarity index 84% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma rename to matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma index a531dad1c..290157d30 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/ysc.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredproper_8.ma". -include "basic_2/dynamic/ypr.ma". +include "basic_2/reduction/ypr.ma". (* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) @@ -21,7 +21,6 @@ inductive ysc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ | ysc_fsup : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → ysc h g G1 L1 T1 G2 L2 T2 | ysc_cpr : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g G1 L1 T1 G1 L1 T2 | ysc_ssta : ∀T2,l. ⦃G1, L1⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G1, L1⦄ ⊢ T1 •[h, g] T2 → ysc h g G1 L1 T1 G1 L1 T2 -| ysc_lsubsv: ∀L2. G1 ⊢ L2 ¡⊑[h, g] L1 → (L1 = L2 → ⊥) → ysc h g G1 L1 T1 G1 L2 T1 . interpretation @@ -32,7 +31,8 @@ interpretation lemma ysc_ypr: ∀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 * -G2 -L2 -T2 /2 width=1/ /2 width=2/ +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/2 width=2 by ypr_fsup, ypr_cpr, ypr_ssta/ qed. (* Inversion lemmas on "big tree" parallel reduction for closures ***********) @@ -40,8 +40,8 @@ qed. lemma ypr_inv_ysc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨ ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡ L2 & T1 = T2. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /3 width=1/ /3 width=2/ -[ #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/ -| #L2 #HL21 elim (lenv_eq_dec L1 L2) #H destruct /3 width=1/ /4 width=1/ -] +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/3 width=2 by and3_intro, or_introl, or_intror, ysc_fsup, ysc_ssta/ +#T2 #HT12 elim (term_eq_dec T1 T2) #H destruct +/4 width=1 by and3_intro, or_introl, or_intror, ysc_cpr/ 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 3b79088f2..571d2e6de 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 @@ -39,15 +39,6 @@ table { } ] *) - [ { "\"big tree\" parallel computation" * } { - [ "ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "ygt_lift" + "ygt_ygt" * ] - [ "yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "yprs_lift" + "yprs_yprs" * ] - } - ] - [ { "\"big tree\" parallel reduction" * } { - [ "ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ] - } - ] [ { "local env. ref. for stratified native validity" * } { [ "lsubsv ( ? ⊢ ? ¡⊑[?,?] ? )" "lsubsv_ldrop" + "lsubsv_lsubd" + "lsubsv_lsuba" + "lsubsv_lsstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ] } @@ -93,6 +84,11 @@ table { [ "csn ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csn_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csn_lift" + "csn_lpx" * ] } ] + [ { "\"big tree\" parallel computation" * } { + [ "ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "ygt_lift" + "ygt_ygt" * ] + [ "yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "yprs_lift" + "yprs_yprs" * ] + } + ] [ { "decomposed extended computation" * } { [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ] } @@ -119,6 +115,10 @@ table { ] class "water" [ { "reduction" * } { + [ { "\"big tree\" parallel reduction" * } { + [ "ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ] + } + ] [ { "context-sensitive extended normal forms" * } { [ "cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] } -- 2.39.2