From: Ferruccio Guidi Date: Fri, 25 Oct 2013 19:27:16 +0000 (+0000) Subject: - bug fix in the induction for the closure property X-Git-Tag: make_still_working~1065 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=02df4ecb9d5ad173a3e306952cc09d83b62cfdcf - bug fix in the induction for the closure property - some renaming --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma index 2f79d793b..ae51de39d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma @@ -146,3 +146,14 @@ lemma cpxs_inv_cnx1: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L #T0 #T #H1T0 #_ #IHT #H2T0 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ qed-. + +lemma cpxs_neq_inv_step_sn: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T & T1 = T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[h, g] T2. +#h #g #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 +[ #H elim H -H // +| #T1 #T #H1 #H2 #IH2 #H12 elim (eq_term_dec T1 T) #H destruct + [ -H1 -H2 /3 width=1 by/ + | -IH2 /3 width=4 by ex3_intro/ (**) (* auto fails without clear *) + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma index 61174c0ff..3ba52668c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma @@ -48,7 +48,7 @@ lemma csx_cpx_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∀T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ ⬊*[h, g] T2. #h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 @csx_intro #T #HLT2 #HT2 -elim (term_eq_dec T1 T2) #HT12 +elim (eq_term_dec T1 T2) #HT12 [ -IHT1 -HLT12 destruct /3 width=1/ | -HT1 -HT2 /3 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma index 7c95fed6e..ccd336acb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_alt.ma @@ -55,7 +55,7 @@ lemma csxa_cpxs_trans: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T1 → ∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L⦄ ⊢ ⬊⬊*[h, g] T2. #h #g #G #L #T1 #H elim H -T1 #T1 #HT1 #IHT1 #T2 #HLT12 @csxa_intro #T #HLT2 #HT2 -elim (term_eq_dec T1 T2) #HT12 +elim (eq_term_dec T1 T2) #HT12 [ -IHT1 -HLT12 destruct /3 width=1/ | -HT1 -HT2 /3 width=4/ qed. @@ -69,7 +69,7 @@ lemma csxa_intro_cpx: ∀h,g,G,L,T1. ( [ -H #H destruct #H elim H // | #T0 #T #HLT1 #HLT2 #IHT #HT10 #HT12 destruct - elim (term_eq_dec T0 T) #HT0 + elim (eq_term_dec T0 T) #HT0 [ -HLT1 -HLT2 -H /3 width=1/ | -IHT -HT12 /4 width=3/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma index a365b4310..c387f545c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma @@ -90,7 +90,7 @@ elim (cpx_inv_appl1 … HL) -HL * elim (cpx_inv_abbr1 … HL) -HL * [ #V3 #T3 #HV3 #HLT3 #H0 destruct elim (lift_total V0 0 1) #V4 #HV04 - elim (term_eq_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) + elim (eq_term_dec (ⓓ{a}V.ⓐV2.T) (ⓓ{a}V3.ⓐV4.T3)) [ -IHVT #H0 destruct elim (eq_false_inv_tpair_sn … H) -H [ -HLV10 -HV3 -HLT3 -HVT diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index cf46c84d1..29cbd8d5d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -16,75 +16,40 @@ include "basic_2/notation/relations/btpredstarproper_8.ma". include "basic_2/reduction/fpbc.ma". include "basic_2/computation/fpbs.ma". -(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************) +(* GENEARAL "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES *************) inductive fpbg (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ -| fpbg_inj : ∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ≥[h, g] ⦃G, L, T⦄ → ⦃G, L, T⦄ ≻[h, g] ⦃G2, L2, T2⦄ → +| 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_step: ∀G,L,L2,T. fpbg h g G1 L1 T1 G L T → ⦃G, L⦄ ⊢ ➡[h, g] L2 → fpbg h g G1 L1 T1 G L2 T . 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). -(* Basic forvard 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 fpbs_strap1, fpbc_fwd_fpb, fpb_lpx/ -qed-. - (* 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⦄. -/3 width=5 by fpbg_inj, fpbg_step/ qed. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/3 width=5 by fpbg_cpxs, fpbg_fqup, fqu_fqup, cpx_cpxs/ +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⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 -lapply (fpbg_fwd_fpbs … H1) #H0 -elim (fpb_fpbc_or_fpn … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] -/2 width=5 by fpbg_inj, fpbg_step/ -qed-. +axiom 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⦄. -lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ → +axiom 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⦄. -#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -G2 -L2 -T2 -/3 width=5 by fpbg_step, fpbg_inj, fpbs_strap2/ -qed-. lemma fpbg_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 +#h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H @(fpbs_ind … H) -G2 -L2 -T2 /2 width=5 by fpbg_strap1/ 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 #HT1 @(fpbs_ind … HT1) -G -L -T +lemma fpbs_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 #H @(fpbs_ind_dx … H) -G1 -L1 -T1 /3 width=5 by fpbg_strap2/ qed-. - -lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … L2 T2 H) -G2 -L2 -T2 -/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fqu, fpb_fquq, fqu_fquq/ -qed. - -lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → - ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. -#h #g #G #L #T1 #T2 #H @(cpxs_ind … H) -T2 -[ #H elim H // -| #T #T2 #_ #HT2 #IHT1 #HT12 - elim (term_eq_dec T1 T) #H destruct - [ -IHT1 /4 width=1/ - | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1 - @(fpbg_strap1 … HT1) -HT1 /2 width=1 by fpb_cpx/ - ] -] -qed. - -lemma cprs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → - ⦃G, L, T1⦄ >[h, g] ⦃G, L, T2⦄. -/3 width=1 by cprs_cpxs, cpxs_fpbg/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_alt.ma deleted file mode 100644 index c74629d3f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_alt.ma +++ /dev/null @@ -1,37 +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/btpredstarproper_8.ma". -include "basic_2/reduction/fpbc.ma". -include "basic_2/computation/fpbs.ma". - -(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************) - -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 -. - -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). - -(* 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=5 by fpbg_cpxs, fpbg_fqup, fqu_fqup, cpx_cpxs/ -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 deleted file mode 100644 index 4f092111a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/fpbg.ma". - -(* "BIG TREE" ORDER FOR CLOSURES ********************************************) - -(* Main properties **********************************************************) - -theorem fpbg_trans: ∀h,g. tri_transitive … (fpbg h g). -/3 width=5 by fpbg_fwd_fpbs, fpbg_fpbs_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 9afc2523b..7a964e40f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_lift.ma @@ -12,28 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/unfold/lsstas_lift.ma". -include "basic_2/reduction/fpb_lift.ma". -include "basic_2/reduction/fpbc_lift.ma". +include "basic_2/computation/cpxs_lift.ma". include "basic_2/computation/fpbg.ma". -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) +(* 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⦄. -#h #g #G #L #T1 #T2 #l2 #H @(lsstas_ind_dx … H) -l2 -T2 -[ #H elim H // -| #l2 #T #T2 #HT1 #HT2 #IHT1 #HT12 #l1 #Hl21 - elim (term_eq_dec T1 T) #H destruct [ -IHT1 |] - [ elim (le_inv_plus_l … Hl21) -Hl21 #_ #Hl1 - >(plus_minus_m_m … Hl1) -Hl1 /3 width=5 by ssta_fpbc, fpbg_inj/ - | #Hl1 >commutative_plus in Hl21; #Hl21 - elim (le_inv_plus_l … Hl21) -Hl21 #Hl12 #Hl21 - lapply (lsstas_da_conf … HT1 … Hl1) -HT1 - >(plus_minus_m_m … Hl12) -Hl12 - /4 width=5 by ssta_fpb, fpbg_strap1/ - ] -] -qed. +/4 width=5 by fpbg_cpxs, lsstas_cpxs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma new file mode 100644 index 000000000..099567d41 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr.ma @@ -0,0 +1,72 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpbg.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 forward lemmas *****************************************************) + +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 H -G2 -L2 -T2 +/3 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fqu/ +qed-. + +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/fpbr_fpbr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma new file mode 100644 index 000000000..786030aff --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbr_fpbr.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fpbg_fpbg.ma". +include "basic_2/computation/fpbr.ma". + +(* RESTRICTED "BIG TREE" ORDER FOR CLOSURES *********************************) + +(* Advanced 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⦄. +/3 width=5 by fpbr_fwd_fpbg, fpbg_fwd_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/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma index 064c94f04..0f63844e2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma @@ -55,9 +55,15 @@ lemma fpbs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. /2 width=5 by tri_TC_strap/ qed-. +lemma fqup_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/4 width=5 by fqu_fquq, fpb_fquq, tri_step/ +qed. + lemma fqus_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … L2 T2 H) -G2 -L2 -T2 +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 /3 width=5 by fpb_fquq, tri_step/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma index 86cbe3ee3..1135589db 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma @@ -28,3 +28,7 @@ lemma cpr_lpr_ssta_fpbs: ∀h,g,G,L1,L2,T1,T2,U2,l2. ⦃G, L2⦄ ⊢ T2 ▪[h, g] l2+1 → ⦃G, L2⦄ ⊢ T2 •[h, g] U2 → ⦃G, L1, T1⦄ ≥[h, g] ⦃G, L2, U2⦄. /3 width=5 by fpbs_trans, cpr_lpr_fpbs, ssta_fpbs/ qed. + +lemma cpxs_fqup_fpbs: ∀h,g,G1,G2,L1,L2,T1,T,T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T → + ⦃G1, L1, T⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. +/3 width=5 by fpbs_trans, cpxs_fpbs, fqup_fpbs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma index 19136df6f..70cabad47 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma @@ -12,25 +12,18 @@ (* *) (**************************************************************************) -include "basic_2/unfold/lsstas_lift.ma". -include "basic_2/reduction/fpb_lift.ma". +include "basic_2/computation/cpxs_lift.ma". include "basic_2/computation/fpbs.ma". (* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) (* Advanced properties ******************************************************) +lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → + ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. +/3 width=5 by cpxs_fpbs, lsstas_cpxs/ qed. + lemma ssta_fpbs: ∀h,g,G,L,T,U,l. ⦃G, L⦄ ⊢ T ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T •[h, g] U → ⦃G, L, T⦄ ≥[h, g] ⦃G, L, U⦄. -/3 width=2 by fpb_fpbs, ssta_fpb/ qed. - -lemma lsstas_fpbs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, g, l2] T2 → - ∀l1. l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄. -#h #g #G #L #T1 #T2 #l2 #H @(lsstas_ind_dx … H) -l2 -T2 // -#l2 #T #T2 #HT1 #HT2 #IHT1 #l1 >commutative_plus #Hl21 #Hl1 -elim (le_inv_plus_l … Hl21) -Hl21 #Hl12 #Hl21 -lapply (lsstas_da_conf … HT1 … Hl1) -HT1 ->(plus_minus_m_m … Hl12) -Hl12 -/3 width=5 by ssta_fpb, fpbs_strap1/ -qed. +/3 width=5 by lsstas_fpbs, ssta_lsstas/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma deleted file mode 100644 index 29b81d043..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma +++ /dev/null @@ -1,56 +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/predsnstar_8.ma". -include "basic_2/reduction/fpn.ma". -include "basic_2/computation/lpxs.ma". - -(* ORDERED "BIG TREE" NORMAL FORMS ******************************************) - -definition fpns: ∀h. sd h → tri_relation genv lenv term ≝ - λh,g,G1,L1,T1,G2,L2,T2. - ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & T1 = T2. - -interpretation - "ordered 'big tree' normal forms (closure)" - 'PRedSnStar h g G1 L1 T1 G2 L2 T2 = (fpns h g G1 L1 T1 G2 L2 T2). - -(* Basic_properties *********************************************************) - -lemma fpns_refl: ∀h,g. tri_reflexive … (fpns h g). -/2 width=1 by and3_intro/ qed. - -lemma fpn_fpns: ∀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 * /3 width=1 by lpx_lpxs, and3_intro/ -qed. - -lemma fpns_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 * #H1G #H1L #G1T * -/3 width=3 by lpxs_strap1, and3_intro/ -qed-. - -lemma fpns_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 * #H1G #H1L #G1T * -/3 width=3 by lpxs_strap2, and3_intro/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma fpns_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ➡*[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=4 by lpxs_fwd_length, and3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index 6c24fe86b..e89bf398a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -28,19 +28,6 @@ interpretation "'big tree' strong normalization (closure)" 'BTSN h g G L T = (fsb h g G L T). -(* Basic eliminators ********************************************************) - -theorem fsb_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⦄ → - (⦃G1, L1, T1⦄ ⋕ ⦃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 -/5 width=1 by fpb_fpbc, fsb_intro/ -qed-. - (* Basic inversion lemmas ***************************************************) lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. 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 1d9c2a497..ceb1230ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_alt.ma @@ -13,10 +13,10 @@ (**************************************************************************) include "basic_2/notation/relations/btsnalt_5.ma". -include "basic_2/computation/fpbg_alt.ma". +include "basic_2/computation/fpbg.ma". include "basic_2/computation/fsb.ma". -(* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) +(* GENERAL "BIG TREE" STRONGLY NORMALIZING TERMS ****************************) (* Note: alternative definition of fsb *) inductive fsba (h) (g): relation3 genv lenv term ≝ 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 086cf114b..f9bea7ca4 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/fpbg.ma". +include "basic_2/computation/fpbr.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 fpbg_fpbs_trans, cprs_fpbs/ +@(cprs_ind … H) -T2 /4 width=6 by fpbr_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, fpbg_fpbs_trans, cprs_fpbs/ +@(cprs_ind … H) -T2 /4 width=10 by snv_cprs_lpr_aux, fpbr_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,10 +88,10 @@ 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 → @@ -103,18 +103,18 @@ 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 fpbg_fpbs_trans, cprs_fpbs/ +|4: /3 width=5 by fpbr_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 @@ -125,18 +125,18 @@ lapply (lsstas_mono … H1 … H2) -h -T -l #H destruct /2 width=3 by cpcs_canc_ 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 fpbg_fpbs_trans, lsstas_fpbs, monotonic_le_minus_l/ -T #U2 #HTU2 #HU12 + /3 width=8 by fpbr_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 d1363a3cf..a15ef134b 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_fpbg/ + /4 width=10 by da_ldef, da_ldec, fqup_fpbr/ |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_fpbg/ + /4 width=7 by da_lift, fqup_fpbr/ ] | #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_fpbg, lpr_pair/ + /4 width=9 by da_bind, fqup_fpbr, lpr_pair/ | #T2 #HT12 #HT2 #H1 #H2 destruct - /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_ldrop/ + /4 width=11 by da_inv_lift, fqup_fpbr, 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_fpbg/ + [ #V2 #T2 #HV12 #HT12 #H destruct -IH3 -IH2 /4 width=7 by da_flat, fqup_fpbr/ | #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, 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_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_fpbg, snv_lref/ + [ #H destruct -HLK1 /4 width=10 by fqup_fpbr, 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_fpbg, snv_lift/ + lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbr, 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_fpbg, snv_bind, lpr_pair/ + [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbr, snv_bind, lpr_pair/ | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 - /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/ + /4 width=10 by fqup_fpbr, 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_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 + 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 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_fpbg/ #HW10 + lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fqup_fpbr/ #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, 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 = 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_fpbg, snv_lift/ + lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbr, 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_fpbg, snv_bind/ + elim (lsstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct /4 width=8 by fqup_fpbr, 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_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 + 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 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_fpbg/ + lapply (lsstas_inv_cast1 … H2) -H2 /3 width=8 by fqup_fpbr/ ] 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 5166e92a2..423777820 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_fpbg/ #V2 #HWV2 #HV2 + [ elim (IH1 … HWl1 … HW0 … HW12 … HK12) -IH1 -HW0 /2 width=1 by fqup_fpbr/ #V2 #HWV2 #HV2 elim (lift_total V2 0 (i+1)) - /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 + /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 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_fpbg/ -l1 #W2 #HXW2 #HW02 + | elim (IH1 … HVl1 … HW0 … HVX0 … HK12) -IH1 -HVl1 -HW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbr/ -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_fpbg, lpr_pair/ -T1 + elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbr, 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_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13 + 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 (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_fpbg, cpcs_flat, lpr_cpr_conf, lsstas_appl, ex2_intro/ + /4 width=5 by fqup_fpbr, 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 -L #H + elim (lt_refl_false … H) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fsb.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fsb.etc new file mode 100644 index 000000000..3cd6861ad --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/fsb.etc @@ -0,0 +1,12 @@ +(* Basic eliminators ********************************************************) + +theorem fsb_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⦄ → + (⦃G1, L1, T1⦄ ⋕ ⦃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 +/5 width=1 by fpb_fpbc, fsb_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsn_8.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsn_8.etc new file mode 100644 index 000000000..dc3b08203 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsn_8.etc @@ -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 @{ 'PRedSn $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsnstar_8.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsnstar_8.etc new file mode 100644 index 000000000..f396ff17d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpn/predsnstar_8.etc @@ -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 @{ 'PRedSnStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma index 6f0a4d7c2..72ae1cd80 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma @@ -55,7 +55,7 @@ qed-. (* Basic properties *********************************************************) -lemma aarity_eq_dec: ∀A1,A2:aarity. Decidable (A1 = A2). +lemma eq_aarity_dec: ∀A1,A2:aarity. Decidable (A1 = A2). #A1 elim A1 -A1 [ #A2 elim A2 -A2 /2 width=1/ #B2 #A2 #_ #_ @or_intror #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma deleted file mode 100644 index c909e2ed6..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma +++ /dev/null @@ -1,46 +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/bteq_6.ma". -include "basic_2/grammar/lenv_length.ma". -include "basic_2/grammar/genv.ma". - -(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************) - -definition bteq: tri_relation genv lenv term ≝ - λG1,L1,T1,G2,L2,T2. - ∧∧ G1 = G2 & |L1| = |L2| & T1 = T2. - -interpretation - "equivalent 'big tree' normal forms (closure)" - 'BTEq G1 L1 T1 G2 L2 T2 = (bteq G1 L1 T1 G2 L2 T2). - -(* Basic_properties *********************************************************) - -lemma bteq_refl: tri_reflexive … bteq. -/2 width=1 by and3_intro/ qed. - -lemma bteq_sym: tri_symmetric … bteq. -#G1 #G2 #L1 #L2 #T1 #T2 * // -qed-. - -lemma bteq_dec: ∀G1,G2,L1,L2,T1,T2. Decidable (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄). -#G1 #G2 #L1 #L2 #T1 #T2 elim (genv_eq_dec G1 G2) -#H1G [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ] -elim (eq_nat_dec (|L1|) (|L2|)) -#H1L [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ] -elim (term_eq_dec T1 T2) -#H1T [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ] -/3 width=1 by and3_intro, or_introl/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma deleted file mode 100644 index 7870b2644..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma +++ /dev/null @@ -1,31 +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/grammar/bteq.ma". - -(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************) - -(* Main properties **********************************************************) - -theorem bteq_trans: tri_transitive … bteq. -#G1 #G #L1 #L #T1 #T * // -qed-. - -theorem bteq_canc_sn: ∀G,G1,G2,L,L1,L2,T,T1,T2. ⦃G, L, T⦄ ⋕ ⦃G1, L1, T1⦄ → - ⦃G, L, T⦄ ⋕ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄. -/3 width=5 by bteq_trans, bteq_sym/ qed-. - -theorem bteq_canc_dx: ∀G1,G2,G,L1,L2,L,T1,T2,T. ⦃G1, L1, T1⦄ ⋕ ⦃G, L, T⦄ → - ⦃G2, L2, T2⦄ ⋕ ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄. -/3 width=5 by bteq_trans, bteq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma index 3308b79ed..2ab808305 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma @@ -38,4 +38,4 @@ interpretation "abstraction (global environment)" (* Basic properties *********************************************************) -axiom genv_eq_dec: ∀G1,G2:genv. Decidable (G1 = G2). +axiom eq_genv_dec: ∀G1,G2:genv. Decidable (G1 = G2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma index bc0b447c4..b85496fa5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma @@ -43,16 +43,16 @@ inductive item2: Type[0] ≝ (* Basic properties *********************************************************) -axiom item0_eq_dec: ∀I1,I2:item0. Decidable (I1 = I2). +axiom eq_item0_dec: ∀I1,I2:item0. Decidable (I1 = I2). (* Basic_1: was: bind_dec *) -axiom bind2_eq_dec: ∀I1,I2:bind2. Decidable (I1 = I2). +axiom eq_bind2_dec: ∀I1,I2:bind2. Decidable (I1 = I2). (* Basic_1: was: flat_dec *) -axiom flat2_eq_dec: ∀I1,I2:flat2. Decidable (I1 = I2). +axiom eq_flat2_dec: ∀I1,I2:flat2. Decidable (I1 = I2). (* Basic_1: was: kind_dec *) -axiom item2_eq_dec: ∀I1,I2:item2. Decidable (I1 = I2). +axiom eq_item2_dec: ∀I1,I2:item2. Decidable (I1 = I2). (* Basic_1: removed theorems 21: s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma index 909231ae8..95e155b74 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma @@ -40,7 +40,7 @@ interpretation "abstraction (local environment)" (* Basic properties *********************************************************) -axiom lenv_eq_dec: ∀L1,L2:lenv. Decidable (L1 = L2). +axiom eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma index e22681c4a..5b62fa940 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma @@ -93,7 +93,7 @@ interpretation "native type annotation (term)" (* Basic properties *********************************************************) (* Basic_1: was: term_dec *) -axiom term_eq_dec: ∀T1,T2:term. Decidable (T1 = T2). +axiom eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2). (* Basic inversion lemmas ***************************************************) @@ -120,7 +120,7 @@ lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2. (②{I} V1. T1 = ②{I} V2. T2 → ⊥) → (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)). #I #V1 #T1 #V2 #T2 #H -elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct +elim (eq_term_dec V1 V2) /3 width=1/ #HV12 destruct @or_intror @conj // #HT12 destruct /2 width=1/ qed-. @@ -128,7 +128,7 @@ lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2. (②{I} V1. T1 = ②{I} V2. T2 → ⊥) → (T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)). #I #V1 #T1 #V2 #T2 #H -elim (term_eq_dec T1 T2) /3 width=1/ #HT12 destruct +elim (eq_term_dec T1 T2) /3 width=1/ #HT12 destruct @or_intror @conj // #HT12 destruct /2 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma index f3ef6187e..defc91ed9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tstc.ma @@ -81,7 +81,7 @@ qed. lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2). * #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ] -[ elim (item2_eq_dec I1 I2) #HI12 +[ elim (eq_item2_dec I1 I2) #HI12 [ destruct /2 width=1/ | @or_intror #H elim (tstc_inv_pair1 … H) -H #V #T #H destruct /2 width=1/ @@ -90,7 +90,7 @@ lemma tstc_dec: ∀T1,T2. Decidable (T1 ≃ T2). lapply (tstc_inv_atom1 … H) -H #H destruct | @or_intror #H lapply (tstc_inv_atom2 … H) -H #H destruct -| elim (item0_eq_dec I1 I2) #HI12 +| elim (eq_item0_dec I1 I2) #HI12 [ destruct /2 width=1/ | @or_intror #H lapply (tstc_inv_atom2 … H) -H #H destruct /2 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index b5405f69d..87d49091b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -73,7 +73,6 @@ b: "big tree" reduction c: conversion d: decomposed extended reduction e: decomposed extended conversion -n: order on "big tree" normal forms q: restricted reduction r: reduction s: substitution @@ -84,7 +83,8 @@ x: extended reduction c: proper single step (successor) e: reflexive transitive closure to normal form (evaluation) -g: proper multiple step (greater) +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) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma deleted file mode 100644 index 5ee962fe5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⋕ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTEq $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarrestricted_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarrestricted_8.ma new file mode 100644 index 000000000..139ec01da --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstarrestricted_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 @{ 'BTPRedStarRestricted $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_8.ma deleted file mode 100644 index dc3b08203..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_8.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* 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 @{ 'PRedSn $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_8.ma deleted file mode 100644 index f396ff17d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_8.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* 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 @{ 'PRedSnStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma index 1abe847ab..94c114260 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/btpred_8.ma". include "basic_2/relocation/fquq_alt.ma". -include "basic_2/reduction/fpn.ma". +include "basic_2/reduction/lpx.ma". (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) @@ -38,16 +38,3 @@ lemma cpr_fpb: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L, T1⦄ ≽ lemma lpr_fpb: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡ L2 → ⦃G, L1, T⦄ ≽[h, g] ⦃G, L2, T⦄. /3 width=1 by fpb_lpx, lpr_lpx/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma fpb_bteq_fwd_fpn: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⋕ ⦃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 by and3_intro/ -[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H - [ #H1 #H2 elim (fqu_fwd_bteq … H1 H2) - | * #HG #HL #HT #_ destruct // - ] -| #T2 #HT12 * // -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma index c560a1ab0..45e671601 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma @@ -32,25 +32,6 @@ lemma cpr_fpbc: ∀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_cpx, cpr_cpx/ qed. -lemma fpb_fpbc_or_fpn: ∀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 -/3 width=1 by and3_intro, or_intror/ -[ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H [| * ] - /3 width=1 by fpbc_fqu, and3_intro, or_introl, or_intror/ -| #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct - /4 width=1 by and3_intro, or_introl, or_intror, fpbc_cpx/ -] -qed-. - -lemma fpb_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - (⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥) → - ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #H0 elim (fpb_fpbc_or_fpn … H) -H // -#H elim H0 -H0 /2 width=3 by fpn_fwd_bteq/ -qed. - (* Basic forward lemmas *****************************************************) lemma fpbc_fwd_fpb: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → @@ -58,9 +39,3 @@ lemma fpbc_fwd_fpb: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /3 width=1 by fpb_fquq, fpb_cpx, fqu_fquq/ qed-. - -lemma fpbc_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=8 by fqu_fwd_bteq/ -#T2 #_ #HT12 * /2 width=1 by/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma index 6236452bb..987258b79 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc_lift.ma @@ -22,7 +22,7 @@ include "basic_2/reduction/fpbc.ma". lemma ssta_fpbc: ∀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 (term_eq_dec T1 T2) +#h #g #G #L #T1 #T2 #l #HT1 #HT12 elim (eq_term_dec T1 T2) /3 width=5 by fpbc_cpx, ssta_cpx/ #H destruct elim (ssta_inv_refl_pos … HT1 … HT12) qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpn.ma deleted file mode 100644 index f33adbde9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpn.ma +++ /dev/null @@ -1,39 +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/predsn_8.ma". -include "basic_2/grammar/bteq.ma". -include "basic_2/reduction/lpx.ma". - -(* ADJACENT "BIG TREE" NORMAL FORMS *****************************************) - -definition fpn: ∀h. sd h → tri_relation genv lenv term ≝ - λh,g,G1,L1,T1,G2,L2,T2. - ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2. - -interpretation - "adjacent 'big tree' normal forms (closure)" - 'PRedSn h g G1 L1 T1 G2 L2 T2 = (fpn h g G1 L1 T1 G2 L2 T2). - -(* Basic_properties *********************************************************) - -lemma fpn_refl: ∀h,g. tri_reflexive … (fpn h g). -/2 width=1 by and3_intro/ qed. - -(* Basic forward lemmas *****************************************************) - -lemma fpn_fwd_bteq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢➡[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * /3 width=4 by lpx_fwd_length, and3_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma index 3b4690edd..98d45f043 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma @@ -14,7 +14,6 @@ include "basic_2/notation/relations/supterm_6.ma". include "basic_2/grammar/cl_weight.ma". -include "basic_2/grammar/bteq.ma". include "basic_2/relocation/ldrop.ma". (* SUPCLOSURE ***************************************************************) @@ -67,19 +66,6 @@ lemma fqu_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃ ⦃G2, L2, /2 width=7 by fqu_fwd_length_lref1_aux/ qed-. -lemma fqu_fwd_bteq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ⋕ ⦃G2, L2, T2⦄ → ⊥. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I #G #L #V * #_ #H elim (plus_xSy_x_false … H) -| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_x … H) -| #a #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H) -| #I #G #L #V #T * #_ #_ #H elim (discr_tpair_xy_y … H) -| #G #L #K #T #U #e #HLK #_ * #_ #H - lapply (ldrop_fwd_length_lt4 … HLK ?) // >H -L #H - elim (lt_refl_false … H) -] -qed-. - (* Advanced eliminators *****************************************************) lemma fqu_wf_ind: ∀R:relation3 …. ( diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/gget_gget.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/gget_gget.ma index 6c1001b6a..ee7027ce4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/gget_gget.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/gget_gget.ma @@ -32,7 +32,7 @@ qed-. lemma gget_dec: ∀G1,G2,e. Decidable (⇩[e] G1 ≡ G2). #G1 #G2 #e elim (gget_total e G1) #G #HG1 -elim (genv_eq_dec G G2) #HG2 +elim (eq_genv_dec G G2) #HG2 [ destruct /2 width=1/ | @or_intror #HG12 lapply (gget_mono … HG1 … HG12) -HG1 -HG12 /2 width=1/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma index f33a942a6..325be4b39 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma @@ -73,3 +73,11 @@ lemma fqus_fwd_fw: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -L2 -T2 /3 width=3 by fquq_fwd_fw, transitive_le/ qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma fqup_inv_step_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → + ∃∃G,L,T. ⦃G1, L1, T1⦄ ⊃ ⦃G, L, T⦄ & ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄. +#G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 /2 width=5 by ex2_3_intro/ +#G1 #G #L1 #L #T1 #T #H1 #_ * /4 width=9 by fqus_strap2, fqu_fquq, ex2_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma index 0d8241111..2681a04ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_alt.ma @@ -54,8 +54,8 @@ lemma fqus_fqup_trans: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G, L /2 width=5 by fqus_strap1_fqu, fqup_strap1/ qed-. -lemma fqup_fqus_trans: ∀G1,G,L1,L,T1,T. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → - ∀G2,L2,T2. ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. -#G1 #G #L1 #L #T1 #T #H1 @(fqup_ind_dx … H1) -H1 -G1 -L1 -T1 +lemma fqup_fqus_trans: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G, L, T⦄ → + ⦃G, L, T⦄ ⊃* ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. +#G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 @(fqup_ind_dx … H1) -H1 -G1 -L1 -T1 /3 width=5 by fqus_strap2_fqu, fqup_strap2/ 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 0b1ec4de4..a78ccb133 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 @@ -89,7 +89,8 @@ table { } ] [ { "\"big tree\" parallel computation" * } { - [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_alt" "fpbg_lift" + "fpbg_fpbg" * ] + [ "fpbr ( ⦃?,?,?⦄ ⊃≥[?,?] ⦃?,?,?⦄ )" "fpbr_fpbr" * ] + [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ] [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ] } ] @@ -207,7 +208,7 @@ table { } ] [ { "iterated structural successor for closures" * } { - [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" "fqus_fqus" * ] + [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ] [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ] } ] @@ -258,7 +259,6 @@ table { } ] [ { "closures" * } { -(* [ "bteq ( ⦃?,?,?⦄ ⪴ ⦃?,?,?⦄ )" "bteq_bteq" * ] *) [ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?,?} )" * ] } ]