From f6a6221dcb90a12b04378ca2de86192e0e39f9ab Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 14 Dec 2013 22:18:47 +0000 Subject: [PATCH] - "big tree" theorem is now proved up to some conjectures involving just computation - redefined "big tree" proper computation now replaces its restricted form and is transitive - improved definition of "big tree" proper reduction involves lazy extended computation for local enviroments --- .../basic_2/computation/cpxs_lleq.ma | 5 + .../basic_2/computation/csx_fpbs.ma | 16 ++- .../{fpbr_fpbr.ma => fpbc_fpbs.ma} | 25 ++-- .../basic_2/computation/fpbc_fpns.ma | 40 ------- .../lambdadelta/basic_2/computation/fpbg.ma | 58 ++++++--- .../basic_2/computation/fpbg_fpbg.ma | 61 +++++----- .../basic_2/computation/fpbg_fpns.ma | 78 ++++++++++++ .../basic_2/computation/fpbg_lift.ma | 10 +- .../lambdadelta/basic_2/computation/fpbr.ma | 74 ------------ .../lambdadelta/basic_2/computation/fpbs.ma | 36 ++++++ .../basic_2/computation/fpbs_fpns.ma | 25 ++++ .../basic_2/computation/{fpbc.ma => fpbu.ma} | 24 ++-- .../basic_2/computation/fpbu_fpns.ma | 76 ++++++++++++ .../{fpbc_lift.ma => fpbu_lift.ma} | 12 +- .../lambdadelta/basic_2/computation/fsb.ma | 4 +- .../basic_2/computation/fsb_aaa.ma | 40 +++++++ .../basic_2/computation/fsb_alt.ma | 53 +++++++-- .../basic_2/computation/fsb_csx.ma | 49 ++++++-- .../basic_2/computation/fsb_fleq.ma | 51 -------- .../basic_2/computation/lsx_fpbc.ma | 111 ------------------ .../lambdadelta/basic_2/dynamic/snv.ma | 10 +- .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 76 ++++++------ .../lambdadelta/basic_2/dynamic/snv_da_lpr.ma | 32 ++--- .../lambdadelta/basic_2/dynamic/snv_lpr.ma | 72 ++++++------ .../lambdadelta/basic_2/dynamic/snv_lsstas.ma | 18 +-- .../basic_2/dynamic/snv_lsstas_lpr.ma | 54 ++++----- .../fpbg/btpredstarproper_8.etc} | 0 .../lambdadelta/basic_2/etc/fpbg/fpbg.etc | 40 +++++++ .../basic_2/etc/fpbg/fpbg_fpbg.etc | 57 +++++++++ .../basic_2/etc/fpbg/fpbg_fpns.etc | 34 ++++++ .../basic_2/etc/fpbg/fpbg_lift.etc | 28 +++++ .../contribs/lambdadelta/basic_2/names.txt | 3 +- ...rrestricted_8.ma => lazybtpredproper_8.ma} | 4 +- .../relations/lazybtpredstarproper_8.ma | 19 +++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 14 +-- 35 files changed, 780 insertions(+), 529 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/computation/{fpbr_fpbr.ma => fpbc_fpbs.ma} (56%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpns.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpns.ma rename matita/matita/contribs/lambdadelta/basic_2/computation/{fpbc.ma => fpbu.ma} (66%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma rename matita/matita/contribs/lambdadelta/basic_2/computation/{fpbc_lift.ma => fpbu_lift.ma} (82%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/fsb_fleq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.ma rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/btpredstarproper_8.ma => etc/fpbg/btpredstarproper_8.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{btpredstarrestricted_8.ma => lazybtpredproper_8.ma} (90%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma index be7ba8161..f8790c5d9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma @@ -24,3 +24,8 @@ lemma lleq_cpxs_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → #h #g #G #L2 #T1 #T2 #H @(cpxs_ind_dx … H) -T1 /4 width=6 by lleq_cpx_conf_dx, lleq_cpx_trans, cpxs_strap2/ qed-. + +lemma lleq_cpxs_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → + ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2. +#h #g #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by lleq_cpx_conf_dx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma index 99f39de1d..7d8882793 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma @@ -12,14 +12,26 @@ (* *) (**************************************************************************) -include "basic_2/computation/lpxs.ma". +include "basic_2/computation/fpbs.ma". include "basic_2/computation/csx_lpx.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) (* Advanced properties ******************************************************) +lemma csx_fpb_conf: ∀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. +#h #g #G1 #L1 #T1 #HT1 #G2 #L2 #T2 * +/2 width=5 by csx_cpx_trans, csx_fquq_conf, csx_lpx_conf/ +qed-. + +lemma csx_fpbs_conf: ∀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. +#h #g #G1 #L1 #T1 #HT1 #G2 #L2 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 +/2 width=5 by csx_fpb_conf/ +qed-. + lemma csx_lpxs_conf: ∀h,g,G,L1. ∀T:term. ⦃G, L1⦄ ⊢ ⬊*[h, g] T → ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L1 #T #HT #L2 #H @(lpxs_ind … H) -L2 /2 width=3 by csx_lpx_conf/ +/3 width=5 by csx_fpbs_conf, lpxs_fpbs/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma similarity index 56% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma index 24d0634b5..28efb6e6b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpbs.ma @@ -12,25 +12,16 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbg_fpbg.ma". -include "basic_2/computation/fpbr.ma". +include "basic_2/computation/fpbs_fpns.ma". +include "basic_2/computation/fpbs_fpbs.ma". +include "basic_2/computation/fpbc.ma". -(* RESTRICTED "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***********) +(* SINGLE-STEP "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********) -(* Advanced forward lemmas **************************************************) +(* Forward lemmas on "big tree" parallel computation for closures ***********) -lemma fpbr_fwd_fpbg: ∀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 #H elim (fpbr_inv_fqu_fpbs … H) -H -/2 width=5 by fqu_fpbs_fpbg/ -qed-. - -lemma fpbr_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → +lemma fpbc_fwd_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⦄. -/3 width=5 by fpbr_fwd_fpbg, fpbg_fwd_fpbs/ +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * +/3 width=5 by fpbu_fwd_fpbs, fpbs_trans, fpns_fpbs/ qed-. - -(* Main properties **********************************************************) - -theorem fpbr_trans: ∀h,g. tri_transitive … (fpbr h g). -/3 width=5 by fpbr_fwd_fpbs, fpbr_fpbs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma deleted file mode 100644 index 672d2d6e4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_fpns.ma +++ /dev/null @@ -1,40 +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/relocation/lleq_lleq.ma". -include "basic_2/computation/fpns.ma". -include "basic_2/computation/fpbs_alt.ma". -include "basic_2/computation/fpbc.ma". - -(* ATOMIC "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************) - -(* Forward lemmas on parallel computation for "big tree" normal forms *******) - -lemma fpbs_fwd_fpbc_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨ - ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_fpbsa … H) -H -#L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct -[ -HT1 elim (fqus_inv_gen … HT2) -HT2 - [ #HT2 @or_intror - /5 width=9 by fpbsa_inv_fpbs, fpbc_fqup, ex3_2_intro, ex2_3_intro, or_intror/ - | * #HG #HL #HT destruct elim (lleq_dec T2 L L2 0) #H - [ /3 width=1 by fpns_intro, or_introl/ - | /5 width=5 by fpbc_lpxs, ex2_3_intro, or_intror/ - ] - ] -| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H - /5 width=9 by fpbsa_inv_fpbs, fpbc_cpxs, cpx_cpxs, ex3_2_intro, ex2_3_intro, or_intror/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index a96b0bbbd..b5c336e24 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -12,29 +12,51 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/btpredstarproper_8.ma". +include "basic_2/notation/relations/lazybtpredstarproper_8.ma". include "basic_2/computation/fpbc.ma". (* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) -(* Note: this is not transitive *) -inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbg_cpxs: ∀L2,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → - fpbg h g G1 L1 T1 G1 L2 T2 -| fpbg_fqup: ∀G2,L,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃+ ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L2 → - fpbg h g G1 L1 T1 G2 L2 T2 -| fpbg_lpxs: ∀G2,L,L0,L2,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T⦄ ⊃* ⦃G2, L, T2⦄ → ⦃G2, L⦄ ⊢ ➡*[h, g] L0 → - (L ⋕[0, T2] L0 → ⊥) → ⦃G2, L0⦄ ⊢ ➡*[h, g] L2 → L0 ⋕[0, T2] L2 → - fpbg h g G1 L1 T1 G2 L2 T2 -. +definition fpbg: ∀h. sd h → tri_relation genv lenv term ≝ + λh,g. tri_TC … (fpbc h g). -interpretation "'big tree' proper parallel computation (closure)" - 'BTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2). +interpretation "general 'big tree' proper parallel computation (closure)" + 'LazyBTPRedStarProper h g G1 L1 T1 G2 L2 T2 = (fpbg h g G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma fpbc_fpbg: ∀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 -/3 width=9 by fpbg_fqup, fpbg_cpxs, fpbg_lpxs/ -qed. +lemma fpbc_fpbg: ∀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 by tri_inj/ qed. + +lemma fpbg_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 by tri_step/ qed. + +lemma fpbg_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 by tri_TC_strap/ qed. + +(* Note: this is used in the closure proof *) +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⦄. +/4 width=1 by fpbc_fpbg, fpbu_fpbc, fpbu_fqup/ qed. + +(* Basic eliminators ********************************************************) + +lemma fpbg_ind: ∀h,g,G1,L1,T1. ∀R:relation3 …. + (∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2) → + (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → R G L T → R G2 L2 T2) → + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. +#h #g #G1 #L1 #T1 #R #IH1 #IH2 #G2 #L2 #T2 #H +@(tri_TC_ind … IH1 IH2 G2 L2 T2 H) +qed-. + +lemma fpbg_ind_dx: ∀h,g,G2,L2,T2. ∀R:relation3 …. + (∀G1,L1,T1. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1) → + (∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G L T → R G1 L1 T1) → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → R G1 L1 T1. +#h #g #G2 #L2 #T2 #R #IH1 #IH2 #G1 #L1 #T1 #H +@(tri_TC_ind_dx … IH1 IH2 G1 L1 T1 H) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma index 97846fda4..2cb1f197e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma @@ -12,46 +12,41 @@ (* *) (**************************************************************************) -include "basic_2/computation/lpxs_lpxs.ma". -include "basic_2/computation/fpbs_alt.ma". -include "basic_2/computation/fpbg.ma". +include "basic_2/computation/fpbc_fpbs.ma". +include "basic_2/computation/fpbg_fpns.ma". (* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) -(* Advanced forward lemmas **************************************************) - -lemma fpbg_fwd_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 #H elim H -G2 -L2 -T2 -/3 width=5 by cpxs_fqus_lpxs_fpbs, cpxs_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/ -qed-. +(* Advanced inversion lemmas ************************************************) -lemma fpbg_fwd_fpbc_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → +lemma fpbg_inv_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 -[ /4 width=5 by fpbc_cpxs, lpxs_fpbs, ex2_3_intro/ -| #G2 #L #L2 #T #T2 #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct - [ -HT1 /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/ - | /5 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, fqup_fqus, ex3_2_intro, ex2_3_intro/ - ] -| #G2 #L #L0 #L2 #T #T2 #HT1 #HT2 #HL0 #H0 #HL02 #H02 - lapply (lpxs_trans … HL0 … HL02) #HL2 - elim (eq_term_dec T1 T) #H destruct - [ -HT1 elim (fqus_inv_gen … HT2) -HT2 - [ /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/ - | * #H1 #H2 #H3 destruct - /4 width=5 by fpbc_lpxs, lpxs_fpbs, ex2_3_intro/ - ] - | /4 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, ex3_2_intro, ex2_3_intro/ - ] +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbg_ind_dx … H) -G1 -L1 -T1 +[ #G1 #L1 #T1 * /3 width=5 by fpns_fpbs, ex2_3_intro/ +| #G1 #G #L1 #L #T1 #T * + #G0 #L0 #T0 #H10 #H0 #_ * + /5 width=9 by fpbu_fwd_fpbs, fpbs_trans, fpns_fpbs, ex2_3_intro/ ] qed-. +(* Advanced forward lemmas **************************************************) + +lemma fpbg_fwd_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 #H @(fpbg_ind … H) -G2 -L2 -T2 +[2: #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 @(fpbs_trans … IH1) -IH1 ] (**) (* full auto fails *) +/2 width=1 by fpbc_fwd_fpbs/ +qed-. + (* Advanced properties ******************************************************) -lemma fqu_fpbs_fpbg: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃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 #H elim(fpbs_fpbsa … H) -H -#L0 #T0 #HT0 #HT02 #HL02 elim (fqu_cpxs_trans … HT0 … H1) -T -/3 width=7 by fpbg_fqup, fqus_strap2_fqu/ -qed. +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⦄. +/5 width=5 by fpbg_inv_fpbu_sn, fpbs_fpbg_trans, fpbc_fpbg, fpbu_fpbc/ qed-. + +(* Man properties ***********************************************************) + +theorem fpbg_trans: ∀h,g. tri_transitive … (fpbg h g). +/2 width=5 by tri_TC_transitive/ qed-. + diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpns.ma new file mode 100644 index 000000000..bf1e62fde --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpns.ma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/fpbc_fpns.ma". +include "basic_2/computation/fpbg.ma". + +(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) + +(* Properties on parallel computation for "big tree" normal forms ***********) + +lemma fpbg_fpns_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 #H @(fpbg_ind … H) -G -L -T +[ /3 width=5 by fpbc_fpbg, fpbc_fpns_trans/ +| /4 width=9 by fpbg_strap1, fpbc_fpns_trans/ +] +qed-. + +lemma fpns_fpbg_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. +#h #g #G #G2 #L #L2 #T #T2 #H @(fpbg_ind_dx … H) -G -L -T +[ /3 width=5 by fpbc_fpbg, fpns_fpbc_trans/ +| /4 width=9 by fpbg_strap2, fpns_fpbc_trans/ +] +qed-. + +lemma fpbs_fpbg: ∀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, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind … H) -G2 -L2 -T2 +[ /2 width=1 by or_introl/ +| #G #G2 #L #L2 #T #T2 #_ #H2 * #H1 elim (fpb_fpbu … H2) -H2 #H2 + [ /3 width=5 by fpns_trans, or_introl/ + | /5 width=5 by fpbc_fpbg, fpns_fpbc_trans, fpbu_fpbc, or_intror/ + | /3 width=5 by fpbg_fpns_trans, or_intror/ + | /4 width=5 by fpbg_strap1, fpbu_fpbc, or_intror/ + ] +] +qed-. + +(* Advanced properties ******************************************************) + +lemma fpbg_fpb_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 #H1 #H2 elim (fpb_fpbu … H2) -H2 +/3 width=5 by fpbg_fpns_trans, fpbg_strap1, fpbu_fpbc/ +qed-. + + +lemma fpb_fpbg_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 #H1 elim (fpb_fpbu … H1) -H1 +/3 width=5 by fpns_fpbg_trans, fpbg_strap2, fpbu_fpbc/ +qed-. + +lemma fpbs_fpbg_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 #H @(fpbs_ind … H) -G -L -T /3 width=5 by fpb_fpbg_trans/ +qed-. + +(* Note: this is used in the closure proof *) +lemma fpbg_fpbs_trans: ∀h,g,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ∀G1,L1,T1. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄. +#h #g #G #G2 #L #L2 #T #T2 #H @(fpbs_ind_dx … H) -G -L -T /3 width=5 by fpbg_fpb_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma index 26dec0777..4dd9afb73 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/computation/fpbc_lift.ma". +include "basic_2/computation/fpbu_lift.ma". include "basic_2/computation/fpbg.ma". (* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************) @@ -20,9 +20,9 @@ include "basic_2/computation/fpbg.ma". (* Advanced properties ******************************************************) lemma lsstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. -/4 width=5 by fpbc_fpbg, lsstas_fpbc/ qed. + ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >⋕[h, g] ⦃G, L, T2⦄. +/5 width=5 by fpbc_fpbg, fpbu_fpbc, lsstas_fpbu/ qed. lemma ssta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → - ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. -/3 width=2 by fpbc_fpbg, ssta_fpbc/ qed. + ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >⋕[h, g] ⦃G, L, T2⦄. +/4 width=2 by fpbc_fpbg, fpbu_fpbc, ssta_fpbu/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma deleted file mode 100644 index 04f0e2309..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma +++ /dev/null @@ -1,74 +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/btpredstarrestricted_8.ma". -include "basic_2/computation/fpbs.ma". - -(* RESTRICTED "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***********) - -inductive fpbr (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbr_inj : ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpbr h g G1 L1 T1 G2 L2 T2 -| fpbr_step: ∀G,G2,L,L2,T,T2. fpbr h g G1 L1 T1 G L T → ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - fpbr h g G1 L1 T1 G2 L2 T2 -. - -interpretation "restricted 'big tree' proper parallel computation (closure)" - 'BTPRedStarRestricted h g G1 L1 T1 G2 L2 T2 = (fpbr h g G1 L1 T1 G2 L2 T2). - -(* Basic inversion lemmas ***************************************************) - -lemma fpbr_inv_fqu_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → - ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 [ /2 width=5 by ex2_3_intro/ ] (**) (* auto fails without brackets *) -#G #G2 #L #L2 #T #T2 #_ #HT2 * /3 width=9 by fpbs_strap1, ex2_3_intro/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma fpbr_fwd_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 #H elim H -G2 -L2 -T2 -/3 width=5 by fpbs_strap1, fqup_fpbs, fqu_fqup/ -qed-. - -(* Basic properties *********************************************************) - -lemma fqu_fpbs_fpbr: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃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 #H @(fpbs_ind … H) -G2 -L2 -T2 -/2 width=5 by fpbr_inj, fpbr_step/ -qed. - -lemma fpbr_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ → - ⦃G, L, T⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃≥[h, g] ⦃G2, L2, T2⦄. -/3 width=5 by fqu_fpbs_fpbr, fpbr_fwd_fpbs/ qed-. - -(* Note: this is used in the closure proof *) -lemma fpbr_fpbs_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 @(fpbs_ind … HT2) -G2 -L2 -T2 -/2 width=5 by fpbr_step/ -qed-. - -lemma fqup_fpbr_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃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 @(fqup_ind … HT1) -G -L -T -/3 width=5 by fpbr_strap2/ -qed-. - -(* Note: this is used in the closure proof *) -lemma fqup_fpbr: ∀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 elim (fqup_inv_step_sn … H) -H -/3 width=5 by fqu_fpbs_fpbr, fqus_fpbs/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index 0f63844e2..29eee60e4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -86,3 +86,39 @@ lemma lprs_fpbs: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → ⦃G, L1, T⦄ lemma cpr_lpr_fpbs: ∀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 fpbs_strap1, lpr_fpb, cpr_fpb/ qed. + +lemma fpbs_fqus_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → + ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind … H) -G2 -L2 -T2 +/3 width=5 by fpbs_strap1, fpb_fquq/ +qed-. + +lemma fpbs_cpxs_trans: ∀h,g,G1,G,L1,L,T1,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → + ⦃G, L⦄ ⊢ T ➡*[h, g] T2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T2⦄. +#h #g #G1 #G #L1 #L #T1 #T #T2 #H1 #H @(cpxs_ind … H) -T2 +/3 width=5 by fpbs_strap1, fpb_cpx/ +qed-. + +lemma fpbs_lpxs_trans: ∀h,g,G1,G,L1,L,L2,T1,T. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → + ⦃G, L⦄ ⊢ ➡*[h, g] L2 → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L2, T⦄. +#h #g #G1 #G #L1 #L #L2 #T1 #T #H1 #H @(lpxs_ind … H) -L2 +/3 width=5 by fpbs_strap1, fpb_lpx/ +qed-. + +lemma fqus_fpbs_trans: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊃* ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fqus_ind_dx … H) -G1 -L1 -T1 +/3 width=5 by fpbs_strap2, fpb_fquq/ +qed-. + +lemma cpxs_fpbs_trans: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T #T2 #H1 #H @(cpxs_ind_dx … H) -T1 +/3 width=5 by fpbs_strap2, fpb_cpx/ +qed-. + +lemma lpxs_fpbs_trans: ∀h,g,G1,G2,L1,L,L2,T1,T2. ⦃G1, L, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ➡*[h, g] L → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L #L2 #T1 #T2 #H1 #H @(lpxs_ind_dx … H) -L1 +/3 width=5 by fpbs_strap2, fpb_lpx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpns.ma new file mode 100644 index 000000000..2006ef222 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpns.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/fpns.ma". +include "basic_2/computation/fpbs.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +(* Properties on parallel computation for "big tree" normal forms ***********) + +lemma fpns_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 * /2 width=1 by lpxs_fpbs/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma similarity index 66% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma index a66e1ac90..ab90b6f6f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma @@ -16,31 +16,31 @@ include "basic_2/notation/relations/btpredproper_8.ma". include "basic_2/relocation/lleq.ma". include "basic_2/computation/fpbs.ma". -(* ATOMIC "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************) +(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) -inductive fpbc (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbc_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbc h g G1 L1 T1 G2 L2 T2 -| fpbc_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbc h g G1 L1 T1 G1 L1 T2 -| fpbc_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T1] L2 → ⊥) → fpbc h g G1 L1 T1 G1 L2 T1 +inductive fpbu (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ +| fpbu_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2 +| fpbu_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2 +| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T1] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 . interpretation - "'big tree' proper parallel reduction (closure)" - 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbc h g G1 L1 T1 G2 L2 T2). + "unitary 'big tree' proper parallel reduction (closure)" + 'BTPRedProper h g G1 L1 T1 G2 L2 T2 = (fpbu h g G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) -lemma cprs_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → +lemma cprs_fpbu: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -/3 width=1 by fpbc_cpxs, cprs_cpxs/ qed. +/3 width=1 by fpbu_cpxs, cprs_cpxs/ qed. -lemma lprs_fpbc: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[0, T] L2 → ⊥) → +lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[0, T] L2 → ⊥) → ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. -/3 width=1 by fpbc_lpxs, lprs_lpxs/ qed. +/3 width=1 by fpbu_lpxs, lprs_lpxs/ qed. (* Basic forward lemmas *****************************************************) -lemma fpbc_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → +lemma fpbu_fwd_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 * -G2 -L2 -T2 /3 width=1 by lpxs_fpbs, cpxs_fpbs, fqup_fpbs/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma new file mode 100644 index 000000000..9f5111ad2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/cpxs_lleq.ma". +include "basic_2/computation/lpxs_lleq.ma". +include "basic_2/computation/lpxs_lpxs.ma". +include "basic_2/computation/fpns.ma". +include "basic_2/computation/fpbs_alt.ma". +include "basic_2/computation/fpbu.ma". + +(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) + +(* Properties on parallel computation for "big tree" normal forms ***********) + +lemma fpns_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⦄. +#h #g #F1 #F2 #K1 #K2 #T1 #T2 * -F2 -K2 -T2 +#K2 #HK12 #HT1 #G2 #L2 #U2 * -G2 -L2 -U2 +[ #G2 #L2 #U2 #H12 elim (lpxs_lleq_fqup_trans … H12 … HK12 HT1) -K2 + /3 width=5 by fpbu_fqup, fpns_intro, ex2_3_intro/ +| /4 width=9 by fpbu_cpxs, fpns_intro, lpxs_cpxs_trans, lleq_cpxs_conf_dx, ex2_3_intro/ +| /5 width=5 by fpbu_lpxs, lpxs_trans, lleq_canc_sn, ex2_3_intro/ +] +qed-. + +lemma fpb_fpbu: ∀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, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H + [ /4 width=1 by fpbu_fqup, fqu_fqup, or_intror/ + | * #H1 #H2 #H3 destruct /2 width=1 by or_introl/ + ] +| #T2 #HT12 elim (eq_term_dec T1 T2) + #HnT12 destruct /4 width=1 by fpbu_cpxs, cpx_cpxs, or_intror, or_introl/ +| #L2 #HL12 elim (lleq_dec … T1 L1 L2 0) + /4 width=3 by fpbu_lpxs, fpns_intro, lpx_lpxs, or_intror, or_introl/ +] +qed-. + +lemma fpbs_fpbu_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ ∨ + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +(* ALTERNATIVE PROOF +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 +[ /2 width=1 by or_introl/ +| #G1 #G #L1 #L #T1 #T #H1 #_ * [ #H2 | * #G0 #L0 #T0 #H0 #H02 ] + elim (fpb_fpbu … H1) -H1 #H1 + [ /3 width=1 by +*) +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim(fpbs_fpbsa … H) -H +#L #T #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct +[ -HT1 elim (fqus_inv_gen … HT2) -HT2 + [ #HT2 @or_intror + /5 width=9 by fpbsa_inv_fpbs, fpbu_fqup, ex3_2_intro, ex2_3_intro, or_intror/ + | * #HG #HL #HT destruct elim (lleq_dec T2 L L2 0) #H + [ /3 width=1 by fpns_intro, or_introl/ + | /5 width=5 by fpbu_lpxs, ex2_3_intro, or_intror/ + ] + ] +| elim (cpxs_neq_inv_step_sn … HT1 H) -HT1 -H + /5 width=9 by fpbsa_inv_fpbs, fpbu_cpxs, cpx_cpxs, ex3_2_intro, ex2_3_intro, or_intror/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma similarity index 82% rename from matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma index 6915c72cf..d7b48650e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbc_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lift.ma @@ -14,19 +14,19 @@ include "basic_2/static/ssta_ssta.ma". include "basic_2/computation/cpxs_lift.ma". -include "basic_2/computation/fpbc.ma". +include "basic_2/computation/fpbu.ma". -(* ATOMIC "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES ***************) +(* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) (* Advanced properties ******************************************************) -lemma lsstas_fpbc: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → +lemma lsstas_fpbu: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. -/4 width=5 by fpbc_cpxs, lsstas_cpxs/ qed. +/4 width=5 by fpbu_cpxs, lsstas_cpxs/ qed. -lemma ssta_fpbc: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → +lemma ssta_fpbu: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. #h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) -/3 width=5 by ssta_lsstas, lsstas_fpbc/ #H destruct +/3 width=5 by ssta_lsstas, lsstas_fpbu/ #H destruct elim (ssta_inv_refl_pos … HT1 … HT12) qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index 64090eec9..1616402de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btsn_5.ma". -include "basic_2/computation/fpbc.ma". +include "basic_2/computation/fpbu.ma". include "basic_2/computation/csx_alt.ma". (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) @@ -43,5 +43,5 @@ qed-. (* Basic inversion lemmas ***************************************************) lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. -#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro_cprs, fpbc_cpxs/ +#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro_cprs, fpbu_cpxs/ 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 new file mode 100644 index 000000000..095d1fb11 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_aaa.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/csx_aaa.ma". +include "basic_2/computation/fsb_csx.ma". + +(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) + +(* Main properties **********************************************************) + +(* Note: this is the "big tree" theorem ("small step" version) *) +theorem aaa_fsb: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥[h, g] T. +/3 width=2 by aaa_csx, csx_fsb/ qed. + +(* Note: this is the "big tree" theorem ("big step" version) *) +theorem aaa_fsba: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥⦥[h, g] T. +/3 width=2 by fsb_fsba, aaa_fsb/ qed. + +(* Advanced eliminators on atomica arity assignment for terms ***************) + +fact 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. ⦃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 +#G1 #L1 #T1 #H1 #IH1 #A1 #HTA1 @IH -IH // +#G2 #L2 #T2 #H12 @IH1 // \ No newline at end of file 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 39b97103d..992775d70 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btsnalt_5.ma". -include "basic_2/computation/fpbg.ma". +include "basic_2/computation/fpbg_fpbg.ma". include "basic_2/computation/fsb.ma". (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) @@ -21,7 +21,7 @@ include "basic_2/computation/fsb.ma". (* Note: alternative definition of fsb *) inductive fsba (h) (g): relation3 genv lenv term ≝ | fsba_intro: ∀G1,L1,T1. ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → fsba h g G2 L2 T2 + ∀G2,L2,T2. ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄ → fsba h g G2 L2 T2 ) → fsba h g G1 L1 T1. interpretation @@ -30,19 +30,54 @@ interpretation (* Basic eliminators ********************************************************) -theorem fsba_ind_alt: ∀h,g. ∀R: relation3 …. ( - ∀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 fsba_ind_alt: ∀h,g. ∀R: relation3 …. ( + ∀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. #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. +#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. +#h #g #G #L #T #H @(fsb_ind_alt … H) -G -L -T +#G1 #L1 #T1 #_ #IH @fsba_intro +#G2 #L2 #T2 #H elim (fpbg_inv_fpbu_sn … H) -H +/3 width=5 by fsba_fpbs_trans/ +qed. + (* Main inversion lemmas ****************************************************) theorem fsba_inv_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥⦥[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. #h #g #G #L #T #H @(fsba_ind_alt … H) -G -L -T -/4 width=1 by fsb_intro, fpbc_fpbg/ +/5 width=1 by fsb_intro, fpbc_fpbg, fpbu_fpbc/ +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. +/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 → + (∀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. +#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 6b1e14497..f25939dd3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -12,19 +12,52 @@ (* *) (**************************************************************************) -include "basic_2/computation/csx_aaa.ma". -include "basic_2/computation/fsb.ma". +include "basic_2/computation/lsx_csx.ma". +include "basic_2/computation/fsb_alt.ma". + +axiom lsx_fqup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + G1 ⊢ ⋕⬊*[h, g, T1] L1 → G2 ⊢ ⋕⬊*[h, g, T2] L2. + +axiom fqup_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → + ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) → + ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 & + K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) -(* Advanced propreties ******************************************************) +(* Advanced propreties on context-senstive extended bormalizing terms *******) lemma csx_fsb: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T → ⦃G, L⦄ ⊢ ⦥[h, g] T. -#h #g #G #L #T #H @(csx_ind_fpbc … H) -T /3 width=1 by fsb_intro/ +#h #g #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1 +#T1 #HT1 @(lsx_ind h g T1 G1 … L1) /2 width=1 by csx_lsx/ -L1 +#L1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1 +#G1 #L1 #T1 #IHu #H1 #IHl #IHc @fsb_intro +#G2 #L2 #T2 * -G2 -L2 -T2 +[ #G2 #L2 #T2 #H12 @IHu -IHu /2 width=5 by lsx_fqup_conf/ -H1 [| -IHl ] + [ #L0 #HL20 #HnL20 #_ elim (fqup_lpxs_trans_nlleq … H12 … HL20 HnL20) -L2 + /6 width=5 by fsb_fpbs_trans, lpxs_fpbs, fqup_fpbs, lpxs_cpxs_trans/ + | #T0 #HT20 #HnT20 elim (fqup_cpxs_trans_neq … H12 … HT20 HnT20) -T2 + /4 width=5 by fsb_fpbs_trans, fqup_fpbs/ + ] +| -H1 -IHu -IHl /3 width=1 by/ +| -H1 -IHu /5 width=5 by fsb_fpbs_trans, lpxs_fpbs, lpxs_cpxs_trans/ +] qed. -(* Main properties **********************************************************) +(* 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. +/4 width=4 by fsb_inv_csx, csx_fsb, fsb_ind_alt/ qed-. -(* Note: this is the "big tree" theorem ("small step" version) *) -theorem aaa_fsb: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⦥[h, g] T. -/3 width=2 by aaa_csx, csx_fsb/ qed. +lemma csx_ind_fpbg: ∀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_fpbg/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_fleq.ma deleted file mode 100644 index 72f4695ca..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_fleq.ma +++ /dev/null @@ -1,51 +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/computation/fpbs_fleq.ma". -include "basic_2/computation/fpbg_fpbg.ma". -include "basic_2/computation/fsb.ma". - -(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) - -axiom fleq_fpbc_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⦄. - -axiom fleq_fpbg_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⦄. - -(* Properties ******************************************************) - -lemma fsb_fleq_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. -#h #g #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 -/4 width=5 by fsb_intro, fleq_fpbc_trans/ -qed-. - -(* Advanced eliminators *****************************************************) - -lemma fsb_ind_fpbg_fpbs: ∀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 - ) → - ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⦥[h, g] T1 → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → R G2 L2 T2. -#h #g #R #IH #G1 #L1 #T1 #H @(fsb_ind_alt … H) -G1 -L1 -T1 -#G1 #L1 #T1 #H1 #IH1 #G2 #L2 #T2 #H12 elim (fpbs_fwd_fpb_sn … H12) -H12 -[ #H12 @IH -IH /2 width=5 by fsb_fleq_trans/ - -H1 #G0 #L0 #T0 #H20 lapply (fleq_fpbg_trans … H12 H20) -G2 -L2 -T2 - #H10 elim (fpbg_fwd_fpb_sn … H10) -H10 /2 width=5 by/ -| -H1 -IH * /2 width=5 by/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.ma deleted file mode 100644 index 2c6418f2a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_fpbc.ma +++ /dev/null @@ -1,111 +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/computation/lpxs_lpxs.ma". -include "basic_2/computation/fpbs.ma". -include "basic_2/computation/fpbc.ma". -include "basic_2/computation/csx_lift.ma". -include "basic_2/computation/csx_lpxs.ma". -include "basic_2/computation/lsx_csx.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -(* Advanced eliminators for context-sensitive ext. strongly norm. terms *****) - -lemma tollens: ∀R1,R2,R3:Prop. (R1 → R2) → (R2 → R3) → R1 → R3. -/3 width=1/ qed-. - -axiom fqus_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ → - ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) → - ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 & - K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄. - -axiom fpbs_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ≥[h, g] ⦃G2, K2, T2⦄ → - ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) → - ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 & - K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. - - -lemma csx_ind_fpbc_fpbs: ∀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 - ) → - ∀G1,L1,T1. ⦃G1, L1⦄ ⊢ ⬊*[h, g] T1 → - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄ → - R G2 L2 T2. -#h #g #R #IH1 #G1 #L1 #T1 #H @(csx_ind_alt … H) -T1 -#T1 #HT1 @(lsx_ind h g T1 G1 … L1) /2 width=1 by csx_lsx/ -L1 -#L1 @(fqup_wf_ind … G1 L1 T1) -G1 -L1 -T1 -#G1 #L1 #T1 #IH2 #H1 #IH3 #IH4 #G2 #L2 #T2 #H12 -@IH1 -IH1 (* /4 width=5 by lsx_inv_csx, csx_lpxs_conf, csx_fqus_conf/ *) -[2: #G #L #T * - [ - | - | #L0 #HL20 #HnT2 elim (fpbs_lpxs_trans_nlleq … H12 … HL20 HnT2) -L2 - #L2 #HL12 #HnT1 #H12 @(IH3 … HL12 HnT1 … H12) -IH3 - #H26 #H27 #H28 #H29 #H30 #H31 #H32 - @(IH4) … H27 H28) - - [ #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 - lapply (fqup_fqus_trans … H15 … H21) -H15 -H21 #H - @(IH3 … H23 H24) - - #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 - @(IH4 … H3 … H10) -IH4 -H10 -H3 // - - - - [ -IH4 | -H1 -IH2 -IH4 | -H1 -H2 -IH2 -IH3 ] -[ #G0 #L0 #T0 #H20 elim (lpxs_lleq_fqup_trans … H20 … HYL2 HT2) -L2 - #L2 #H20 #HL20 lapply (fqus_fqup_trans … H12 H20) -G2 -Y -T2 - #H10 @(IH2 … H10) -IH2 /2 width=5 by csx_fqup_conf/ -(* - #T2 #HT02 #H #G3 #L3 #T3 #HT23 elim (fqup_cpxs_trans_neq … H10 … HT02 H) -T0 - /4 width=8 by fqup_fqus_trans, fqup_fqus/ -*) -| (* #T0 #HT20 #H elim (fqus_cpxs_trans_neq … H12 … HT20 H) -T2 /3 width=4 by/ *) -| #L0 #HL20 #HnT2 @(IH4 L0) /3 width=3 by lpxs_trans, lleq_canc_sn/ - - - - - - | /3 width=3 by / - [ /2 width=3 - - lapply (lpxs_trans … HYL2 … HL20) - #HYL0 lapply (tollens ???? HnT2) [ @(lleq_canc_sn … HT2) | skip ] -L2 - #HnT2 elim (fqus_lpxs_trans_nlleq … H12 … HYL0 HnT2) - - - - lapply (lleq_canc_sn … L0 … HT2) - - - - | - -elim (lpxs_lleq_fqup_trans … H12 … HYL2 HT2) -L2 - - -] -qed-. - -lemma csx_ind_fpbc: ∀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=8 by csx_ind_fpbc_fqus/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma index 07bdd7cbf..a85645f07 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma @@ -79,13 +79,13 @@ fact snv_inv_bind_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀a,I,V,T. X qed-. lemma snv_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{a,I}V.T ¡[h, g] → - ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. + ⦃G, L⦄ ⊢ V ¡[h, g] ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ T ¡[h, g]. /2 width=4 by snv_inv_bind_aux/ qed-. fact snv_inv_appl_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀V,T. X = ⓐV.T → ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & - ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. + ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & + ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. #h #g #G #L #X * -L -X [ #G #L #k #V #T #H destruct | #I #G #L #K #V0 #i #_ #_ #V #T #H destruct @@ -97,8 +97,8 @@ qed-. lemma snv_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ¡[h, g] → ∃∃a,W,W0,U,l. ⦃G, L⦄ ⊢ V ¡[h, g] & ⦃G, L⦄ ⊢ T ¡[h, g] & - ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & - ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. + ⦃G, L⦄ ⊢ V ▪[h, g] l+1 & ⦃G, L⦄ ⊢ V •[h, g] W & ⦃G, L⦄ ⊢ W ➡* W0 & + ⦃G, L⦄ ⊢ T •*➡*[h, g] ⓛ{a}W0.U. /2 width=3 by snv_inv_appl_aux/ qed-. fact snv_inv_cast_aux: ∀h,g,G,L,X. ⦃G, L⦄ ⊢ X ¡[h, g] → ∀W,T. X = ⓝW.T → 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 f9bea7ca4..e62507f9b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -14,7 +14,7 @@ include "basic_2/unfold/lsstas_lsstas.ma". include "basic_2/computation/fpbs_lift.ma". -include "basic_2/computation/fpbr.ma". +include "basic_2/computation/fpbg_fpns.ma". include "basic_2/equivalence/cpes_cpds.ma". include "basic_2/dynamic/snv.ma". @@ -47,28 +47,28 @@ definition IH_snv_lsstas: ∀h:sh. sd h → relation3 genv lenv term ≝ (* Properties for the preservation results **********************************) fact snv_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ¡[h, g]. #h #g #G0 #L0 #T0 #IH #G #L1 #T1 #HLT0 #HT1 #T2 #H -@(cprs_ind … H) -T2 /4 width=6 by fpbr_fpbs_trans, cprs_fpbs/ +@(cprs_ind … H) -T2 /4 width=6 by fpbg_fpbs_trans, cprs_fpbs/ qed-. fact da_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ T2 ▪[h, g] l. #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L1 #T1 #HLT0 #HT1 #l #Hl #T2 #H -@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbr_fpbs_trans, cprs_fpbs/ +@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbg_fpbs_trans, cprs_fpbs/ qed-. fact da_cpcs_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → - ∀T2. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T2⦄ → ⦃G, L⦄ ⊢ T2 ¡[h, g] → ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀l2. ⦃G, L⦄ ⊢ T2 ▪[h, g] l2 → ⦃G, L⦄ ⊢ T1 ⬌* T2 → l1 = l2. #h #g #G0 #L0 #T0 #IH2 #IH1 #G #L #T1 #HLT01 #HT1 #T2 #HLT02 #HT2 #l1 #Hl1 #l2 #Hl2 #H @@ -76,8 +76,8 @@ elim (cpcs_inv_cprs … H) -H /4 width=18 by da_cprs_lpr_aux, da_mono/ qed-. fact ssta_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀l. ⦃G, L1⦄ ⊢ T1 ▪[h, g] l+1 → ∀U1. ⦃G, L1⦄ ⊢ T1 •[h, g] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → @@ -88,55 +88,55 @@ elim (IH … H01 … 1 … Hl U1 … HT12 … HL12) qed-. fact lsstas_cprs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[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, g, l2] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*[h, g, l2] U2 & ⦃G, L2⦄ ⊢ U1 ⬌* U2. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l1 #l2 #Hl21 #Hl1 #U1 #HTU1 #T2 #H -@(cprs_ind … H) -T2 [ /2 width=10/ ] +@(cprs_ind … H) -T2 [ /2 width=10 by/ ] #T #T2 #HT1T #HTT2 #IHT1 #L2 #HL12 elim (IHT1 L1) // -IHT1 #U #HTU #HU1 elim (IH1 … Hl21 … HTU … HTT2 … HL12) -IH1 -HTU -HTT2 [2: /3 width=12 by da_cprs_lpr_aux/ |3: /3 width=10 by snv_cprs_lpr_aux/ -|4: /3 width=5 by fpbr_fpbs_trans, cprs_fpbs/ +|4: /3 width=5 by fpbg_fpbs_trans, cprs_fpbs/ ] -G0 -L0 -T0 -T1 -T -l1 #U2 #HTU2 #HU2 /4 width=5 by lpr_cpcs_conf, cpcs_trans, ex2_intro/ qed-. fact lsstas_cpcs_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[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, g, l] U1 → - ∀T2. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → + ∀T2. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T2⦄ → ⦃G, L1⦄ ⊢ T2 ¡[h, g] → ∀l2. l ≤ l2 → ⦃G, L1⦄ ⊢ T2 ▪[h, g] l2 → ∀U2. ⦃G, L1⦄ ⊢ T2 •*[h, g, l] U2 → ⦃G, L1⦄ ⊢ T1 ⬌* T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L2⦄ ⊢ U1 ⬌* U2. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G #L1 #T1 #H01 #HT1 #l #l1 #Hl1 #HTl1 #U1 #HTU1 #T2 #H02 #HT2 #l2 #Hl2 #HTl2 #U2 #HTU2 #H #L2 #HL12 elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (lsstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1/ #W1 #H1 #HUW1 -elim (lsstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1/ #W2 #H2 #HUW2 -L0 -T0 +elim (lsstas_cprs_lpr_aux … H01 HT1 … Hl1 HTl1 … HTU1 … H1 … HL12) -T1 /2 width=1 by/ #W1 #H1 #HUW1 +elim (lsstas_cprs_lpr_aux … H02 HT2 … Hl2 HTl2 … HTU2 … H2 … HL12) -T2 /2 width=1 by/ #W2 #H2 #HUW2 -L0 -T0 lapply (lsstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_dx/ qed-. fact snv_ssta_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - ∀G,L,T. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + ∀G,L,T. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T⦄ → ⦃G, L⦄ ⊢ T ¡[h, g] → ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ∀U. ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L⦄ ⊢ U ¡[h, g]. /3 width=8 by lsstas_inv_SO, ssta_lsstas/ qed-. fact lsstas_cpds_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L, T1⦄ → ⦃G, L⦄ ⊢ T1 ¡[h, g] → ∀l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ∀U1. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] U1 → ∀T2. ⦃G, L⦄ ⊢ T1 •*➡*[h, g] T2 → ∃∃U2,l. l ≤ l2 & ⦃G, L⦄ ⊢ T2 •*[h, g, l] U2 & ⦃G, L⦄ ⊢ U1 •*⬌*[h, g] U2. @@ -149,15 +149,15 @@ elim (le_or_ge l2 l) #Hl2 | lapply (lsstas_da_conf … HT1T … Hl1) #Hl1l lapply (lsstas_conf_le … HT1T … HTU1) -HTU1 // #HTU1 elim (lsstas_cprs_lpr_aux … IH3 IH2 IH1 … Hl1l … HTU1 … HTT2 L) - /3 width=8 by fpbr_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12 + /3 width=8 by fpbg_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12 /3 width=5 by cpcs_cpes, ex3_2_intro/ ] qed-. fact cpds_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → - ∀G,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + ∀G,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G, L1, T1⦄ → ⦃G, L1⦄ ⊢ T1 ¡[h, g] → ∀U1. ⦃G, L1⦄ ⊢ T1 •*➡*[h, g] U1 → ∀T2. ⦃G, L1⦄ ⊢ T1 ➡ T2 → ∀L2. ⦃G, L1⦄ ⊢ ➡ L2 → ∃∃U2. ⦃G, L2⦄ ⊢ T2 •*➡*[h, g] U2 & ⦃G, L2⦄ ⊢ U1 ➡* U2. 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 a15ef134b..b44137664 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 @@ -22,9 +22,9 @@ include "basic_2/dynamic/snv_cpcs.ma". (* Properties on degree assignment for terms ********************************) fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_da_cpr_lpr h g G1 L1 T1. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #_ #_ #_ #_ #l #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1 @@ -39,14 +39,14 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0. 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, fqup_fpbr/ + /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 (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, fqup_fpbr/ + /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, fqup_fpbr, 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, fqup_fpbr, 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, fqup_fpbr/ + [ #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) ⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_cpr_lpr h g G1 L1 T1. #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #_ destruct -IH4 -IH3 -IH2 -IH1 -H1 @@ -36,29 +36,29 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct lapply (fqup_lref … G1 … HLK1) #HKL elim (cpr_inv_lref1 … H2) -H2 - [ #H destruct -HLK1 /4 width=10 by fqup_fpbr, snv_lref/ + [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/ | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12 lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbr, snv_lift/ + lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/ ] | #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) | #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 elim (snv_inv_bind … H1) -H1 #HV1 #HT1 elim (cpr_inv_bind1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbr, snv_bind, lpr_pair/ + [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/ | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 - /4 width=10 by fqup_fpbr, snv_inv_lift, lpr_pair, ldrop_ldrop/ + /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1 elim (cpr_inv_appl1 … H2) -H2 * [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 - lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #HV2 - lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbr/ #HT2 - lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbr/ #H2l0 - elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbr/ -HV1 #W2 #HVW2 #HW12 - elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbr/ -HT12 -HTU1 #X #HTU2 #H + lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 + lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2 + lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #H2l0 + elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) -Hl0 -HVW1 -HV12 /2 width=1 by fqup_fpbg/ -HV1 #W2 #HVW2 #HW12 + elim (cpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HT12 -HTU1 #X #HTU2 #H elim (cprs_inv_abst1 … H) -H #W20 #U2 #HW120 #_ #H destruct lapply (lpr_cprs_conf … HL12 … HW10) -L1 #HW10 lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120 @@ -70,38 +70,38 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 lapply (cprs_div … HW10 … HW230) -W30 #HW120 - lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbr/ #HW10 + lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbg/ #HW10 lapply (ssta_da_conf … HVW1 … Hl0) ⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_snv_lsstas h g G1 L1 T1. #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #HG0 #HL0 #HT0 #_ #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 @@ -37,19 +37,19 @@ fact snv_lsstas_aux: ∀h,g,G0,L0,T0. lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ] lapply (fqup_lref … G1 … HLK1) #H - lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbr, snv_lift/ + lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/ | #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) | #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 elim (snv_inv_bind … H1) -H1 #HV1 #HT1 lapply (da_inv_bind … Hl1) -Hl1 #Hl1 - elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbr, snv_bind/ + elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbg, snv_bind/ | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct elim (snv_inv_appl … H1) -H1 #a #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10 lapply (da_inv_flat … Hl1) -Hl1 #Hl1 elim (lsstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct - lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbr/ #HU1 - elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbr/ -T1 -l1 #X #l #_ #H #HU10 -l2 + lapply (IH1 … HT1 … Hl1 … HTU1) /2 width=1 by fqup_fpbg/ #HU1 + elim (lsstas_cpds_aux … IH1 IH4 IH3 IH2 … Hl1 … HTU1 … HT10) -IH4 -IH3 -IH2 -IH1 /2 width=1 by fqup_fpbg/ -T1 -l1 #X #l #_ #H #HU10 -l2 elim (lsstas_inv_bind1 … H) -H #U0 #_ #H destruct -T0 -l elim (cpes_inv_abst2 … HU10) -HU10 #W2 #U2 #HU12 #HU02 elim (cprs_inv_abst … HU02) -HU02 #HW02 #_ @@ -58,6 +58,6 @@ fact snv_lsstas_aux: ∀h,g,G0,L0,T0. [ lapply (lsstas_inv_O … H2) -H2 #H destruct // ] elim (snv_inv_cast … H1) -H1 lapply (da_inv_flat … Hl1) -Hl1 - lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbr/ + lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbg/ ] qed-. 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 423777820..2ff0d940c 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 @@ -23,10 +23,10 @@ include "basic_2/dynamic/lsubsv_lsstas.ma". (* Properties on sn parallel reduction for local environments ***************) fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → - (∀G1,L1,T1. ⦃G0, L0, T0⦄ ⊃≥[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_lsstas h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >⋕[h, g] ⦃G1, L1, T1⦄ → IH_lsstas_cpr_lpr h g G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lsstas_cpr_lpr h g G1 L1 T1. #h #g #G0 #L0 #T0 #IH4 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #_ #_ #_ #_ #l1 #l2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH4 -IH3 -IH2 -IH1 @@ -51,13 +51,13 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. |2,4: * #K0 #V0 #X0 #H #HVX0 #HX0 lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct ] - [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbr/ #V2 #HWV2 #HV2 + [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2 elim (lift_total V2 0 (i+1)) - /6 width=11 by fqup_fpbr, cpcs_lift, lsstas_ldec, ex2_intro/ - | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbr/ #W2 #HVW2 #HW02 + /6 width=11 by fqup_fpbg, cpcs_lift, lsstas_ldec, ex2_intro/ + | elim (IH1 … HVl1 … HW0 … HV12 … HK12) -IH1 -HVl1 -HW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02 elim (lift_total W2 0 (i+1)) /4 width=11 by cpcs_lift, lsstas_ldef, ex2_intro/ - | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbr/ -l1 #W2 #HXW2 #HW02 + | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02 elim (lift_total W2 0 (i+1)) /3 width=11 by cpcs_lift, lsstas_lift, ex2_intro/ ] @@ -69,10 +69,10 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct elim (cpr_inv_bind1 … H3) -H3 * [ #V2 #T2 #HV12 #HT12 #H destruct - elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbr, lpr_pair/ -T1 + elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 /4 width=5 by cpcs_bind2, lpr_cpr_conf, lsstas_bind, ex2_intro/ | #T3 #HT13 #HXT3 #H1 #H2 destruct - elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbr, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13 + elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13 elim (lsstas_inv_lift1 … HTU3 L2 … HXT3) -T3 /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_ldrop, ex2_intro/ ] @@ -83,7 +83,7 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. elim (cpr_inv_appl1 … H3) -H3 * [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH4 -IH3 -IH2 elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 - /4 width=5 by fqup_fpbr, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/ + /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/ | #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2 lapply (da_inv_bind … Hl1) -Hl1 #Hl1 @@ -92,18 +92,18 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. lapply (cprs_div … HW10 … HW20) -W0 #HW12 lapply (ssta_da_conf … HVW1 … Hl0) [h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/3 width=9 by fpbg_fqup, fpbg_cpxs, fpbg_lpxs/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc new file mode 100644 index 000000000..97846fda4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpbg.etc @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/lpxs_lpxs.ma". +include "basic_2/computation/fpbs_alt.ma". +include "basic_2/computation/fpbg.ma". + +(* GENERAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) + +(* Advanced forward lemmas **************************************************) + +lemma fpbg_fwd_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 #H elim H -G2 -L2 -T2 +/3 width=5 by cpxs_fqus_lpxs_fpbs, cpxs_fqup_fpbs, fpbs_trans, lpxs_fpbs, cpxs_fpbs/ +qed-. + +lemma fpbg_fwd_fpbc_sn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → + ∃∃G,L,T. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G, L, T⦄ & ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 +[ /4 width=5 by fpbc_cpxs, lpxs_fpbs, ex2_3_intro/ +| #G2 #L #L2 #T #T2 #HT1 #HT2 #HL2 elim (eq_term_dec T1 T) #H destruct + [ -HT1 /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/ + | /5 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, fqup_fqus, ex3_2_intro, ex2_3_intro/ + ] +| #G2 #L #L0 #L2 #T #T2 #HT1 #HT2 #HL0 #H0 #HL02 #H02 + lapply (lpxs_trans … HL0 … HL02) #HL2 + elim (eq_term_dec T1 T) #H destruct + [ -HT1 elim (fqus_inv_gen … HT2) -HT2 + [ /3 width=5 by fpbc_fqup, lpxs_fpbs, ex2_3_intro/ + | * #H1 #H2 #H3 destruct + /4 width=5 by fpbc_lpxs, lpxs_fpbs, ex2_3_intro/ + ] + | /4 width=9 by fpbc_cpxs, fpbsa_inv_fpbs, ex3_2_intro, ex2_3_intro/ + ] +] +qed-. + +(* Advanced properties ******************************************************) + +lemma fqu_fpbs_fpbg: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃ ⦃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 #H elim(fpbs_fpbsa … H) -H +#L0 #T0 #HT0 #HT02 #HL02 elim (fqu_cpxs_trans … HT0 … H1) -T +/3 width=7 by fpbg_fqup, fqus_strap2_fqu/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc new file mode 100644 index 000000000..0ed65c927 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_fpns.etc @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/fpns.ma". +include "basic_2/computation/fpbg.ma". + +(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) + +(* Properties on parallel computation for "big tree" normal forms ***********) + +axiom fpns_fpbg_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 * -F2 -K2 -T2 +#K2 #HK12 #HT1 #G2 #L2 #U2 * -G2 -L2 -U2 +[ /4 width=9 by fpbc_cpxs, fpns_intro, lpxs_cpxs_trans, lleq_cpxs_conf_dx, ex2_3_intro/ +| #G2 #L2 #U2 #H12 elim (lpxs_lleq_fqup_trans … H12 … HK12 HT1) -K2 + /3 width=5 by fpbc_fqup, fpns_intro, ex2_3_intro/ +| /5 width=5 by fpbc_lpxs, lpxs_trans, lleq_canc_sn, ex2_3_intro/ +] +qed-. +*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc new file mode 100644 index 000000000..26dec0777 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpbg/fpbg_lift.etc @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/fpbc_lift.ma". +include "basic_2/computation/fpbg.ma". + +(* GENERAL "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *********************) + +(* Advanced properties ******************************************************) + +lemma lsstas_fpbg: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → (T1 = T2 → ⊥) → + ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. +/4 width=5 by fpbc_fpbg, lsstas_fpbc/ qed. + +lemma ssta_fpbg: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → + ⦃G, L⦄ ⊢ T1 •[h, g] T2 → ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. +/3 width=2 by fpbc_fpbg, ssta_fpbc/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 31e1d7c40..6f00405d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -82,10 +82,11 @@ x: extended reduction - forth letter (if present) -c: proper single step (successor) +c: proper single step (general) (successor) e: reflexive transitive closure to normal form (evaluation) g: proper multiple step (general) (greater) p: non-reflexive transitive closure (plus) q: reflexive closure (question) r: proper multiple step (restricted) (restricted) s: reflexive transitive closure (star) +u: proper single step (restricted) (unit) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarrestricted_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarrestricted_8.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma index 139ec01da..a821838f7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarrestricted_8.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredproper_8.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⊃≥ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻⋕ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" non associative with precedence 45 - for @{ 'BTPRedStarRestricted $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. + for @{ 'LazyBTPRedProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma new file mode 100644 index 000000000..91a275ab8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >⋕ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'LazyBTPRedStarProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. 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 6e021dd88..48a2983e9 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 @@ -80,20 +80,20 @@ table { } ] [ { "strongly normalizing \"big tree\" computation" * } { - [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_fleq" + "fsb_csx" * ] + [ "fsb ( ⦃?,?⦄ ⊢ ⦥[?,?] ? )" "fsb_alt ( ⦃?,?⦄ ⊢ ⦥⦥[?,?] ? )" "fsb_aaa" + "fsb_csx" * ] } ] [ { "strongly normalizing extended computation" * } { - [ "lsx ()" "lsx_cpxs" + "lsx_fpbc" + "lsx_csx" * ] - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] + [ "lsx ( ? ⊢ ⬊*[?,?,?] ? )" "lsx_cpxs" + "lsx_csx" * ] + [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" + "csx_fpbs" * ] } ] [ { "\"big tree\" parallel computation" * } { - [ "fpbr ( ⦃?,?,?⦄ ⊃≥[?,?] ⦃?,?,?⦄ )" "fpbr_fpbr" * ] - [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ] - [ "fpbc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbc_lift" + "fpbc_fpns" * ] - [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ] + [ "fpbg ( ⦃?,?,?⦄ >⋕[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpns" + "fpbg_fpbg" * ] + [ "fpbc ( ⦃?,?,?⦄ ≻⋕[?,?] ⦃?,?,?⦄ )" "fpbc_fpns" + "fpbc_fpbs" * ] + [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_fpns" * ] + [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpns" + "fpbs_fpbs" * ] } ] [ { "parallel computation for \"big tree\" normal forms" * } { -- 2.39.2