From: Ferruccio Guidi Date: Wed, 29 Jan 2014 18:55:32 +0000 (+0000) Subject: bug fix in the notation of normal forms, now we specify that they are X-Git-Tag: make_still_working~984 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=606dab57f31b66eb3f30f603185124b88dfad4c1;p=helm.git bug fix in the notation of normal forms, now we specify that they are normal forms for reduction. This will allow to enable normal forms for substitution ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma index 61dadbcde..2e81a1a0a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma @@ -19,7 +19,7 @@ include "basic_2/computation/csx.ma". (* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************) definition cpre: relation4 genv lenv term term ≝ - λG,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 ∧ ⦃G, L⦄ ⊢ 𝐍⦃T2⦄. + λG,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 ∧ ⦃G, L⦄ ⊢ ➡ 𝐍⦃T2⦄. interpretation "context-sensitive parallel evaluation (term)" 'PEval G L T1 T2 = (cpre G L T1 T2). @@ -29,8 +29,7 @@ interpretation "context-sensitive parallel evaluation (term)" (* Basic_1: was just: nf2_sn3 *) lemma csx_cpre: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡* 𝐍⦃T2⦄. #h #g #G #L #T1 #H @(csx_ind … H) -T1 -#T1 #_ #IHT1 -elim (cnr_dec G L T1) /3 width=3/ -* #T #H1T1 #H2T1 -elim (IHT1 … H2T1) -IHT1 -H2T1 [2: /2 width=2/ ] #T2 * /4 width=3/ +#T1 #_ #IHT1 elim (cnr_dec G L T1) /3 width=3 by ex_intro, conj/ +* #T #H1T1 #H2T1 elim (IHT1 … H2T1) -IHT1 -H2T1 /2 width=2 by cpr_cpx/ +#T2 * /4 width=3 by cprs_strap2, ex_intro, conj/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index 640f4dbfc..45c8cfe7d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -44,20 +44,20 @@ qed-. (* Basic_1: was: pr3_pr2 *) lemma cpr_cprs: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2. -/2 width=1/ qed. +/2 width=1 by inj/ qed. (* Basic_1: was: pr3_refl *) lemma cprs_refl: ∀G,L,T. ⦃G, L⦄ ⊢ T ➡* T. -/2 width=1/ qed. +/2 width=1 by cpr_cprs/ qed. lemma cprs_strap1: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ T ➡ T2 → ⦃G, L⦄ ⊢ T1 ➡* T2. -normalize /2 width=3/ qed. +normalize /2 width=3 by step/ qed. (* Basic_1: was: pr3_step *) lemma cprs_strap2: ∀G,L,T1,T,T2. ⦃G, L⦄ ⊢ T1 ➡ T → ⦃G, L⦄ ⊢ T ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2. -normalize /2 width=3/ qed. +normalize /2 width=3 by TC_strap/ qed. lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr. /3 width=5 by lsubr_cpr_trans, LTC_lsub_trans/ @@ -65,51 +65,49 @@ qed-. (* Basic_1: was: pr3_pr1 *) lemma tprs_cprs: ∀G,L,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ T1 ➡* T2. -#G #L #T1 #T2 #H @(lsubr_cprs_trans … H) -H // -qed. +/2 width=3 by lsubr_cprs_trans/ qed. lemma cprs_bind_dx: ∀G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡* T2 → ∀a. ⦃G, L⦄ ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. #G #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1 -/3 width=1/ /3 width=3/ -qed. +/3 width=3 by cprs_strap2, cpr_cprs, cpr_pair_sn, cpr_bind/ qed. (* Basic_1: was only: pr3_thin_dx *) lemma cprs_flat_dx: ∀I,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2. -#I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 /3 width=1/ -#T #T2 #_ #HT2 #IHT1 -@(cprs_strap1 … IHT1) -V1 -T1 /2 width=1/ +#I #G #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 +/3 width=5 by cprs_strap1, cpr_flat, cpr_cprs, cpr_pair_sn/ qed. lemma cprs_flat_sn: ∀I,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ∀V1,V2. ⦃G, L⦄ ⊢ V1 ➡* V2 → ⦃G, L⦄ ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2. -#I #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind … H) -V2 /3 width=1/ -#V #V2 #_ #HV2 #IHV1 -@(cprs_strap1 … IHV1) -V1 -T1 /2 width=1/ +#I #G #L #T1 #T2 #HT12 #V1 #V2 #H @(cprs_ind … H) -V2 +/3 width=3 by cprs_strap1, cpr_cprs, cpr_pair_sn, cpr_flat/ qed. lemma cprs_zeta: ∀G,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T → ⦃G, L.ⓓV⦄ ⊢ T1 ➡* T → ⦃G, L⦄ ⊢ +ⓓV.T1 ➡* T2. -#G #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/ +#G #L #V #T1 #T #T2 #HT2 #H @(cprs_ind_dx … H) -T1 +/3 width=3 by cprs_strap2, cpr_cprs, cpr_bind, cpr_zeta/ qed. lemma cprs_tau: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → ∀V. ⦃G, L⦄ ⊢ ⓝV.T1 ➡* T2. -#G #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/ +#G #L #T1 #T2 #H @(cprs_ind … H) -T2 +/3 width=3 by cprs_strap1, cpr_cprs, cpr_tau/ qed. lemma cprs_beta_dx: ∀a,G,L,V1,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V2 → ⦃G, L⦄ ⊢ W1 ➡ W2 → ⦃G, L.ⓛW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ ⓐV1.ⓛ{a}W1.T1 ➡* ⓓ{a}ⓝW2.V2.T2. -#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 * -T2 /3 width=1/ -/4 width=7 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_beta/ (**) (* auto too slow without trace *) +#a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 * -T2 +/4 width=7 by cprs_strap1, cpr_cprs, cprs_bind_dx, cprs_flat_dx, cpr_beta/ qed. lemma cprs_theta_dx: ∀a,G,L,V1,V,V2,W1,W2,T1,T2. ⦃G, L⦄ ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → ⦃G, L.ⓓW1⦄ ⊢ T1 ➡* T2 → ⦃G, L⦄ ⊢ W1 ➡ W2 → ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2. -#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ] -/4 width=9 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_theta/ (**) (* auto too slow without trace *) +#a #G #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 +/4 width=9 by cprs_strap1, cpr_cprs, cprs_bind_dx, cprs_flat_dx, cpr_theta/ qed. (* Basic inversion lemmas ***************************************************) @@ -125,17 +123,17 @@ qed-. lemma cprs_inv_cast1: ∀G,L,W1,T1,U2. ⦃G, L⦄ ⊢ ⓝW1.T1 ➡* U2 → ⦃G, L⦄ ⊢ T1 ➡* U2 ∨ ∃∃W2,T2. ⦃G, L⦄ ⊢ W1 ➡* W2 & ⦃G, L⦄ ⊢ T1 ➡* T2 & U2 = ⓝW2.T2. #G #L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/ -#U2 #U #_ #HU2 * /3 width=3/ * +#U2 #U #_ #HU2 * /3 width=3 by cprs_strap1, or_introl/ * #W #T #HW1 #HT1 #H destruct -elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ * -#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/ +elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3 by cprs_strap1, or_introl/ * +#W2 #T2 #HW2 #HT2 #H destruct /4 width=5 by cprs_strap1, ex3_2_intro, or_intror/ qed-. (* Basic_1: was: nf2_pr3_unfold *) -lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → T = U. +lemma cprs_inv_cnr1: ∀G,L,T,U. ⦃G, L⦄ ⊢ T ➡* U → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → T = U. #G #L #T #U #H @(cprs_ind_dx … H) -T // #T0 #T #H1T0 #_ #IHT #H2T0 -lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/ +lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ qed-. (* Basic_1: removed theorems 13: diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma index 3d67c002c..e2975c54a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma @@ -19,7 +19,7 @@ include "basic_2/computation/csx.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL EVALUATION ON TERMS ******************) definition cpxe: ∀h. sd h → relation4 genv lenv term term ≝ - λh,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 ∧ ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T2⦄. + λh,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 ∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T2⦄. interpretation "context-sensitive extended parallel evaluation (term)" 'PEval h g G L T1 T2 = (cpxe h g G L T1 T2). @@ -28,8 +28,7 @@ interpretation "context-sensitive extended parallel evaluation (term)" lemma csx_cpxe: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 → ∃T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] 𝐍⦃T2⦄. #h #g #G #L #T1 #H @(csx_ind … H) -T1 -#T1 #_ #IHT1 -elim (cnx_dec h g G L T1) /3 width=3/ -* #T #H1T1 #H2T1 -elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/ +#T1 #_ #IHT1 elim (cnx_dec h g G L T1) /3 width=3 by ex_intro, conj/ +* #T #H1T1 #H2T1 elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 +#T2 * /4 width=3 by cpxs_strap2, ex_intro, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma index a3f8e8316..36ef1b2a1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma @@ -152,7 +152,7 @@ lapply (cpxs_strap1 … HW1 … HW2) -W lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/ qed-. -lemma cpxs_inv_cnx1: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → T = U. +lemma cpxs_inv_cnx1: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → T = U. #h #g #G #L #T #U #H @(cpxs_ind_dx … H) -T // #T0 #T #H1T0 #_ #IHT #H2T0 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1 by/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma deleted file mode 100644 index 2b4eadd6e..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma +++ /dev/null @@ -1,57 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/substitution/cpys_cpys.ma". -include "basic_2/reduction/cpx_cpys.ma". -include "basic_2/computation/cpxs_cpxs.ma". - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Main properties **********************************************************) - -axiom cpys_split_down: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 → - ∀i. d ≤ i → i ≤ d + e → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[i, d+e-i] T & ⦃G, L⦄ ⊢ T ▶*×[d, i-d] T2. - -lemma cpys_tpxs_trans: ∀h,g,G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T → - ∀T2. ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2. -#h #g #G #L #T1 #T #d #e #HT1 #T2 #H @(cpxs_ind … H) -T2 -/3 width=5 by cpxs_strap1, cpys_cpx, lsubr_cpx_trans, cpx_cpxs/ -qed-. - -lemma cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[0, ∞] T & ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2. -#h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 -[ /2 width=3 by ex2_intro/ -| /4 width=3 by cpx_cpxs, cpx_sort, ex2_intro/ -| #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 * #V #HV1 #HV2 - elim (lift_total V 0 (i+1)) #W #HVW - lapply (cpxs_lift … HV2 (⋆) (Ⓣ) … HVW … HVW2) - [ @ldrop_atom #H destruct | /3 width=7 by cpys_subst_Y2, ex2_intro/ ] -| #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 * #T #HT1 #HT2 - @(ex2_intro … (ⓑ{a,I}V1.T)) - [ @cpys_bind // - | @cpxs_bind // - - elim (cpys_split_down … HT1 1) -HT1 // #T0 #HT10 #HT0 - @(ex2_intro … (ⓑ{a,I}V.T0)) - [ @cpys_bind // - | @(cpxs_trans … (ⓑ{a,I}V.T)) @cpxs_bind // -HT10 - - -(* - lapply (lsuby_cpys_trans … HT10 (L.ⓑ{I}V) ?) -HT10 /2 width=1 by lsuby_succ/ #HT10 -*) -| #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 * - /3 width=5 by cpys_flat, cpxs_flat, ex2_intro/ \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma index ec36d47f1..eed76daea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma @@ -19,7 +19,7 @@ include "basic_2/computation/lpxs_cpxs.ma". (* Forward lemmas involving same top term constructor ***********************) -lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U. +lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≃ U. #h #g #G #L #T #HT #U #H >(cpxs_inv_cnx1 … H HT) -G -L -T // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma index 08cf4d2cd..41bd98df3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma @@ -21,7 +21,7 @@ include "basic_2/computation/cpxs_tstc.ma". (* Vector form of forward lemmas involving same top term constructor ********) (* Basic_1: was just: nf2_iso_appls_lref *) -lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → +lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≃ U. #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) #V #Vs #IHVs #U #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma index 6d55772c4..cd28a524b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma @@ -51,7 +51,7 @@ elim (eq_term_dec T1 T2) #HT12 destruct /3 width=4 by/ qed-. (* Basic_1: was just: sn3_nf2 *) -lemma cnx_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +lemma cnx_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] T. /2 width=1 by NF_to_SN/ qed. lemma csx_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ⬊*[h, g] ⋆k. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma index 21431dc3b..5e9ea06c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma @@ -22,7 +22,7 @@ include "basic_2/computation/csx_vector.ma". (* Advanced properties ******************************************************) (* Basic_1: was just: sn3_appls_lref *) -lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → +lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T. #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) #V #Vs #IHV #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index 730604ddb..a78d6c70d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -23,11 +23,25 @@ include "basic_2/computation/lpxs_cpxs.ma". fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z. // qed-. -fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶×[d, e] T1 → e = ∞ → +axiom cpxs_cpys_conf_lpxs: ∀h,g,G,d,e. + ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡*[h, g] T1 → + ∀T2. ⦃G, L0⦄ ⊢ T0 ▶*×[d, e] T2 → + ∀L1. ⦃G, L0⦄ ⊢ ➡*[h, g] L1 → + ∃∃T. ⦃G, L1⦄ ⊢ T1 ▶*×[d, e] T & ⦃G, L0⦄ ⊢ T2 ➡*[h, g] T. + +axiom cpxs_conf_lpxs_lpys: ∀h,g,G,d,e. + ∀I,L0,V0,T0,T1. ⦃G, L0.ⓑ{I}V0⦄ ⊢ T0 ➡*[h, g] T1 → + ∀L1. ⦃G, L0⦄ ⊢ ➡*[h, g] L1 → ∀V2. ⦃G, L0⦄ ⊢ V0 ▶*×[d, e] V2 → + ∃∃T. ⦃G, L1.ⓑ{I}V0⦄ ⊢ T1 ▶*×[⫯d, e] T & ⦃G, L0.ⓑ{I}V2⦄ ⊢ T0 ➡*[h, g] T. + + +include "basic_2/reduction/cpx_cpys.ma". + +fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶*×[d, e] T1 → e = ∞ → ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → - ∃∃T2. ⦃G, L2⦄ ⊢ T ▶×[d, e] T2 & ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & + ∃∃T2. ⦃G, L2⦄ ⊢ T ▶*×[d, e] T2 & ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & L1 ⋕[T, d] L2 ↔ T1 = T2. -#h #g #G #L1 #T #T1 #d #e #H elim H -G -L1 -T -T1 -d -e [ * ] +#h #g #G #L1 #T #T1 #d #e #H @(cpys_ind_alt … H) -G -L1 -T -T1 -d -e [ * ] [ /5 width=5 by lpxs_fwd_length, lleq_sort, ex3_intro, conj/ | #i #G #L1 elim (lt_or_ge i (|L1|)) [2: /6 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_aux, ex3_intro, conj/ ] #Hi #d elim (ylt_split i d) [ /5 width=5 by lpxs_fwd_length, lleq_skip, ex3_intro, conj/ ] @@ -36,19 +50,42 @@ fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶×[d, e] T1 → e = elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (lpxs_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct elim (lift_total V2 0 (i+1)) #W2 #HVW2 - @(ex3_intro … W2) /2 width=7 by cpxs_delta, cpy_subst/ -I -K1 -V1 -Hdi + @(ex3_intro … W2) /2 width=7 by cpxs_delta, cpys_subst/ -I -K1 -V1 -Hdi @conj #H [ elim HnL12 // | destruct elim (lift_inv_lref2_be … HVW2) // ] | /5 width=5 by lpxs_fwd_length, lleq_gref, ex3_intro, conj/ -| #I #G #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #He #L2 #HL12 destruct +| #I #G #L1 #K1 #V #V1 #T1 #i #d #e #Hdi #Hide #HLK1 #HV1 #HVT1 #_ #He #L2 #HL12 destruct elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (lpxs_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct + elim (lpxs_inv_pair1 … H) -H #K2 #W #HK12 #HVW #H destruct + elim (cpxs_cpys_conf_lpxs … HVW … HV1 … HK12) -HVW -HV1 -HK12 #W1 #HW1 #VW1 + elim (lift_total W1 0 (i+1)) #U1 #HWU1 lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1 - elim (lift_total V2 0 (i+1)) #W2 #HVW2 - @(ex3_intro … W2) /2 width=10 by cpxs_lift, cpy_subst/ + @(ex3_intro … U1) /2 width=10 by cpxs_lift, cpys_subst/ +| #a #I #G #L #V #V1 #T #T1 #d #e #HV1 #_ #IHV1 #IHT1 #He #L2 #HL12 + elim (IHV1 … HL12) // -IHV1 #V2 #HV2 #HV12 * #H1V #H2V + elim (IHT1 … (L2.ⓑ{I}V2)) /4 width=3 by lpxs_cpx_trans, lpxs_pair, cpys_cpx/ -IHT1 -He #T2 #HT2 #HT12 * #H1T #H2T + elim (cpxs_conf_lpxs_lpys … HT12 … HL12 … HV1) -HT12 -HL12 -HV1 #T0 #HT20 #HT10 + @(ex3_intro … (ⓑ{a,I}V2.T0)) + [ @cpys_bind // @(cpys_trans_eq … T2) /3 width=5 by lsuby_cpys_trans, lsuby_succ/ + | /2 width=1 by cpxs_bind/ + | @conj #H destruct + [ elim (lleq_inv_bind … H) -H #HV #HT >H1V -H1V // + | @lleq_bind /2 width=1/ + + + /3 width=5 by lsuby_cpys_trans, lsuby_succ/ +| #I #G #L #V #V1 #T #T1 #d #e #HV1 #HT1 #IHV1 #IHT1 #He #L2 #HL12 + elim (IHV1 … HL12) // -IHV1 #V2 #HV2 #HV12 * #H1V #H2V + elim (IHT1 … HL12) // -IHT1 #T2 #HT2 #HT12 * #H1T #H2T -He -HL12 + @(ex3_intro … (ⓕ{I}V2.T2)) /2 width=1 by cpxs_flat, cpys_flat/ + @conj #H destruct [2: /3 width=1 by lleq_flat/ ] + elim (lleq_inv_flat … H) -H /3 width=1 by eq_f2/ +] + - elim (lleq_dec (#i) L1 L2 d) - + [ + | @cpxs_bind // + @(lpx_cpxs_trans … HT12) | ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma index c720a11c0..e94aea008 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ 𝐍 break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ ➡ 𝐍 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Normal $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma index 56ae56448..20844ce63 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/normal_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ 𝐍 break [ term 46 h , break term 46 g ] break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐍 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Normal $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma index 627be72ac..4cebc3027 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ 𝐈 break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ ➡ 𝐈 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'NotReducible $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma index ad1d1187f..4a4e3f3a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/notreducible_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ 𝐈 break [ term 46 h , break term 46 g ] break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐈 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'NotReducible $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma index c8473ccc3..d1b688b8c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ 𝐑 break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ ➡ 𝐑 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Reducible $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma index ac8033449..c63231648 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/reducible_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ 𝐑 break [ term 46 h , break term 46 g ] break ⦃ term 46 T ⦄ )" +notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐑 break ⦃ term 46 T ⦄ )" non associative with precedence 45 for @{ 'Reducible $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma index 35a28700a..a8a5bcc9c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma @@ -17,39 +17,39 @@ include "basic_2/reduction/crr.ma". (* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************) -definition cir: relation3 genv lenv term ≝ λG,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⊥. +definition cir: relation3 genv lenv term ≝ λG,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⊥. interpretation "context-sensitive irreducibility (term)" 'NotReducible G L T = (cir G L T). (* Basic inversion lemmas ***************************************************) -lemma cir_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ 𝐈⦃#i⦄ → ⊥. +lemma cir_inv_delta: ∀G,L,K,V,i. ⇩[i] L ≡ K.ⓓV → ⦃G, L⦄ ⊢ ➡ 𝐈⦃#i⦄ → ⊥. /3 width=3 by crr_delta/ qed-. -lemma cir_inv_ri2: ∀I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈⦃②{I}V.T⦄ → ⊥. +lemma cir_inv_ri2: ∀I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ ➡ 𝐈⦃②{I}V.T⦄ → ⊥. /3 width=1 by crr_ri2/ qed-. -lemma cir_inv_ib2: ∀a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → - ⦃G, L⦄ ⊢ 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄. +lemma cir_inv_ib2: ∀a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓑ{a,I}V.T⦄ → + ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ➡ 𝐈⦃T⦄. /4 width=1 by crr_ib2_sn, crr_ib2_dx, conj/ qed-. -lemma cir_inv_bind: ∀a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ & ib2 a I. +lemma cir_inv_bind: ∀a,I,G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓑ{a,I}V.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ ➡ 𝐈⦃T⦄ & ib2 a I. #a * [ elim a -a ] #G #L #V #T #H [ elim H -H /3 width=1 by crr_ri2, or_introl/ ] elim (cir_inv_ib2 … H) -H /3 width=1 by and3_intro, or_introl/ qed-. -lemma cir_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄. +lemma cir_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓐV.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ & 𝐒⦃T⦄. #G #L #V #T #HVT @and3_intro /3 width=1/ generalize in match HVT; -HVT elim T -T // * // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crr_beta, crr_theta/ qed-. -lemma cir_inv_flat: ∀I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃ⓕ{I}V.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl. +lemma cir_inv_flat: ∀I,G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓕ{I}V.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl. * #G #L #V #T #H [ elim (cir_inv_appl … H) -H /2 width=1 by and4_intro/ | elim (cir_inv_ri2 … H) -H // @@ -58,22 +58,22 @@ qed-. (* Basic properties *********************************************************) -lemma cir_sort: ∀G,L,k. ⦃G, L⦄ ⊢ 𝐈⦃⋆k⦄. +lemma cir_sort: ∀G,L,k. ⦃G, L⦄ ⊢ ➡ 𝐈⦃⋆k⦄. /2 width=4 by crr_inv_sort/ qed. -lemma cir_gref: ∀G,L,p. ⦃G, L⦄ ⊢ 𝐈⦃§p⦄. +lemma cir_gref: ∀G,L,p. ⦃G, L⦄ ⊢ ➡ 𝐈⦃§p⦄. /2 width=4 by crr_inv_gref/ qed. -lemma tir_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ 𝐈⦃⓪{I}⦄. +lemma tir_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃⓪{I}⦄. /2 width=3 by trr_inv_atom/ qed. lemma cir_ib2: ∀a,I,G,L,V,T. - ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄. + ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓑ{a,I}V.T⦄. #a #I #G #L #V #T #HI #HV #HT #H elim (crr_inv_ib2 … HI H) -HI -H /2 width=1 by/ qed. -lemma cir_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐈⦃V⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃ⓐV.T⦄. +lemma cir_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓐV.T⦄. #G #L #V #T #HV #HT #H1 #H2 elim (crr_inv_appl … H2) -H2 /2 width=1 by/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma index bf68aedee..2f0461191 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma @@ -19,16 +19,16 @@ include "basic_2/reduction/cir.ma". (* Advanved properties ******************************************************) -lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ 𝐈⦃T⦄. +lemma cir_labst_last: ∀G,L,T,W. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐈⦃T⦄. /3 width=2 by crr_inv_labst_last/ qed. -lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ 𝐈⦃T⦄. +lemma cir_tif: ∀G,T,W. ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄. /3 width=2 by crr_inv_trr/ qed. (* Advanced inversion lemmas ************************************************) -lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄. +lemma cir_inv_append_sn: ∀G,L,K,T. ⦃G, K @@ L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄. /3 width=1/ qed-. -lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ 𝐈⦃T⦄. +lemma cir_inv_tir: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡ 𝐈⦃T⦄. /3 width=1/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma index 0c518239a..0cea0de9c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma @@ -19,10 +19,10 @@ include "basic_2/reduction/cir.ma". (* Properties on relocation *************************************************) -lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐈⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K → - ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐈⦃U⦄. +lemma cir_lift: ∀G,K,T. ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K → + ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄. /3 width=8 by crr_inv_lift/ qed. -lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐈⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → - ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐈⦃T⦄. +lemma cir_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ ➡ 𝐈⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡ 𝐈⦃T⦄. /3 width=8 by crr_lift/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma index d7da41971..ad3c60831 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma @@ -19,42 +19,42 @@ include "basic_2/reduction/crx.ma". (* CONTEXT-SENSITIVE EXTENDED IRREDUCIBLE TERMS *****************************) definition cix: ∀h. sd h → relation3 genv lenv term ≝ - λh,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⊥. + λh,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⊥. interpretation "context-sensitive extended irreducibility (term)" 'NotReducible h g G L T = (cix h g G L T). (* Basic inversion lemmas ***************************************************) -lemma cix_inv_sort: ∀h,g,G,L,k,l. deg h g k (l+1) → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄ → ⊥. +lemma cix_inv_sort: ∀h,g,G,L,k,l. deg h g k (l+1) → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃⋆k⦄ → ⊥. /3 width=2 by crx_sort/ qed-. -lemma cix_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃#i⦄ → ⊥. +lemma cix_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃#i⦄ → ⊥. /3 width=4 by crx_delta/ qed-. -lemma cix_inv_ri2: ∀h,g,I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃②{I}V.T⦄ → ⊥. +lemma cix_inv_ri2: ∀h,g,I,G,L,V,T. ri2 I → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃②{I}V.T⦄ → ⊥. /3 width=1 by crx_ri2/ qed-. -lemma cix_inv_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ → - ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄. +lemma cix_inv_ib2: ∀h,g,a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓑ{a,I}V.T⦄ → + ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ➡[h, g] 𝐈⦃T⦄. /4 width=1 by crx_ib2_sn, crx_ib2_dx, conj/ qed-. -lemma cix_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ & ib2 a I. +lemma cix_inv_bind: ∀h,g,a,I,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓑ{a,I}V.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ & ⦃G, L.ⓑ{I}V⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ & ib2 a I. #h #g #a * [ elim a -a ] #G #L #V #T #H [ elim H -H /3 width=1 by crx_ri2, or_introl/ ] elim (cix_inv_ib2 … H) -H /3 width=1 by and3_intro, or_introl/ qed-. -lemma cix_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓐV.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄. -#h #g #G #L #V #T #HVT @and3_intro /3 width=1/ +lemma cix_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓐV.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ & 𝐒⦃T⦄. +#h #g #G #L #V #T #HVT @and3_intro /3 width=1 by crx_appl_sn, crx_appl_dx/ generalize in match HVT; -HVT elim T -T // * // #a * #U #T #_ #_ #H elim H -H /2 width=1 by crx_beta, crx_theta/ qed-. -lemma cix_inv_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓕ{I}V.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ & 𝐒⦃T⦄ & I = Appl. +lemma cix_inv_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃ⓕ{I}V.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ & 𝐒⦃T⦄ & I = Appl. #h #g * #G #L #V #T #H [ elim (cix_inv_appl … H) -H /2 width=1 by and4_intro/ | elim (cix_inv_ri2 … H) -H // @@ -63,31 +63,31 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma cix_inv_cir: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄. +lemma cix_inv_cir: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄. /3 width=1 by crr_crx/ qed-. (* Basic properties *********************************************************) -lemma cix_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃⋆k⦄. +lemma cix_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃⋆k⦄. #h #g #G #L #k #Hk #H elim (crx_inv_sort … H) -L #l #Hkl lapply (deg_mono … Hk Hkl) -h -k (cpr_inv_sort1 … H) // qed. (* Basic_1: was: nf2_abst *) -lemma cnr_abst: ∀a,G,L,W,T. ⦃G, L⦄ ⊢ 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃ⓛ{a}W.T⦄. +lemma cnr_abst: ∀a,G,L,W,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓛ{a}W.T⦄. #a #G #L #W #T #HW #HT #X #H elim (cpr_inv_abst1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct >(HW … HW0) -W0 >(HT … HT0) -T0 // qed. (* Basic_1: was only: nf2_appl_lref *) -lemma cnr_appl_simple: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃ⓐV.T⦄. +lemma cnr_appl_simple: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃ⓐV.T⦄. #G #L #V #T #HV #HT #HS #X #H elim (cpr_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct >(HV … HV0) -V0 >(HT … HT0) -T0 // qed. (* Basic_1: was: nf2_dec *) -axiom cnr_dec: ∀G,L,T1. ⦃G, L⦄ ⊢ 𝐍⦃T1⦄ ∨ +axiom cnr_dec: ∀G,L,T1. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T1⦄ ∨ ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡ T2 & (T1 = T2 → ⊥). (* Basic_1: removed theorems 1: nf2_abst_shift *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma index 487fd68bb..7c596245f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_cir.ma @@ -19,10 +19,10 @@ include "basic_2/reduction/cnr_crr.ma". (* Main properties on context-sensitive irreducible terms *******************) -theorem cir_cnr: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄. +theorem cir_cnr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄. /2 width=4 by cpr_fwd_cir/ qed. (* Main inversion lemmas on context-sensitive irreducible terms *************) -theorem cnr_inv_cir: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈⦃T⦄. +theorem cnr_inv_cir: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T⦄. /2 width=5 by cnr_inv_crr/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma index 7ee9e1f29..c72c3315e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_crr.ma @@ -20,7 +20,7 @@ include "basic_2/reduction/cnr.ma". (* Advanced inversion lemmas on context-sensitive reducible terms ***********) (* Note: this property is unusual *) -lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → ⊥. +lemma cnr_inv_crr: ∀G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → ⊥. #G #L #T #H elim H -L -T [ #L #K #V #i #HLK #H elim (cnr_inv_delta … HLK H) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma index 9f29fe9a8..48fa090bd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma @@ -20,7 +20,7 @@ include "basic_2/reduction/cnr.ma". (* Advanced properties ******************************************************) (* Basic_1: was only: nf2_csort_lref *) -lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄. +lemma cnr_lref_atom: ∀G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄. #G #L #i #HL #X #H elim (cpr_inv_lref1 … H) -H // * #K #V1 #V2 #HLK #_ #_ @@ -28,7 +28,7 @@ lapply (ldrop_mono … HL … HLK) -L #H destruct qed. (* Basic_1: was: nf2_lref_abst *) -lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ 𝐍⦃#i⦄. +lemma cnr_lref_abst: ∀G,L,K,V,i. ⇩[i] L ≡ K. ⓛV → ⦃G, L⦄ ⊢ ➡ 𝐍⦃#i⦄. #G #L #K #V #i #HLK #X #H elim (cpr_inv_lref1 … H) -H // * #K0 #V1 #V2 #HLK0 #_ #_ @@ -38,8 +38,8 @@ qed. (* Relocation properties ****************************************************) (* Basic_1: was: nf2_lift *) -lemma cnr_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ 𝐍⦃T⦄ → - ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄. +lemma cnr_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄ → + ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡ 𝐍⦃T0⦄. #G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 <(HLT … HT1) in HT0; -L #HT0 @@ -47,8 +47,8 @@ elim (cpr_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 qed. (* Note: this was missing in basic_1 *) -lemma cnr_inv_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ 𝐍⦃T0⦄ → - ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍⦃T⦄. +lemma cnr_inv_lift: ∀G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ ➡ 𝐍⦃T0⦄ → + ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄. #G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H elim (lift_total X d e) #X0 #HX0 lapply (cpr_lift … H … HL0 … HT0 … HX0) -L #HTX0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma index d423f119e..61e6e6cc6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma @@ -27,37 +27,37 @@ interpretation (* Basic inversion lemmas ***************************************************) -lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄ → deg h g k 0. +lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄ → deg h g k 0. #h #g #G #L #k #H elim (deg_total h g k) #l @(nat_ind_plus … l) -l // #l #_ #Hkl lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_sort/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *) lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H) qed-. -lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄ → ⊥. +lemma cnx_inv_delta: ∀h,g,I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄ → ⊥. #h #g #I #G #L #K #V #i #HLK #H elim (lift_total V 0 (i+1)) #W #HVW lapply (H W ?) -H [ /3 width=7 by cpx_delta/ ] -HLK #H destruct elim (lift_inv_lref2_be … HVW) -HVW // qed-. -lemma cnx_inv_abst: ∀h,g,a,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓛ{a}V.T⦄ → - ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ 𝐍[h, g]⦃T⦄. +lemma cnx_inv_abst: ∀h,g,a,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓛ{a}V.T⦄ → + ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃V⦄ ∧ ⦃G, L.ⓛV⦄ ⊢ ➡[h, g] 𝐍⦃T⦄. #h #g #a #G #L #V1 #T1 #HVT1 @conj [ #V2 #HV2 lapply (HVT1 (ⓛ{a}V2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct // | #T2 #HT2 lapply (HVT1 (ⓛ{a}V1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct // ] qed-. -lemma cnx_inv_abbr: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃-ⓓV.T⦄ → - ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ 𝐍[h, g]⦃T⦄. +lemma cnx_inv_abbr: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃-ⓓV.T⦄ → + ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃V⦄ ∧ ⦃G, L.ⓓV⦄ ⊢ ➡[h, g] 𝐍⦃T⦄. #h #g #G #L #V1 #T1 #HVT1 @conj [ #V2 #HV2 lapply (HVT1 (-ⓓV2.T1) ?) -HVT1 /2 width=2 by cpx_pair_sn/ -HV2 #H destruct // | #T2 #HT2 lapply (HVT1 (-ⓓV1.T2) ?) -HVT1 /2 width=2 by cpx_bind/ -HT2 #H destruct // ] qed-. -lemma cnx_inv_zeta: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃+ⓓV.T⦄ → ⊥. +lemma cnx_inv_zeta: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃+ⓓV.T⦄ → ⊥. #h #g #G #L #V #T #H elim (is_lift_dec T 0 1) [ * #U #HTU lapply (H U ?) -H /2 width=3 by cpx_zeta/ #H destruct @@ -69,56 +69,56 @@ lemma cnx_inv_zeta: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃+ⓓV.T⦄ → ] qed-. -lemma cnx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄ → - ∧∧ ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ & ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ & 𝐒⦃T⦄. +lemma cnx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓐV.T⦄ → + ∧∧ ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃V⦄ & ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ & 𝐒⦃T⦄. #h #g #G #L #V1 #T1 #HVT1 @and3_intro -[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct // -| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct // +[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1 by cpx_pair_sn/ -HV2 #H destruct // +| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1 by cpx_flat/ -HT2 #H destruct // | generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H [ elim (lift_total V1 0 1) #V2 #HV12 - lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct - | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1/ #H destruct + lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3 by cpr_cpx, cpr_theta/ -HV12 #H destruct + | lapply (H (ⓓ{a}ⓝW1.V1.U1) ?) -H /3 width=1 by cpr_cpx, cpr_beta/ #H destruct ] ] qed-. -lemma cnx_inv_tau: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓝV.T⦄ → ⊥. +lemma cnx_inv_tau: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓝV.T⦄ → ⊥. #h #g #G #L #V #T #H lapply (H T ?) -H /2 width=4 by cpx_tau, discr_tpair_xy_y/ qed-. (* Basic forward lemmas *****************************************************) -lemma cnx_fwd_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍⦃T⦄. +lemma cnx_fwd_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐍⦃T⦄. #h #g #G #L #T #H #U #HTU @H /2 width=1 by cpr_cpx/ (**) (* auto fails because a δ-expansion gets in the way *) qed-. (* Basic properties *********************************************************) -lemma cnx_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆k⦄. +lemma cnx_sort: ∀h,g,G,L,k. deg h g k 0 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄. #h #g #G #L #k #Hk #X #H elim (cpx_inv_sort1 … H) -H // * #l #Hkl #_ lapply (deg_mono … Hkl Hk) -h -L (HW … HW0) -W0 >(HT … HT0) -T0 // qed. -lemma cnx_appl_simple: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃V⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → 𝐒⦃T⦄ → - ⦃G, L⦄ ⊢ 𝐍[h, g]⦃ⓐV.T⦄. +lemma cnx_appl_simple: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃V⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → 𝐒⦃T⦄ → + ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓐV.T⦄. #h #g #G #L #V #T #HV #HT #HS #X #H elim (cpx_inv_appl1_simple … H) -H // #V0 #T0 #HV0 #HT0 #H destruct >(HV … HV0) -V0 >(HT … HT0) -T0 // qed. -axiom cnx_dec: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T1⦄ ∨ +axiom cnx_dec: ∀h,g,G,L,T1. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T1⦄ ∨ ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 & (T1 = T2 → ⊥). diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma index 3e62a5c60..18dc60e3e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_cix.ma @@ -19,10 +19,10 @@ include "basic_2/reduction/cnx_crx.ma". (* Main properties on context-sensitive extended irreducible terms **********) -theorem cix_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄. +theorem cix_cnr: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄. /2 width=6 by cpx_fwd_cix/ qed. (* Main inversion lemmas on context-sensitive extended irreducible terms ****) -theorem cnr_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T⦄. +theorem cnr_inv_cix: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T⦄. /2 width=7 by cnx_inv_crx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma index ec9abbd33..c6d51c630 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma @@ -20,7 +20,7 @@ include "basic_2/reduction/cnx.ma". (* Advanced inversion lemmas on context-sensitive reducible terms ***********) (* Note: this property is unusual *) -lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⊥. +lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⊥. #h #g #G #L #T #H elim H -L -T [ #L #k #l #Hkl #H lapply (cnx_inv_sort … H) -H #H @@ -28,16 +28,16 @@ lemma cnx_inv_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ | #I #L #K #V #i #HLK #H elim (cnx_inv_delta … HLK H) | #L #V #T #_ #IHV #H - elim (cnx_inv_appl … H) -H /2 width=1/ + elim (cnx_inv_appl … H) -H /2 width=1 by/ | #L #V #T #_ #IHT #H - elim (cnx_inv_appl … H) -H /2 width=1/ + elim (cnx_inv_appl … H) -H /2 width=1 by/ | #I #L #V #T * #H1 #H2 destruct [ elim (cnx_inv_zeta … H2) | elim (cnx_inv_tau … H2) ] |6,7: #a * [ elim a ] #L #V #T * #H1 #_ #IH #H2 destruct - [1,3: elim (cnx_inv_abbr … H2) -H2 /2 width=1/ - |*: elim (cnx_inv_abst … H2) -H2 /2 width=1/ + [1,3: elim (cnx_inv_abbr … H2) -H2 /2 width=1 by/ + |*: elim (cnx_inv_abst … H2) -H2 /2 width=1 by/ ] | #a #L #V #W #T #H elim (cnx_inv_appl … H) -H #_ #_ #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma index f52149d5b..65c035f4a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma @@ -19,7 +19,7 @@ include "basic_2/reduction/cnx.ma". (* Advanced properties ******************************************************) -lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃#i⦄. +lemma cnx_lref_atom: ∀h,g,G,L,i. ⇩[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃#i⦄. #h #g #G #L #i #HL #X #H elim (cpx_inv_lref1 … H) -H // * #I #K #V1 #V2 #HLK #_ #_ @@ -28,16 +28,16 @@ qed. (* Relocation properties ****************************************************) -lemma cnx_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄ → ⇩[s, d, e] L0 ≡ L → - ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄. +lemma cnx_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ⇩[s, d, e] L0 ≡ L → + ⇧[d, e] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡[h, g] 𝐍⦃T0⦄. #h #g #G #L0 #L #T #T0 #s #d #e #HLT #HL0 #HT0 #X #H elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 <(HLT … HT1) in HT0; -L #HT0 >(lift_mono … HT10 … HT0) -T1 -X // qed. -lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ 𝐍[h, g]⦃T0⦄ → ⇩[s, d, e] L0 ≡ L → - ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃T⦄. +lemma cnx_inv_lift: ∀h,g,G,L0,L,T,T0,s,d,e. ⦃G, L0⦄ ⊢ ➡[h, g] 𝐍⦃T0⦄ → ⇩[s, d, e] L0 ≡ L → + ⇧[d, e] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄. #h #g #G #L0 #L #T #T0 #s #d #e #HLT0 #HL0 #HT0 #X #H elim (lift_total X d e) #X0 #HX0 lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma index 5cee2e207..d0e1e19ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_cir.ma @@ -19,7 +19,7 @@ include "basic_2/reduction/cpr.ma". (* Advanced forward lemmas on context-sensitive irreducible terms ***********) -lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ 𝐈⦃T1⦄ → T2 = T1. +lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ ➡ 𝐈⦃T1⦄ → T2 = T1. #G #L #T1 #T2 #H elim H -G -L -T1 -T2 [ // | #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H @@ -28,15 +28,15 @@ lemma cpr_fwd_cir: ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → ⦃G, L⦄ ⊢ [ elim (cir_inv_bind … H) -H #HV1 #HT1 * #H destruct lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct lapply (IHT1 … HT1) -IHT1 #H destruct // - | elim (cir_inv_ib2 … H) -H /2 width=1/ /3 width=2/ + | elim (cir_inv_ib2 … H) -H /3 width=2 by or_introl, eq_f2/ ] | * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H [ elim (cir_inv_appl … H) -H #HV1 #HT1 #_ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // - | elim (cir_inv_ri2 … H) /2 width=1/ + | elim (cir_inv_ri2 … H) /2 width=1 by/ ] | #G #L #V1 #T1 #T #T2 #_ #_ #_ #H - elim (cir_inv_ri2 … H) /2 width=1/ + elim (cir_inv_ri2 … H) /2 width=1 by or_introl/ | #G #L #V1 #T1 #T2 #_ #_ #H elim (cir_inv_ri2 … H) /2 width=1/ | #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma index 196cdadb0..ce54e9a7e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma @@ -19,7 +19,7 @@ include "basic_2/reduction/cpx.ma". (* Advanced forward lemmas on context-sensitive extended irreducible terms **) -lemma cpx_fwd_cix: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ 𝐈[h, g]⦃T1⦄ → T2 = T1. +lemma cpx_fwd_cix: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L⦄ ⊢ ➡[h, g] 𝐈⦃T1⦄ → T2 = T1. #h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2 [ // | #G #L #k #l #Hkl #H elim (cix_inv_sort … Hkl H) @@ -29,19 +29,19 @@ lemma cpx_fwd_cix: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ⦃G, L [ elim (cix_inv_bind … H) -H #HV1 #HT1 * #H destruct lapply (IHV1 … HV1) -IHV1 -HV1 #H destruct lapply (IHT1 … HT1) -IHT1 #H destruct // - | elim (cix_inv_ib2 … H) -H /2 width=1/ /3 width=2/ + | elim (cix_inv_ib2 … H) -H /3 width=2 by or_introl, eq_f2/ ] | * #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV1 #IHT1 #H [ elim (cix_inv_appl … H) -H #HV1 #HT1 #_ >IHV1 -IHV1 // -HV1 >IHT1 -IHT1 // - | elim (cix_inv_ri2 … H) /2 width=1/ + | elim (cix_inv_ri2 … H) /2 width=1 by/ ] | #G #L #V1 #T1 #T #T2 #_ #_ #_ #H - elim (cix_inv_ri2 … H) /2 width=1/ + elim (cix_inv_ri2 … H) /2 width=1 by or_introl/ | #G #L #V1 #T1 #T2 #_ #_ #H - elim (cix_inv_ri2 … H) /2 width=1/ + elim (cix_inv_ri2 … H) /2 width=1 by/ | #G #L #V1 #V2 #T #_ #_ #H - elim (cix_inv_ri2 … H) /2 width=1/ + elim (cix_inv_ri2 … H) /2 width=1 by/ | #a #G #L #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #H elim (cix_inv_appl … H) -H #_ #_ #H elim (simple_inv_bind … H) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma index 79d9269b3..02aaa8209 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma @@ -45,7 +45,7 @@ interpretation (* Basic inversion lemmas ***************************************************) -fact crr_inv_sort_aux: ∀G,L,T,k. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = ⋆k → ⊥. +fact crr_inv_sort_aux: ∀G,L,T,k. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = ⋆k → ⊥. #G #L #T #k0 * -L -T [ #L #K #V #i #HLK #H destruct | #L #V #T #_ #H destruct @@ -58,10 +58,10 @@ fact crr_inv_sort_aux: ∀G,L,T,k. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = ⋆k → ] qed-. -lemma crr_inv_sort: ∀G,L,k. ⦃G, L⦄ ⊢ 𝐑⦃⋆k⦄ → ⊥. +lemma crr_inv_sort: ∀G,L,k. ⦃G, L⦄ ⊢ ➡ 𝐑⦃⋆k⦄ → ⊥. /2 width=6 by crr_inv_sort_aux/ qed-. -fact crr_inv_lref_aux: ∀G,L,T,i. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = #i → +fact crr_inv_lref_aux: ∀G,L,T,i. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = #i → ∃∃K,V. ⇩[i] L ≡ K.ⓓV. #G #L #T #j * -L -T [ #L #K #V #i #HLK #H destruct /2 width=3 by ex1_2_intro/ @@ -75,10 +75,10 @@ fact crr_inv_lref_aux: ∀G,L,T,i. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = #i → ] qed-. -lemma crr_inv_lref: ∀G,L,i. ⦃G, L⦄ ⊢ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[i] L ≡ K.ⓓV. +lemma crr_inv_lref: ∀G,L,i. ⦃G, L⦄ ⊢ ➡ 𝐑⦃#i⦄ → ∃∃K,V. ⇩[i] L ≡ K.ⓓV. /2 width=4 by crr_inv_lref_aux/ qed-. -fact crr_inv_gref_aux: ∀G,L,T,p. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = §p → ⊥. +fact crr_inv_gref_aux: ∀G,L,T,p. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = §p → ⊥. #G #L #T #q * -L -T [ #L #K #V #i #HLK #H destruct | #L #V #T #_ #H destruct @@ -91,10 +91,10 @@ fact crr_inv_gref_aux: ∀G,L,T,p. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = §p → ] qed-. -lemma crr_inv_gref: ∀G,L,p. ⦃G, L⦄ ⊢ 𝐑⦃§p⦄ → ⊥. +lemma crr_inv_gref: ∀G,L,p. ⦃G, L⦄ ⊢ ➡ 𝐑⦃§p⦄ → ⊥. /2 width=6 by crr_inv_gref_aux/ qed-. -lemma trr_inv_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ 𝐑⦃⓪{I}⦄ → ⊥. +lemma trr_inv_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃⓪{I}⦄ → ⊥. #G * #i #H [ elim (crr_inv_sort … H) | elim (crr_inv_lref … H) -H #L #V #H @@ -103,8 +103,8 @@ lemma trr_inv_atom: ∀G,I. ⦃G, ⋆⦄ ⊢ 𝐑⦃⓪{I}⦄ → ⊥. ] qed-. -fact crr_inv_ib2_aux: ∀a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = ⓑ{a,I}W.U → - ⦃G, L⦄ ⊢ 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑⦃U⦄. +fact crr_inv_ib2_aux: ∀a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = ⓑ{a,I}W.U → + ⦃G, L⦄ ⊢ ➡ 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ ➡ 𝐑⦃U⦄. #G #b #J #L #W0 #U #T #HI * -L -T [ #L #K #V #i #_ #H destruct | #L #V #T #_ #H destruct @@ -119,12 +119,12 @@ fact crr_inv_ib2_aux: ∀a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑⦃T⦄ ] qed-. -lemma crr_inv_ib2: ∀a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑⦃ⓑ{a,I}W.T⦄ → - ⦃G, L⦄ ⊢ 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑⦃T⦄. +lemma crr_inv_ib2: ∀a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐑⦃ⓑ{a,I}W.T⦄ → + ⦃G, L⦄ ⊢ ➡ 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ ➡ 𝐑⦃T⦄. /2 width=5 by crr_inv_ib2_aux/ qed-. -fact crr_inv_appl_aux: ∀G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = ⓐW.U → - ∨∨ ⦃G, L⦄ ⊢ 𝐑⦃W⦄ | ⦃G, L⦄ ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥). +fact crr_inv_appl_aux: ∀G,L,W,U,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → T = ⓐW.U → + ∨∨ ⦃G, L⦄ ⊢ ➡ 𝐑⦃W⦄ | ⦃G, L⦄ ⊢ ➡ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥). #G #L #W0 #U #T * -L -T [ #L #K #V #i #_ #H destruct | #L #V #T #HV #H destruct /2 width=1 by or3_intro0/ @@ -140,6 +140,6 @@ fact crr_inv_appl_aux: ∀G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → T = ⓐW.U ] qed-. -lemma crr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ 𝐑⦃ⓐV.T⦄ → - ∨∨ ⦃G, L⦄ ⊢ 𝐑⦃V⦄ | ⦃G, L⦄ ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥). +lemma crr_inv_appl: ∀G,L,V,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃ⓐV.T⦄ → + ∨∨ ⦃G, L⦄ ⊢ ➡ 𝐑⦃V⦄ | ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥). /2 width=3 by crr_inv_appl_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma index 36cf60341..8b4cfb336 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_append.ma @@ -19,21 +19,21 @@ include "basic_2/reduction/crr.ma". (* Advanved properties ******************************************************) -lemma crr_append_sn: ∀G,L,K,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ 𝐑⦃T⦄. +lemma crr_append_sn: ∀G,L,K,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡ 𝐑⦃T⦄. #G #L #K0 #T #H elim H -L -T /2 width=1/ #L #K #V #i #HLK lapply (ldrop_fwd_length_lt2 … HLK) #Hi lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=3/ qed. -lemma trr_crr: ∀G,L,T. ⦃G, ⋆⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑⦃T⦄. +lemma trr_crr: ∀G,L,T. ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄. #G #L #T #H lapply (crr_append_sn … H) // qed. (* Advanced inversion lemmas ************************************************) -fact crr_inv_labst_last_aux: ∀G,L1,T,W. ⦃G, L1⦄ ⊢ 𝐑⦃T⦄ → - ∀L2. L1 = ⋆.ⓛW @@ L2 → ⦃G, L2⦄ ⊢ 𝐑⦃T⦄. +fact crr_inv_labst_last_aux: ∀G,L1,T,W. ⦃G, L1⦄ ⊢ ➡ 𝐑⦃T⦄ → + ∀L2. L1 = ⋆.ⓛW @@ L2 → ⦃G, L2⦄ ⊢ ➡ 𝐑⦃T⦄. #G #L1 #T #W #H elim H -L1 -T /2 width=1/ /3 width=1/ [ #L1 #K1 #V1 #i #HLK1 #L2 #H destruct lapply (ldrop_fwd_length_lt2 … HLK1) @@ -49,8 +49,8 @@ fact crr_inv_labst_last_aux: ∀G,L1,T,W. ⦃G, L1⦄ ⊢ 𝐑⦃T⦄ → ] qed. -lemma crr_inv_labst_last: ∀G,L,T,W. ⦃G, ⋆.ⓛW @@ L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑⦃T⦄. +lemma crr_inv_labst_last: ∀G,L,T,W. ⦃G, ⋆.ⓛW @@ L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄. /2 width=4/ qed-. -lemma crr_inv_trr: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ 𝐑⦃T⦄ → ⦃G, ⋆⦄ ⊢ 𝐑⦃T⦄. +lemma crr_inv_trr: ∀G,T,W. ⦃G, ⋆.ⓛW⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, ⋆⦄ ⊢ ➡ 𝐑⦃T⦄. /2 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma index 4b28fc1dc..41f626cee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma @@ -19,8 +19,8 @@ include "basic_2/reduction/crr.ma". (* Properties on relocation *************************************************) -lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K → - ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑⦃U⦄. +lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ ➡ 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K → + ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡ 𝐑⦃U⦄. #G #K #T #H elim H -K -T [ #K #K0 #V #i #HK0 #L #s #d #e #HLK #X #H elim (lift_inv_lref1 … H) -H * #Hid #H destruct @@ -46,8 +46,8 @@ lemma crr_lift: ∀G,K,T. ⦃G, K⦄ ⊢ 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e ] qed. -lemma crr_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ 𝐑⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → - ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑⦃T⦄. +lemma crr_inv_lift: ∀G,L,U. ⦃G, L⦄ ⊢ ➡ 𝐑⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡ 𝐑⦃T⦄. #G #L #U #H elim H -L -U [ #L #L0 #W #i #HK0 #K #s #d #e #HLK #X #H elim (lift_inv_lref2 … H) -H * #Hid #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma index 8c26803ad..86796ae0b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma @@ -38,14 +38,14 @@ interpretation (* Basic properties *********************************************************) -lemma crr_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄. +lemma crr_crx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡ 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄. #h #g #G #L #T #H elim H -L -T /2 width=4 by crx_delta, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/ qed. (* Basic inversion lemmas ***************************************************) -fact crx_inv_sort_aux: ∀h,g,G,L,T,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⋆k → +fact crx_inv_sort_aux: ∀h,g,G,L,T,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → T = ⋆k → ∃l. deg h g k (l+1). #h #g #G #L #T #k0 * -L -T [ #L #k #l #Hkl #H destruct /2 width=2 by ex_intro/ @@ -60,10 +60,10 @@ fact crx_inv_sort_aux: ∀h,g,G,L,T,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ] qed-. -lemma crx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃⋆k⦄ → ∃l. deg h g k (l+1). +lemma crx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃⋆k⦄ → ∃l. deg h g k (l+1). /2 width=5 by crx_inv_sort_aux/ qed-. -fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = #i → +fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → T = #i → ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V. #h #g #G #L #T #j * -L -T [ #L #k #l #_ #H destruct @@ -78,10 +78,10 @@ fact crx_inv_lref_aux: ∀h,g,G,L,T,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ] qed-. -lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃#i⦄ → ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V. +lemma crx_inv_lref: ∀h,g,G,L,i. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃#i⦄ → ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I}V. /2 width=6 by crx_inv_lref_aux/ qed-. -fact crx_inv_gref_aux: ∀h,g,G,L,T,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = §p → ⊥. +fact crx_inv_gref_aux: ∀h,g,G,L,T,p. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → T = §p → ⊥. #h #g #G #L #T #q * -L -T [ #L #k #l #_ #H destruct | #I #L #K #V #i #HLK #H destruct @@ -95,10 +95,10 @@ fact crx_inv_gref_aux: ∀h,g,G,L,T,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ] qed-. -lemma crx_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃§p⦄ → ⊥. +lemma crx_inv_gref: ∀h,g,G,L,p. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃§p⦄ → ⊥. /2 width=8 by crx_inv_gref_aux/ qed-. -lemma trx_inv_atom: ∀h,g,I,G. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃⓪{I}⦄ → +lemma trx_inv_atom: ∀h,g,I,G. ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐑⦃⓪{I}⦄ → ∃∃k,l. deg h g k (l+1) & I = Sort k. #h #g * #i #G #H [ elim (crx_inv_sort … H) -H /2 width=4 by ex2_2_intro/ @@ -108,8 +108,8 @@ lemma trx_inv_atom: ∀h,g,I,G. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃⓪{I}⦄ → ] qed-. -fact crx_inv_ib2_aux: ∀h,g,a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → - T = ⓑ{a,I}W.U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃U⦄. +fact crx_inv_ib2_aux: ∀h,g,a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → + T = ⓑ{a,I}W.U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ ➡[h, g] 𝐑⦃U⦄. #h #g #b #J #G #L #W0 #U #T #HI * -L -T [ #L #k #l #_ #H destruct | #I #L #K #V #i #_ #H destruct @@ -125,12 +125,12 @@ fact crx_inv_ib2_aux: ∀h,g,a,I,G,L,W,U,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g ] qed-. -lemma crx_inv_ib2: ∀h,g,a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓑ{a,I}W.T⦄ → - ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ 𝐑[h, g]⦃T⦄. +lemma crx_inv_ib2: ∀h,g,a,I,G,L,W,T. ib2 a I → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃ⓑ{a,I}W.T⦄ → + ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃W⦄ ∨ ⦃G, L.ⓑ{I}W⦄ ⊢ ➡[h, g] 𝐑⦃T⦄. /2 width=5 by crx_inv_ib2_aux/ qed-. -fact crx_inv_appl_aux: ∀h,g,G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T = ⓐW.U → - ∨∨ ⦃G, L⦄ ⊢ 𝐑[h, g]⦃W⦄ | ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ | (𝐒⦃U⦄ → ⊥). +fact crx_inv_appl_aux: ∀h,g,G,L,W,U,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → T = ⓐW.U → + ∨∨ ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃W⦄ | ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥). #h #g #G #L #W0 #U #T * -L -T [ #L #k #l #_ #H destruct | #I #L #K #V #i #_ #H destruct @@ -147,6 +147,6 @@ fact crx_inv_appl_aux: ∀h,g,G,L,W,U,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → T ] qed-. -lemma crx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃ⓐV.T⦄ → - ∨∨ ⦃G, L⦄ ⊢ 𝐑[h, g]⦃V⦄ | ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ | (𝐒⦃T⦄ → ⊥). +lemma crx_inv_appl: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃ⓐV.T⦄ → + ∨∨ ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃V⦄ | ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥). /2 width=3 by crx_inv_appl_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma index 8f5286c54..ca86ad11e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_append.ma @@ -19,13 +19,14 @@ include "basic_2/reduction/crx.ma". (* Advanved properties ******************************************************) -lemma crx_append_sn: ∀h,g,G,L,K,T. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, K @@ L⦄ ⊢ 𝐑[h, g]⦃T⦄. -#h #g #G #L #K0 #T #H elim H -L -T /2 width=1/ /2 width=2/ +lemma crx_append_sn: ∀h,g,G,L,K,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, K @@ L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄. +#h #g #G #L #K0 #T #H elim H -L -T +/2 width=2 by crx_sort, crx_appl_sn, crx_appl_dx, crx_ri2, crx_ib2_sn, crx_ib2_dx, crx_beta, crx_theta/ #I #L #K #V #i #HLK lapply (ldrop_fwd_length_lt2 … HLK) #Hi -lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=2/ -Hi /2 width=4/ +lapply (ldrop_O1_append_sn_le … HLK … K0) -HLK /2 width=4 by crx_delta, lt_to_le/ qed. -lemma trx_crx: ∀h,g,G,L,T. ⦃G, ⋆⦄ ⊢ 𝐑[h, g]⦃T⦄ → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃T⦄. +lemma trx_crx: ∀h,g,G,L,T. ⦃G, ⋆⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃T⦄. #h #g #G #L #T #H lapply (crx_append_sn … H) // qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma index 9e1bc9f81..9c268927a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma @@ -19,8 +19,8 @@ include "basic_2/reduction/crx.ma". (* Properties on relocation *************************************************) -lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K → - ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄. +lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄ → ∀L,s,d,e. ⇩[s, d, e] L ≡ K → + ∀U. ⇧[d, e] T ≡ U → ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄. #h #g #G #K #T #H elim H -K -T [ #K #k #l #Hkl #L #s #d #e #_ #X #H >(lift_inv_sort1 … H) -X /2 width=2 by crx_sort/ @@ -48,8 +48,8 @@ lemma crx_lift: ∀h,g,G,K,T. ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄ → ∀L,s,d,e. ] qed. -lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ 𝐑[h, g]⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → - ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ 𝐑[h, g]⦃T⦄. +lemma crx_inv_lift: ∀h,g,G,L,U. ⦃G, L⦄ ⊢ ➡[h, g] 𝐑⦃U⦄ → ∀K,s,d,e. ⇩[s, d, e] L ≡ K → + ∀T. ⇧[d, e] T ≡ U → ⦃G, K⦄ ⊢ ➡[h, g] 𝐑⦃T⦄. #h #g #G #L #U #H elim H -L -U [ #L #k #l #Hkl #K #s #d #e #_ #X #H >(lift_inv_sort2 … H) -X /2 width=2 by crx_sort/ 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 506fa910b..7b7c453e4 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 @@ -106,7 +106,7 @@ table { ] [ { "context-sensitive extended computation" * } { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_alt ( ⦃?,?⦄ ⊢ ➡➡*[?,?] ? )" "lpxs_ldrop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_cpys" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ] } ] [ { "context-sensitive computation" * } { @@ -130,8 +130,8 @@ table { [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" + "fpb_aaa" * ] } ] - [ { "context-sensitive extended normal forms" * } { - [ "cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] + [ { "normal forms for context-sensitive extended reduction" * } { + [ "cnx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐍⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ] } ] [ { "context-sensitive extended reduction" * } { @@ -139,16 +139,16 @@ table { [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_cpys" + "cpx_lleq" + "cpx_cix" * ] } ] - [ { "context-sensitive extended irreducible forms" * } { - [ "cix ( ⦃?,?⦄ ⊢ 𝐈[?,?]⦃?⦄ )" "cix_append" + "cix_lift" * ] + [ { "irreducible forms for context-sensitive extended reduction" * } { + [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_append" + "cix_lift" * ] } ] - [ { "context-sensitive extended reducible forms" * } { - [ "crx ( ⦃?,?⦄ ⊢ 𝐑[?,?]⦃?⦄ )" "crx_append" + "crx_lift" * ] + [ { "reducible forms for context-sensitive extended reduction" * } { + [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_append" + "crx_lift" * ] } ] - [ { "context-sensitive normal forms" * } { - [ "cnr ( ⦃?,?⦄ ⊢ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] + [ { "normal forms for context-sensitive reduction" * } { + [ "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] } ] [ { "context-sensitive reduction" * } { @@ -156,12 +156,12 @@ table { [ "cpr ( ⦃?,?⦄ ⊢ ? ➡ ? )" "cpr_lift" + "cpr_cir" * ] } ] - [ { "context-sensitive irreducible forms" * } { - [ "cir ( ⦃?,?⦄ ⊢ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ] + [ { "irreducible forms for context-sensitive reduction" * } { + [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_append" + "cir_lift" * ] } ] - [ { "context-sensitive reducible forms" * } { - [ "crr ( ⦃?,?⦄ ⊢ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ] + [ { "reducible forms for context-sensitive reduction" * } { + [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_append" + "crr_lift" * ] } ] }