From cbc645186c8836c88c559c787a4deea63b7a12b0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 8 Mar 2017 21:17:06 +0000 Subject: [PATCH] cpxs_lfpx completed --- .../basic_2/i_static/{lfxss.ma => tc_lfxs.ma} | 100 +++++++++++------- .../basic_2/rt_computation/cpxs_drops.ma | 89 ++++++++++++++++ .../{cpxs_lift.ma => cpxs_fqus.ma} | 56 +--------- .../basic_2/rt_computation/cpxs_lfpx.ma | 57 ++++++++++ .../basic_2/rt_computation/partial.txt | 2 +- .../basic_2/rt_transition/lfpx_lfpx.ma | 23 ++++ .../basic_2/rt_transition/partial.txt | 2 +- .../lambdadelta/basic_2/static/lfxs.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../matita/contribs/lambdadelta/partial.txt | 1 + 10 files changed, 239 insertions(+), 97 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/i_static/{lfxss.ma => tc_lfxs.ma} (74%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{cpxs_lift.ma => cpxs_fqus.ma} (59%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma similarity index 74% rename from matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma rename to matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma index 757d3e684..4c30dc0a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma @@ -15,76 +15,102 @@ include "basic_2/notation/relations/relationstarstar_4.ma". include "basic_2/static/lfxs.ma". -(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) +(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) -definition lfxss (R) (T): relation lenv ≝ TC … (lfxs R T). +definition tc_lfxs (R) (T): relation lenv ≝ TC … (lfxs R T). -interpretation "tc of generic extension on referred entries (local environment)" - 'RelationStarStar R T L1 L2 = (lfxss R T L1 L2). +interpretation "iterated extension on referred entries (local environment)" + 'RelationStarStar R T L1 L2 = (tc_lfxs R T L1 L2). -(* Basic properties ***********************************************************) +(* Basic properties *********************************************************) -lemma lfxss_atom: ∀R,I. ⋆ ⦻**[R, ⓪{I}] ⋆. +lemma tc_lfxs_atom: ∀R,I. ⋆ ⦻**[R, ⓪{I}] ⋆. /2 width=1 by inj/ qed. -lemma lfxss_sort: ∀R,I,L1,L2,V1,V2,s. - L1 ⦻**[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻**[R, ⋆s] L2.ⓑ{I}V2. +lemma tc_lfxs_sort: ∀R,I,L1,L2,V1,V2,s. + L1 ⦻**[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻**[R, ⋆s] L2.ⓑ{I}V2. #R #I #L1 #L2 #V1 #V2 #s #H elim H -L2 /3 width=4 by lfxs_sort, step, inj/ qed. -lemma lfxss_lref: ∀R,I,L1,L2,V1,V2,i. - L1 ⦻**[R, #i] L2 → L1.ⓑ{I}V1 ⦻**[R, #⫯i] L2.ⓑ{I}V2. +lemma tc_lfxs_lref: ∀R,I,L1,L2,V1,V2,i. + L1 ⦻**[R, #i] L2 → L1.ⓑ{I}V1 ⦻**[R, #⫯i] L2.ⓑ{I}V2. #R #I #L1 #L2 #V1 #V2 #i #H elim H -L2 /3 width=4 by lfxs_lref, step, inj/ qed. -lemma lfxss_gref: ∀R,I,L1,L2,V1,V2,l. - L1 ⦻**[R, §l] L2 → L1.ⓑ{I}V1 ⦻**[R, §l] L2.ⓑ{I}V2. +lemma tc_lfxs_gref: ∀R,I,L1,L2,V1,V2,l. + L1 ⦻**[R, §l] L2 → L1.ⓑ{I}V1 ⦻**[R, §l] L2.ⓑ{I}V2. #R #I #L1 #L2 #V1 #V2 #l #H elim H -L2 /3 width=4 by lfxs_gref, step, inj/ qed. -lemma lfxss_sym: ∀R. lexs_frees_confluent R cfull → - (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → - ∀T. symmetric … (lfxss R T). +lemma tc_lfxs_sym: ∀R. lexs_frees_confluent R cfull → + (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → + ∀T. symmetric … (tc_lfxs R T). #R #H1R #H2R #T #L1 #L2 #H elim H -L2 /4 width=3 by lfxs_sym, TC_strap, inj/ qed-. -lemma lfxss_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → - ∀L1,L2,T. L1 ⦻**[R1, T] L2 → L1 ⦻**[R2, T] L2. +lemma tc_lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → + ∀L1,L2,T. L1 ⦻**[R1, T] L2 → L1 ⦻**[R2, T] L2. #R1 #R2 #HR #L1 #L2 #T #H elim H -L2 /4 width=5 by lfxs_co, step, inj/ qed-. -(* + (* Basic inversion lemmas ***************************************************) -lemma lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻*[R, ⓪{I}] Y2 → Y2 = ⋆. -#R #I #Y2 * /2 width=4 by lexs_inv_atom1/ +lemma tc_lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻**[R, ⓪{I}] Y2 → Y2 = ⋆. +#R #I #Y2 #H elim H -Y2 /3 width=3 by inj, lfxs_inv_atom_sn/ qed-. -lemma lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻*[R, ⓪{I}] ⋆ → Y1 = ⋆. -#R #I #Y1 * /2 width=4 by lexs_inv_atom2/ +lemma tc_lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻**[R, ⓪{I}] ⋆ → Y1 = ⋆. +#R #I #Y1 #H @(TC_ind_dx ??????? H) -Y1 +/3 width=3 by inj, lfxs_inv_atom_dx/ qed-. -lemma lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻*[R, ⋆s] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, ⋆s] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R * [ | #Y1 #I #V1 ] #Y2 #s * #f #H1 #H2 -[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ -| lapply (frees_inv_sort … H1) -H1 #Hf - elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct - elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct - /5 width=8 by frees_sort_gen, ex3_5_intro, ex2_intro, or_intror/ -] +lemma tc_lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻**[R, ⋆s] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻**[R, ⋆s] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 #s #H elim H -Y2 +[ #Y2 #H elim (lfxs_inv_sort … H) -H * + /4 width=8 by ex3_5_intro, inj, or_introl, or_intror, conj/ +| #Y #Y2 #_ #H elim (lfxs_inv_sort … H) -H * + [ #H #H2 * * /3 width=8 by ex3_5_intro, or_introl, or_intror, conj/ + | #I #L #L2 #V #V2 #HL2 #H #H2 * * + [ #H1 #H0 destruct + | #I0 #L1 #L0 #V1 #V0 #HL10 #H1 #H0 destruct + /4 width=8 by ex3_5_intro, step, or_intror/ + ] + ] +] +qed-. +(* +lemma tc_lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻**[R, #0] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻**[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 #H elim H -Y2 +[ #Y2 #H elim (lfxs_inv_zero … H) -H * + /4 width=9 by ex4_5_intro, inj, or_introl, or_intror, conj/ +| #Y #Y2 #_ #H elim (lfxs_inv_zero … H) -H * + [ #H #H2 * * /3 width=9 by ex4_5_intro, or_introl, or_intror, conj/ + | #I #L #L2 #V #V2 #HL2 #HV2 #H #H2 * * + [ #H1 #H0 destruct + | #I0 #L1 #L0 #V1 #V0 #HL10 #HV10 #H1 #H0 destruct + @or_intror @ex4_5_intro [6,7: |*: /width=7/ ] + + /4 width=8 by ex3_5_intro, step, or_intror/ + ] + ] +] qed-. -lemma lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻*[R, #0] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. + + + + #R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * [ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ | #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma new file mode 100644 index 000000000..26fb988b5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma @@ -0,0 +1,89 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/cpx_drops.ma". +include "basic_2/rt_computation/cpxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Advanced properties ******************************************************) + +lemma cpxs_delta: ∀h,I,G,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 → + ∀W2. ⬆*[1] V2 ≡ W2 → ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈*[h] W2. +#h #I #G #K #V1 #V2 #H @(cpxs_ind … H) -V2 +[ /3 width=3 by cpx_cpxs, cpx_delta/ +| #V #V2 #_ #HV2 #IH #W2 #HVW2 + elim (lifts_total V (𝐔❴1❵)) #W #HVW + elim (cpx_lifts … HV2 (Ⓣ) … (K.ⓑ{I}V1) … HVW) -HV2 + [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/ + | /3 width=1 by drops_refl, drops_drop/ + ] +] +qed. + +lemma cpxs_lref: ∀h,I,G,K,V,T,i. ⦃G, K⦄ ⊢ #i ⬈*[h] T → + ∀U. ⬆*[1] T ≡ U → ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈*[h] U. +#h #I #G #K #V #T #i #H @(cpxs_ind … H) -T +[ /3 width=3 by cpx_cpxs, cpx_lref/ +| #T0 #T #_ #HT2 #IH #U #HTU + elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0 + elim (cpx_lifts … HT2 (Ⓣ) … (K.ⓑ{I}V) … HTU0) -HT2 + [ #X #HTX <(lifts_mono … HTU … HTX) -T -X /3 width=3 by cpxs_strap1/ + | /3 width=1 by drops_refl, drops_drop/ + ] +] +qed. + +(* Basic_2A1: was: cpxs_delta *) +lemma cpxs_delta_drops: ∀h,I,G,L,K,V1,V2,i. + ⬇*[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ⬈*[h] V2 → + ∀W2. ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h] W2. +#h #I #G #L #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2 +[ /3 width=7 by cpx_cpxs, cpx_delta_drops/ +| #V #V2 #_ #HV2 #IH #W2 #HVW2 + elim (lifts_total V (𝐔❴⫯i❵)) #W #HVW + elim (cpx_lifts … HV2 (Ⓣ) … L … HVW) -HV2 + [ #V0 #HV20 <(lifts_mono … HVW2 … HV20) -V2 -V0 /3 width=3 by cpxs_strap1/ + | /2 width=3 by drops_isuni_fwd_drop2/ + ] +] +qed. +(* +(* Advanced inversion lemmas ************************************************) + +lemma cpxs_inv_lref1: ∀h,o,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h, o] T2 → + T2 = #i ∨ + ∃∃I,K,V1,T1. ⬇[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h, o] T1 & + ⬆[0, i+1] T1 ≡ T2. +#h #o #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ +#T #T2 #_ #HT2 * +[ #H destruct + elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ + * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ +| * #I #K #V1 #T1 #HLK #HVT1 #HT1 + lapply (drop_fwd_drop2 … HLK) #H0LK + elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T + /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ +] +qed-. + +(* Relocation properties ****************************************************) + +lemma cpxs_lift: ∀h,o,G. d_liftable (cpxs h o G). +/3 width=10 by cpx_lift, cpxs_strap1, d_liftable_LTC/ qed. + +lemma cpxs_inv_lift1: ∀h,o,G. d_deliftable_sn (cpxs h o G). +/3 width=6 by d_deliftable_sn_LTC, cpx_inv_lift1/ +qed-. +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma similarity index 59% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma index 9b4822e58..4bacb47f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_fqus.ma @@ -1,35 +1,8 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - +include "basic_2/computation/cpxs_lift.ma". include "basic_2/multiple/fqus_fqus.ma". -include "basic_2/reduction/cpx_lift.ma". -include "basic_2/computation/cpxs.ma". - -(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) (* Advanced properties ******************************************************) -lemma cpxs_delta: ∀h,o,I,G,L,K,V,V2,i. - ⬇[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ⬈*[h, o] V2 → - ∀W2. ⬆[0, i+1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ⬈*[h, o] W2. -#h #o #I #G #L #K #V #V2 #i #HLK #H elim H -V2 -[ /3 width=9 by cpx_cpxs, cpx_delta/ -| #V1 lapply (drop_fwd_drop2 … HLK) -HLK - elim (lift_total V1 0 (i+1)) /4 width=12 by cpx_lift, cpxs_strap1/ -] -qed. - lemma lstas_cpxs: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → ∀d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d1 → d2 ≤ d1 → ⦃G, L⦄ ⊢ T1 ⬈*[h, o] T2. #h #o #G #L #T1 #T2 #d2 #H elim H -G -L -T1 -T2 -d2 // @@ -48,33 +21,6 @@ lemma lstas_cpxs: ∀h,o,G,L,T1,T2,d2. ⦃G, L⦄ ⊢ T1 •*[h, d2] T2 → ] qed. -(* Advanced inversion lemmas ************************************************) - -lemma cpxs_inv_lref1: ∀h,o,G,L,T2,i. ⦃G, L⦄ ⊢ #i ⬈*[h, o] T2 → - T2 = #i ∨ - ∃∃I,K,V1,T1. ⬇[i] L ≡ K.ⓑ{I}V1 & ⦃G, K⦄ ⊢ V1 ⬈*[h, o] T1 & - ⬆[0, i+1] T1 ≡ T2. -#h #o #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/ -#T #T2 #_ #HT2 * -[ #H destruct - elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/ - * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/ -| * #I #K #V1 #T1 #HLK #HVT1 #HT1 - lapply (drop_fwd_drop2 … HLK) #H0LK - elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T - /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/ -] -qed-. - -(* Relocation properties ****************************************************) - -lemma cpxs_lift: ∀h,o,G. d_liftable (cpxs h o G). -/3 width=10 by cpx_lift, cpxs_strap1, d_liftable_LTC/ qed. - -lemma cpxs_inv_lift1: ∀h,o,G. d_deliftable_sn (cpxs h o G). -/3 width=6 by d_deliftable_sn_LTC, cpx_inv_lift1/ -qed-. - (* Properties on supclosure *************************************************) lemma fqu_cpxs_trans: ∀h,o,G1,G2,L1,L2,T2,U2. ⦃G2, L2⦄ ⊢ T2 ⬈*[h, o] U2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma new file mode 100644 index 000000000..b54ea1582 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/rt_transition/lfpx_lfpx.ma". +include "basic_2/rt_computation/cpxs_drops.ma". +include "basic_2/rt_computation/cpxs_cpxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS ************) + +(* Properties with uncounted parallel rt-transition on referred entries *****) + +lemma lfpx_cpxs_conf: ∀h,G. s_r_confluent1 … (cpxs h G) (lfpx h G). +/3 width=5 by lfpx_cpx_conf, s_r_conf1_LTC1/ qed-. + +lemma lfpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpx h G). +#h #G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 // +[ #G #L2 #s1 #L1 #H elim (lfpx_inv_sort … H) -H * /2 width=1 by cpx_cpxs/ +| #I #G #L2 #V #V2 #W2 #_ #IH #HVW2 #Y1 #H + elim (lfpx_inv_zero_pair_dx … H) -H #L1 #V1 #HL1 #HV1 #H destruct + /5 width=3 by lfpx_cpx_conf, cpxs_delta, cpxs_strap2/ +| #I #G #L2 #V #V2 #W2 #i #_ #IH #HVW2 #Y1 #H + elim (lfpx_inv_lref_pair_dx … H) -H #L1 #V1 #HL1 #HV1 + /4 width=3 by cpxs_lref, cpxs_strap2/ +| #p #I #G #L2 #V #V2 #T #T2 #_ #_ #IHV #IHT #L1 #H + elim (lfpx_inv_bind … H) -H /3 width=1 by cpxs_bind/ +| #I #G #L2 #V #V2 #T #T2 #_ #_ #IHV #IHT #L1 #H + elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_flat/ +| #G #L2 #V #T #T2 #T0 #_ #IH #HT02 #L1 #H + elim (lfpx_inv_bind … H) -H /3 width=3 by cpxs_zeta/ +| #G #L2 #V #T #T2 #_ #IH #L1 #H + elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_eps/ +| #G #L2 #V #V2 #T #_ #IH #L1 #H + elim (lfpx_inv_flat … H) -H /3 width=1 by cpxs_ee/ +| #p #G #L2 #V #V2 #W #W2 #T #T2 #_ #_ #_ #IHV #IHW #IHT #L1 #H + elim (lfpx_inv_flat … H) -H #HV #H + elim (lfpx_inv_bind … H) -H /3 width=1 by cpxs_beta/ +| #p #G #L2 #V #V2 #V0 #W #W2 #T #T2 #_ #_ #_ #IHV #IHW #IHT #HV20 #L1 #H + elim (lfpx_inv_flat … H) -H #HV #H + elim (lfpx_inv_bind … H) -H /3 width=3 by cpxs_theta/ +] +qed. + +lemma lfpx_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpx h G). +#h #G #L2 #T1 #T2 #H #L1 #HL12 @(cpxs_ind … H) -T2 +/4 width=7 by lfpx_cpx_trans, cpxs_trans, lfpx_cpxs_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index cb191dab1..7118b99b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,4 +1,4 @@ -cpxs.ma cpxs_tdeq.ma cpxs_cpxs.ma +cpxs.ma cpxs_tdeq.ma cpxs_drops.ma cpxs_lfpx.ma cpxs_cpxs.ma lfpxs.ma lfpxs_fqup.ma csx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma new file mode 100644 index 000000000..bf7dda13c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/cpx_lfxs.ma". +include "basic_2/rt_transition/lfpx.ma". + +(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) + +(* Advanced properties ******************************************************) + +lemma lfpx_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpx h G). +/2 width=5 by cpx_lfxs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 1adc75c38..67ed58697 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,6 +1,6 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma -lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_lfdeq.ma lfpx_aaa.ma +lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_lfdeq.ma lfpx_aaa.ma lfpx_lfpx.ma cnx.ma cnx_simple.ma cnx_drops.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma cpr.ma cpr_drops.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index a2f681634..a1d50e69f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -43,7 +43,7 @@ definition R_confluent2_lfxs: relation4 (relation3 lenv term term) ∀L1. L0 ⦻*[RP1, T0] L1 → ∀L2. L0 ⦻*[RP2, T0] L2 → ∃∃T. R2 L1 T1 T & R1 L2 T2 T. -(* Basic properties ***********************************************************) +(* Basic properties *********************************************************) lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆. /3 width=3 by lexs_atom, frees_atom, ex2_intro/ 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 f3d9d6021..fe1040d58 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 @@ -116,7 +116,7 @@ table { [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_cpxs" * ] + [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_drops" + "cpxs_lfpx" + "cpxs_cpxs" * ] } ] } @@ -143,7 +143,7 @@ table { ] [ { "uncounted context-sensitive rt-transition" * } { [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" * ] - [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" * ] + [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 7596031ba..48819214f 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -5,3 +5,4 @@ basic_2/s_transition basic_2/s_computation basic_2/static basic_2/i_static +apps_2/examples/ex_cpr_omega.ma -- 2.39.2