From: Ferruccio Guidi Date: Sun, 4 Mar 2018 18:59:20 +0000 (+0100) Subject: update in basic_2 X-Git-Tag: make_still_working~362 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=47a745462a714af9d65cea7b61af56524bd98fa1;p=helm.git update in basic_2 + new proof of cpx_frees_conf_lexs with fsle + refactoring --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma index 8a898e91f..ea91a9578 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "basic_2/relocation/lex_tc.ma". +include "basic_2/static/lfxs_fsle.ma". include "basic_2/static/lfeq_fqup.ma". include "basic_2/static/lfeq_lfeq.ma". include "basic_2/i_static/tc_lfxs_fqup.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma index 09039c5e3..5e4a93933 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/static/lfxs_lfxs.ma". +include "basic_2/static/lfxs_fsle.ma". include "basic_2/i_static/tc_lfxs.ma". (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_length.ma new file mode 100644 index 000000000..9c87f6652 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_length.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lexs_length.ma". +include "basic_2/relocation/lex.ma". + +(* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS **************) + +(* Forward lemmas with length for local environments ************************) + +(* Basic_2A1: was: lpx_sn_fwd_length *) +lemma lex_fwd_length: ∀R,L1,L2. L1 ⪤[R] L2 → |L1| = |L2|. +#R #L1 #L2 * /2 width=4 by lexs_fwd_length/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma index d33476cae..9a7621f9c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/relocation/rtmap_id.ma". include "basic_2/syntax/ext2_tc.ma". include "basic_2/relocation/lexs_tc.ma". include "basic_2/relocation/lex.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma index faefb9989..71467ba72 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma @@ -19,9 +19,8 @@ include "basic_2/relocation/lexs.ma". (* Forward lemmas with length for local environments ************************) -(* Basic_2A1: uses: lpx_sn_fwd_length *) lemma lexs_fwd_length: ∀RN,RP,f,L1,L2. L1 ⪤*[RN, RP, f] L2 → |L1| = |L2|. -#RM #RP #f #L1 #L2 #H elim H -f -L1 -L2 // +#RN #RP #f #L1 #L2 #H elim H -f -L1 -L2 // #f #I1 #I2 #L1 #L2 >length_bind >length_bind // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ext.ma new file mode 100644 index 000000000..7da6fa4f2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_ext.ma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/syntax/cext2.ma". +include "basic_2/rt_computation/cpxs.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR BINDERS **********) + +definition cpxs_ext (h) (G): relation3 lenv bind bind ≝ + cext2 (cpxs h G). + +interpretation + "uncounted context-sensitive parallel rt-computation (binder)" + 'PRedTyStar h G L I1 I2 = (cpxs_ext h G L I1 I2). 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 index 46aa78ace..2b12ff438 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma @@ -12,8 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/lfpx_fqup.ma". -include "basic_2/rt_transition/lfpx_cpx.ma". +include "basic_2/rt_transition/lfpx_fsle.ma". include "basic_2/rt_computation/cpxs_drops.ma". include "basic_2/rt_computation/cpxs_cpxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma index c2f308c96..152925b12 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_tdeq.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tdeq_tdeq.ma". -include "basic_2/rt_transition/lfpx_fqup.ma". include "basic_2/rt_transition/lfpx_lfdeq.ma". include "basic_2/rt_computation/cpxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma index a877af8b7..badaae1ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_csx.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tdeq_tdeq.ma". include "basic_2/rt_transition/lfpx_lfdeq.ma". include "basic_2/rt_computation/csx_drops.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma deleted file mode 100644 index d8989b799..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc.ma +++ /dev/null @@ -1,18 +0,0 @@ - -include "basic_2/static/lfxs_lex.ma". -include "basic_2/rt_transition/cpx_etc.ma". -include "basic_2/rt_computation/lfpxs_lpxs.ma". - -lemma R_fle_comp_LTC: ∀R. R_fle_compatible R → R_fle_compatible (LTC … R). -#R #HR #L #T1 #T2 #H elim H -T2 -/3 width=3 by fle_trans_dx/ -qed-. - -lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G). -#h #G #L1 #T1 #T2 #HT12 #L2 #H -elim (tc_lfxs_inv_lex_lfeq … H) -H #L #HL1 #HL2 -lapply (lfxs_lex … HL1 T1) #H -elim (cpx_lfxs_conf_fle … HT12 … H) -HT12 -H // #_ #HT21 #_ -@(lfpxs_lpxs_lfeq … HL1) -HL1 -@(fle_lfxs_trans … HL2) // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc2.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc2.ma deleted file mode 100644 index 0fa9b73d5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_etc2.ma +++ /dev/null @@ -1,63 +0,0 @@ - -include "basic_2/static/lfxs_lex.ma". -include "basic_2/rt_transition/cpx_etc.ma". -include "basic_2/rt_computation/lfpxs_lpxs.ma". - -axiom fle_trans: ∀L1,L,T1,T. ⦃L1, T1⦄ ⊆ ⦃L, T⦄ → - ∀L2,T2. ⦃L, T⦄ ⊆ ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊆ ⦃L2, T2⦄. - -axiom pippo: ∀h,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → ∀L. ⦃G, L1⦄ ⊢⬈[h] L → - ∧∧ ⦃L, T1⦄ ⊆ ⦃L1, T1⦄ & ⦃L, T2⦄ ⊆ ⦃L, T1⦄ & ⦃L1, T2⦄ ⊆ ⦃L1, T1⦄. -(* -lemma pippos: ∀h,G,L1,L. ⦃G, L1⦄ ⊢⬈*[h] L → ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → - ∧∧ ⦃L, T1⦄ ⊆ ⦃L1, T1⦄ & ⦃L, T2⦄ ⊆ ⦃L, T1⦄. -#h #G #L1 #L #H -lapply (lex_inv_ltc … H) -H // #H -@(TC_star_ind ???????? H) -L // -[ #T1 #T2 #H elim (pippo … H) -H /2 width=3 by conj/ -| #L #L0 #HL1 #HL0 #IH #T1 #T2 #HT12 - elim (IH … HT12) -IH #HT1 #HT21 - elim (pippo … T1 T1 … HL0) // #H1 #_ #_ - @conj - [ @(fle_trans … H1) // - -*)(* -lemma pippos: ∀h,G,L1,L. ⦃G, L1⦄ ⊢⬈*[h] L → ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → - ∧∧ ⦃L, T1⦄ ⊆ ⦃L1, T1⦄ & ⦃L, T2⦄ ⊆ ⦃L, T1⦄ & ⦃L1, T2⦄ ⊆ ⦃L1, T1⦄. -#h #G #L1 #L #H -lapply (lex_inv_ltc … H) -H // #H -@(TC_star_ind_dx ???????? H) -L1 /2 width=5 by pippo/ -#L1 #L0 #HL10 #HL0 #IH #T1 #T2 #HT12 -elim (IH … HT12) -IH #HT1 #HT21 #H1T21 -@and3_intro -[2: -*) - -axiom pippos: ∀h,G,L1,L. ⦃G, L1⦄ ⊢⬈*[h] L → ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ⬈[h] T & ⦃L, T2⦄ ⊆ ⦃L, T⦄. - -lemma fle_tc_lfxs_trans: ∀h,G,L1,L2,T1. ⦃G, L1⦄ ⊢⬈*[h, T1] L2 → - ∀T2. ⦃L1, T2⦄ ⊆ ⦃L1, T1⦄ → ⦃G, L1⦄ ⊢⬈* [h, T2] L2. -#h #G #L1 #L2 #T1 #H -@(TC_star_ind_dx ???????? H) -L1 /2 width=1 by tc_lfxs_refl, lfxs_refl/ -#L1 #L #HL1 #_ #IH #T2 #HT21 -lapply (fle_lfxs_trans … HT21 … HL1) -HL1 #HL1 -@(TC_strap … HL1) @IH -IH - - -lemma lfpxs_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G). -#h #G #L1 #T1 #T2 #HT12 #L2 #H -lapply (cpx_fle_comp … HT12) -HT12 #HT21 - -elim (tc_lfxs_inv_lex_lfeq … H) -H #L #HL1 #HL2 -@(lfpxs_lpxs_lfeq … HL1) -HL1 - - -@(fle_lfxs_trans - -elim (pippos … HL1 … HT12) -HT12 #T #H #HT21 -@(lfpxs_lpxs_lfeq … HL1) -HL1 -@(fle_lfxs_trans … HL2) -HL2 // -qed-. - - diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma index ce1bb6d13..70c9539c9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma @@ -19,6 +19,5 @@ include "basic_2/rt_computation/lfpxs.ma". (* Forward lemmas with length for local environments ************************) -(* Basic_2A1: uses: lpxs_fwd_length *) lemma lfpxs_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → |L1| = |L2|. /2 width=3 by tc_lfxs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma index 897199a9e..75c9f227a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/static/lfdeq_lfdeq.ma". include "basic_2/rt_transition/lfpx_lfdeq.ma". include "basic_2/rt_computation/lfpxs_fqup.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma index a6ef10ba9..acb4447e3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/static/lfdeq_lfdeq.ma". include "basic_2/rt_transition/lfpx_lfdeq.ma". include "basic_2/rt_computation/lfsx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma index d520aa6c2..507e0c3ef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/predtysnstar_4.ma". include "basic_2/relocation/lex.ma". -include "basic_2/rt_computation/cpxs.ma". +include "basic_2/rt_computation/cpxs_ext.ma". (* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************) @@ -24,3 +24,17 @@ definition lpxs: ∀h. relation3 genv lenv lenv ≝ interpretation "uncounted parallel rt-computation (local environment)" 'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2). + +(* Basic inversion lemmas ***************************************************) + +lemma lpxs_inv_bind_sn: ∀h,G,I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 → + ∃∃I2,K2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈*[h] I2 & L2 = K2.ⓘ{I2}. +/2 width=1 by lex_inv_bind_sn/ qed-. + +lemma lpxs_inv_pair_sn: ∀h,G,I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢⬈*[h] L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2. +#h #G #I #L2 #K1 #V1 #H +elim (lpxs_inv_bind_sn … H) -H #Y #K2 #HK12 #H0 #H destruct +elim (ext2_inv_pair_sn … H0) -H0 #V2 #HV12 #H destruct +/2 width=5 by ex3_2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma new file mode 100644 index 000000000..8b086f40c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.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/relocation/lex_length.ma". +include "basic_2/rt_computation/lpxs.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************) + +(* Forward lemmas with length for local environments ************************) + +lemma lpxs_fwd_length: ∀h,G,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → |L1| = |L2|. +/2 width=2 by lex_fwd_length/ 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 519cd481c..6b53efa07 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,5 +1,6 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma -lpxs.ma +cpxs_ext.ma +lpxs.ma lpxs_length.ma lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma index 2b6ef64ae..ad6e5d0ec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_cnx.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/syntax/tdeq_tdeq.ma". include "basic_2/rt_transition/lfpx_lfdeq.ma". include "basic_2/rt_transition/cnx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma new file mode 100644 index 000000000..604d922c7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_fsle.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||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_fsle.ma". +include "basic_2/rt_transition/cpm_cpx.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) + +(* Forward lemmas with free variables inclusion for restricted closures *****) + +lemma cpm_fsle_comp: ∀n,h,G. R_fsle_compatible (cpm n h G). +/3 width=6 by cpm_fwd_cpx, cpx_fsle_comp/ qed-. + +lemma lfpr_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpm 0 h G). +/4 width=5 by cpm_fwd_cpx, lfpx_fsle_comp, lfxs_co/ qed-. + +(* Properties with generic extension on referred entries ********************) + +(* Basic_2A1: was just: cpr_llpx_sn_conf *) +lemma cpm_lfxs_conf: ∀R,n,h,G. s_r_confluent1 … (cpm n h G) (lfxs R). +/3 width=5 by cpm_fwd_cpx, cpx_lfxs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma deleted file mode 100644 index f59669831..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lfxs.ma +++ /dev/null @@ -1,32 +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/rt_transition/cpx_lfxs.ma". -include "basic_2/rt_transition/cpm_cpx.ma". - -(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) - -(* Properties with context-sensitive free variables *************************) - -lemma cpm_fsle_comp: ∀n,h,G. R_fsle_compatible (cpm n h G). -/3 width=6 by cpm_fwd_cpx, cpx_fsle_comp/ qed-. - -lemma lfpr_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpm 0 h G). -/4 width=5 by cpm_fwd_cpx, lfpx_fsle_comp, lfxs_co/ qed-. - -(* Properties with generic extension on referred entries ********************) - -(* Basic_2A1: was just: cpr_llpx_sn_conf *) -lemma cpm_lfxs_conf: ∀R,n,h,G. s_r_confluent1 … (cpm n h G) (lfxs R). -/3 width=5 by cpm_fwd_cpx, cpx_lfxs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma deleted file mode 100644 index 2dcee12ee..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_etc.ma +++ /dev/null @@ -1,130 +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/static/fsle_drops.ma". -include "basic_2/static/fsle_fqup.ma". -include "basic_2/static/fsle_fsle.ma". -include "basic_2/static/lfxs_length.ma". -include "basic_2/static/lfxs_fsle.ma". -include "basic_2/rt_transition/cpx.ma". - -(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) - -(* Properties with context-sensitive free variables *************************) - -(* Note: "⦃L2, T1⦄ ⊆ ⦃L0, T1⦄" may not hold *) -axiom cpx_lfxs_conf_fsle: ∀R,h. c_reflexive … R → - (∨∨ (∀G. (cpx h G) = R) | R_fsle_compatible R) → - ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → - ∀L2. L0 ⪤*[R, T0] L2 → - ∧∧ ⦃L2, T0⦄ ⊆ ⦃L0, T0⦄ & ⦃L2, T1⦄ ⊆ ⦃L2, T0⦄ - & ⦃L0, T1⦄ ⊆ ⦃L0, T0⦄. -(* -#R #h #H1R #H2R #G #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G L0 T0) -G -L0 -T0 -#G #L #T #IH #G0 #L0 * * -[ #s #HG #HL #HT #X #HX #Y #HY destruct -IH - lapply (lfxs_fwd_length … HY) -HY #H0 - elim (cpx_inv_sort1 … HX) -HX #H destruct - /3 width=1 by fsle_sort_length, and3_intro/ -| * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct - [ elim (cpx_inv_zero1 … HX) -HX - [ #H destruct - elim (lfxs_inv_zero … HY) -HY * - [ #H1 #H2 destruct -IH /2 width=1 by and3_intro/ - | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct - lapply (lfxs_fwd_length … HK02) #HK - elim H2R -H2R #H2R - [ <(H2R G0) in HV02; -H2R #HV02 - elim (IH … HV02 … HK02) /2 width=2 by fqu_fqup, fqu_lref_O/ -IH -HV02 -HK02 #H1V #H2V #_ - /4 width=1 by fsle_trans_tc, fsle_zero_bi, and3_intro/ - | lapply (H2R … HV02 … HK02) -H2R -HV02 -HK02 -IH #HKV20 - /3 width=1 by fsle_zero_bi, and3_intro/ - ] - | #f #I #K0 #K2 #Hf #HK02 #H1 #H2 destruct - ] - | * #I0 #K0 #V0 #V1 #HV01 #HV1X #H destruct - elim (lfxs_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct - ] - | elim (cpx_inv_lref1 … HX) -HX - [ #H destruct - elim (lfxs_inv_lref … HY) -HY * - [ #H0 #H1 destruct /2 width=1 by and3_intro/ - | #I0 #I2 #K0 #K2 #HK02 #H1 #H2 destruct - lapply (lfxs_fwd_length … HK02) #HK - elim (IH … HK02) [|*: /2 width=4 by fqu_fqup/ ] -IH -HK02 - /3 width=5 by and3_intro, fsle_lifts_SO/ - ] - | * #I0 #K0 #V1 #HV1 #HV1X #H0 destruct - elim (lfxs_inv_lref_bind_sn … HY) -HY #I2 #K2 #HK02 #H destruct - lapply (lfxs_fwd_length … HK02) #HK - elim (IH … HK02) [|*: /2 width=4 by fqu_fqup/ ] -IH -HV1 -HK02 - /3 width=5 by fsle_lifts_SO, and3_intro/ - ] - ] -| #l #HG #HL #HT #X #HX #Y #HY destruct -IH - lapply (lfxs_fwd_length … HY) -HY #H0 - >(cpx_inv_gref1 … HX) -X - /3 width=1 by fsle_gref_length, and3_intro/ -| #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct - lapply (lfxs_fwd_length … HY) #H0 - elim (lfxs_inv_bind … V0 ? HY) -HY // #HV0 #HT0 - elim (cpx_inv_bind1 … HX) -HX * - [ #V1 #T1 #HV01 #HT01 #H destruct - elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V - elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T - /4 width=3 by fsle_bind_eq, fsle_fwd_pair_sn, and3_intro/ - | #T #HT #HXT #H1 #H2 destruct - elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V - elim (IH … HT … HT0) -HT -HT0 -IH // #H1T #H2T #H3T - /3 width=5 by fsle_bind, fsle_inv_lifts_sn, and3_intro/ - ] -| #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct - elim (lfxs_inv_flat … HY) -HY #HV0 #HX0 - elim (cpx_inv_flat1 … HX) -HX * - [ #V1 #T1 #HV01 #HT01 #H destruct - elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V - elim (IH … HT01 … HX0) -HT01 -HX0 -IH // #H1T #H2T #H3T - /3 width=3 by fsle_flat, and3_intro/ - | #HX #H destruct - elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V - elim (IH … HX … HX0) -HX -HX0 -IH // #H1T #H2T #H3T - /4 width=3 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, and3_intro/ - | #HX #H destruct - elim (IH … HX … HV0) -HX -HV0 // #H1V #H2V #H3V - elim (IH G0 … X0… X0 … HX0) -HX0 -IH // #H1T #H2T #H3T - /4 width=3 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, and3_intro/ - | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct - elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0 - elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V - elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W - elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T - lapply (fsle_fwd_pair_sn … H2T) -H2T #H2T - lapply (fsle_fwd_pair_sn … H3T) -H3T #H3T - @and3_intro [ /3 width=5 by fsle_flat, fsle_bind/ ] (**) (* full auto too slow *) - @fsle_bind_sn_ge /4 width=1 by fsle_shift, fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, fsle_bind_dx_sn/ - | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct - elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0 - elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V - elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W - elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T - lapply (fsle_fwd_pair_sn … H2T) -H2T #H2T - lapply (fsle_fwd_pair_sn … H3T) -H3T #H3T - @and3_intro[ /3 width=5 by fsle_flat, fsle_bind/ ] (**) (* full auto too slow *) - @fsle_bind_sn_ge // - [1,3: /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/ - |2,4: /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/ - ] - ] -] -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma index 00b3fca8f..c9fc90513 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfdeq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/lfdeq_lfdeq.ma". -include "basic_2/rt_transition/cpx_lfxs.ma". +include "basic_2/rt_transition/lfpx_fsle.ma". (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma index 5ffcd5b44..479953550 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfeq.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/static/lfeq.ma". -include "basic_2/rt_transition/cpx_lfxs.ma". +include "basic_2/rt_transition/lfpx_fsle.ma". (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma deleted file mode 100644 index 78b1302df..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lfxs.ma +++ /dev/null @@ -1,185 +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/syntax/lveq_length.ma". -include "basic_2/relocation/lexs_length.ma". -include "basic_2/relocation/drops_lexs.ma". -include "basic_2/static/frees_drops.ma". -include "basic_2/static/lsubf_frees.ma". -include "basic_2/static/lfxs_fsle.ma". -include "basic_2/rt_transition/cpx_drops.ma". -include "basic_2/rt_transition/cpx_ext.ma". - -(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) - -(* Properties with context-sensitive free variables *************************) - -(* Basic_2A1: uses: lpx_cpx_frees_trans *) -lemma cpx_frees_conf_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → - ∀L2. L1 ⪤*[cpx_ext h G, cfull, f1] L2 → - ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → - ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. -#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1 -#G0 #L0 #U0 #IH #G #L1 * * -[ -IH #s #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct - lapply (frees_inv_sort … H1) -H1 #Hg1 - elim (cpx_inv_sort1 … H0) -H0 #H destruct - /3 width=3 by frees_sort, sle_refl, ex2_intro/ -| #i #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct - elim (frees_inv_lref_drops … H1) -H1 * - [ -IH #f1 #HL1 #Hf1 #H destruct - elim (cpx_inv_lref1_drops … H0) -H0 - [ #H destruct - /4 width=9 by frees_atom_drops, drops_atom2_lexs_conf, sle_refl, ex2_intro/ - | * -H2 -Hf1 #I #K1 #V1 #V2 #HLK1 - lapply (drops_TF … HLK1) -HLK1 #HLK1 - lapply (drops_mono … HLK1 … HL1) -L1 #H destruct - ] - | #f1 #I #K1 #V1 #Hf1 #HLK1 #H destruct - elim (cpx_inv_lref1_drops … H0) -H0 - [ #H destruct - elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #Z #K2 #HLK2 #HK12 #H - elim (ext2_inv_pair_sn … H) -H #V2 #HV12 #H destruct - elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -L1 -K1 -V1 #f2 #Hf2 #Hf21 - /4 width=7 by frees_lref_pushs, frees_pair_drops, drops_refl, sle_pushs, sle_next, ex2_intro/ - | * #Z #Y #X #V2 #H #HV12 #HVU2 - lapply (drops_mono … H … HLK1) -H #H destruct - elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #I2 #K2 #HLK2 #HK12 #H - elim (ext2_inv_pair_sn … H) -H #V0 #_ #H destruct - lapply (drops_isuni_fwd_drop2 … HLK2) // -V0 #HLK2 - elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -I -L1 -K1 -V1 #f2 #Hf2 #Hf21 - lapply (frees_lifts … Hf2 … HLK2 … HVU2 ??) /4 width=7 by sle_weak, ex2_intro, sle_pushs/ - ] - | #f1 #I #K1 #HLK1 #Hf1 #H destruct - elim (cpx_inv_lref1_drops … H0) -H0 - [ -IH #H destruct - elim (lexs_drops_conf_next … H2 … HLK1) -H2 -HLK1 [ |*: // ] #Z #K2 #HLK2 #_ #H - lapply (ext2_inv_unit_sn … H) -H #H destruct - /3 width=3 by frees_unit_drops, sle_refl, ex2_intro/ - | * -H2 -Hf1 #Z #Y1 #X1 #X2 #HLY1 - lapply (drops_mono … HLK1 … HLY1) -L1 #H destruct - ] - ] -| -IH #l #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct - lapply (frees_inv_gref … H1) -H1 #Hg1 - lapply (cpx_inv_gref1 … H0) -H0 #H destruct - /3 width=3 by frees_gref, sle_refl, ex2_intro/ -| #p #I #V1 #T1 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct - elim (frees_inv_bind … H1) -H1 #gV1 #gT1 #HgV1 #HgT1 #Hg1 - elim (cpx_inv_bind1 … H0) -H0 * - [ #V2 #T2 #HV12 #HT12 #H destruct - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V - lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … (BPair I V1) (BPair I V2) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T - elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 - elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 - elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ - /4 width=10 by frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ - | #T2 #HT12 #HUT2 #H0 #H1 destruct -HgV1 - lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … (BPair Abbr V1) (BPair Abbr V1) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T - elim (IH … HgT1 … HL12T … HT12) // -L1 -T1 #gT2 #HgT2 #HgT21 - lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2 - /5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/ - ] -| #I #V1 #T0 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct - elim (frees_inv_flat … H1) -H1 #gV1 #gT0 #HgV1 #HgT0 #Hg1 - elim (cpx_inv_flat1 … H0) -H0 * - [ #V2 #T2 #HV12 #HT12 #H destruct - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V - lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 - elim (IH … HgT0 … HL12T … HT12) // -IH -HgT0 -HL12T -HT12 #gT2 #HgT2 #HgT21 - elim (sor_isfin_ex gV2 gT2) /2 width=3 by frees_fwd_isfin/ - /3 width=10 by frees_flat, monotonic_sle_sor, ex2_intro/ - | #HU2 #H destruct -HgV1 - lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - elim (IH … HgT0 … HL12T … HU2) // -L1 -T0 -V1 - /4 width=6 by sor_inv_sle_dx, sle_trans, ex2_intro/ - | #HU2 #H destruct -HgT0 - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ -H2 #HL12V - elim (IH … HgV1 … HL12V … HU2) // -L1 -T0 -V1 - /4 width=6 by sor_inv_sle_sn, sle_trans, ex2_intro/ - | #p #V2 #W1 #W2 #T1 #T2 #HV12 #HW12 #HT12 #H0 #H1 #H destruct - elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0 - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V - lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 - lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W - lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … (BPair Abst W1) (BPair Abst W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T - elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_ - lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 - lapply (sor_comm … Hg0) -Hg0 #Hg0 - elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 - elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21 - elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 - elim (sor_isfin_ex (⫱gT2) gV2) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_ - elim (lsubf_beta_tl_dx … HgV2 … HgVT2 … W2) [ |*: /1 width=3 by lsubf_refl/ ] #gT0 #HL2 #HgT02 - lapply (lsubf_frees_trans … HgT2 … HL2) -HgT2 -HL2 #HgT0 - lapply (sor_comm … HgVT2) -HgVT2 #HgVT2 (**) (* this should be removed *) - elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H - elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ - @(ex2_intro … g2) /3 width=5 by frees_flat, frees_bind/ -h -p -G -L1 -L2 -V1 -V2 -W1 -W2 -T1 -T2 - @(sor_inv_sle … Hg2) -Hg2 - [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/ - | @(sle_trans … HgT02) -HgT02 - /3 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl/ - ] (**) (* full auto too slow *) - | #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct - elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0 - lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V - lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 - lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W - lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … (BPair Abbr W1) (BPair Abbr W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T - elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_ - lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 - elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 - elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21 - elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 - elim (sor_isfin_ex (↑gV2) gT2) /3 width=3 by frees_fwd_isfin, isfin_push/ #gV0 #HgV0 #H - elim (sor_isfin_ex gW2 (⫱gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ - elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_ - lapply (sor_assoc_sn … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2 - lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??) - [4: lapply (sor_comm … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *) - /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ - ] -] -qed-. - -(* Basic_2A1: uses: cpx_frees_trans *) -lemma cpx_fsle_comp: ∀h,G. R_fsle_compatible (cpx h G). -#h #G #L #T1 #T2 #HT12 -elim (frees_total L T1) #f1 #Hf1 -elim (cpx_frees_conf_lexs … Hf1 L … HT12) -HT12 -/3 width=8 by lexs_refl, ext2_refl, ex4_4_intro/ -qed-. - -(* Basic_2A1: uses: lpx_frees_trans *) -lemma lfpx_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpx h G). -#h #G #L1 #L2 #T * #f1 #Hf1 #HL12 -elim (cpx_frees_conf_lexs h … Hf1 … HL12 T) // #f2 #Hf2 -lapply (lexs_fwd_length … HL12) -/3 width=8 by lveq_length_eq, ex4_4_intro/ (**) (* full auto fails *) -qed-. - -(* Properties with generic extension on referred entries ********************) - -(* Note: lemma 1000 *) -(* Basic_2A1: uses: cpx_llpx_sn_conf *) -lemma cpx_lfxs_conf: ∀R,h,G. s_r_confluent1 … (cpx h G) (lfxs R). -#R #h #G #L1 #T1 #T2 #H #L2 * #f1 #Hf1 elim (cpx_frees_conf_lexs … Hf1 L1 … H) -T1 -/3 width=5 by lexs_refl, ext2_refl, sle_lexs_trans, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index d5c4a4a8b..8be2aa641 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -12,9 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/static/lfxs_lfxs.ma". include "basic_2/rt_transition/cpm_lsubr.ma". -include "basic_2/rt_transition/cpm_lfxs.ma". +include "basic_2/rt_transition/cpm_fsle.ma". include "basic_2/rt_transition/cpr.ma". include "basic_2/rt_transition/cpr_drops.ma". include "basic_2/rt_transition/lfpr_drops.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma index 537bb8bc8..910324e69 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma @@ -67,14 +67,7 @@ lemma lfpx_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ⬈[h, ⋆s] Y2 → | ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 & Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. /2 width=1 by lfxs_inv_sort/ qed-. -(* -lemma lfpx_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ⬈[h, #0] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 & - ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -/2 width=1 by lfxs_inv_zero/ qed-. -*) + lemma lfpx_inv_lref: ∀h,G,Y1,Y2,i. ⦃G, Y1⦄ ⊢ ⬈[h, #⫯i] Y2 → ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ | ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 & diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_cpx.ma deleted file mode 100644 index bf7dda13c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_cpx.ma +++ /dev/null @@ -1,23 +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/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/lfpx_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_etc.ma new file mode 100644 index 000000000..7d5523fe3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_etc.ma @@ -0,0 +1,123 @@ +(**************************************************************************) +(* ___ *) +(* ||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_fsle.ma". +(* +lemma R_fle_comp_LTC: ∀R. R_fle_compatible R → R_fle_compatible (LTC … R). +#R #HR #L #T1 #T2 #H elim H -T2 +/3 width=3 by fle_trans_dx/ +qed-. +*) + +(* Note: "⦃L2, T1⦄ ⊆ ⦃L0, T1⦄" may not hold *) +axiom lfpx_cpx_conf_fsle4: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → + ∀L2. ⦃G, L0⦄ ⊢⬈[h, T0] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T1⦄. +(* +#h #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G0 L0 T0) -G0 -L0 -T0 +#G #L #T #IH #G0 #L0 * * +[ #s #HG #HL #HT #X #HX #Y #HY destruct -IH + lapply (lfxs_fwd_length … HY) -HY #H0 + elim (cpx_inv_sort1 … HX) -HX #H destruct + /3 width=1 by fsle_sort_length, and3_intro/ +| * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct + [ elim (cpx_inv_zero1 … HX) -HX + [ #H destruct + elim (lfxs_inv_zero … HY) -HY * + [ #H1 #H2 destruct -IH /2 width=1 by and3_intro/ + | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct + lapply (lfxs_fwd_length … HK02) #HK + elim H2R -H2R #H2R + [ <(H2R G0) in HV02; -H2R #HV02 + elim (IH … HV02 … HK02) /2 width=2 by fqu_fqup, fqu_lref_O/ -IH -HV02 -HK02 #H1V #H2V #_ + /4 width=1 by fsle_trans_tc, fsle_zero_bi, and3_intro/ + | lapply (H2R … HV02 … HK02) -H2R -HV02 -HK02 -IH #HKV20 + /3 width=1 by fsle_zero_bi, and3_intro/ + ] + | #f #I #K0 #K2 #Hf #HK02 #H1 #H2 destruct + ] + | * #I0 #K0 #V0 #V1 #HV01 #HV1X #H destruct + elim (lfxs_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct + ] + | elim (cpx_inv_lref1 … HX) -HX + [ #H destruct + elim (lfxs_inv_lref … HY) -HY * + [ #H0 #H1 destruct /2 width=1 by and3_intro/ + | #I0 #I2 #K0 #K2 #HK02 #H1 #H2 destruct + lapply (lfxs_fwd_length … HK02) #HK + elim (IH … HK02) [|*: /2 width=4 by fqu_fqup/ ] -IH -HK02 + /3 width=5 by and3_intro, fsle_lifts_SO/ + ] + | * #I0 #K0 #V1 #HV1 #HV1X #H0 destruct + elim (lfxs_inv_lref_bind_sn … HY) -HY #I2 #K2 #HK02 #H destruct + lapply (lfxs_fwd_length … HK02) #HK + elim (IH … HK02) [|*: /2 width=4 by fqu_fqup/ ] -IH -HV1 -HK02 + /3 width=5 by fsle_lifts_SO, and3_intro/ + ] + ] +| #l #HG #HL #HT #X #HX #Y #HY destruct -IH + lapply (lfxs_fwd_length … HY) -HY #H0 + >(cpx_inv_gref1 … HX) -X + /3 width=1 by fsle_gref_length, and3_intro/ +| #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct + lapply (lfxs_fwd_length … HY) #H0 + elim (lfxs_inv_bind … V0 ? HY) -HY // #HV0 #HT0 + elim (cpx_inv_bind1 … HX) -HX * + [ #V1 #T1 #HV01 #HT01 #H destruct + elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V + elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T + /4 width=3 by fsle_bind_eq, fsle_fwd_pair_sn, and3_intro/ + | #T #HT #HXT #H1 #H2 destruct + elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V + elim (IH … HT … HT0) -HT -HT0 -IH // #H1T #H2T #H3T + /3 width=5 by fsle_bind, fsle_inv_lifts_sn, and3_intro/ + ] +| #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct + elim (lfxs_inv_flat … HY) -HY #HV0 #HX0 + elim (cpx_inv_flat1 … HX) -HX * + [ #V1 #T1 #HV01 #HT01 #H destruct + elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V + elim (IH … HT01 … HX0) -HT01 -HX0 -IH // #H1T #H2T #H3T + /3 width=3 by fsle_flat, and3_intro/ + | #HX #H destruct + elim (IH G0 … V0… V0 … HV0) -HV0 // #H1V #H2V #H3V + elim (IH … HX … HX0) -HX -HX0 -IH // #H1T #H2T #H3T + /4 width=3 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, and3_intro/ + | #HX #H destruct + elim (IH … HX … HV0) -HX -HV0 // #H1V #H2V #H3V + elim (IH G0 … X0… X0 … HX0) -HX0 -IH // #H1T #H2T #H3T + /4 width=3 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, and3_intro/ + | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct + elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0 + elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V + elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W + elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T + lapply (fsle_fwd_pair_sn … H2T) -H2T #H2T + lapply (fsle_fwd_pair_sn … H3T) -H3T #H3T + @and3_intro [ /3 width=5 by fsle_flat, fsle_bind/ ] (**) (* full auto too slow *) + @fsle_bind_sn_ge /4 width=1 by fsle_shift, fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, fsle_bind_dx_sn/ + | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct + elim (lfxs_inv_bind … W0 ? HX0) -HX0 // #HW0 #HT0 + elim (IH … HV01 … HV0) -HV01 -HV0 // #H1V #H2V #H3V + elim (IH … HW01 … HW0) -HW01 -HW0 // #H1W #H2W #H3W + elim (IH … HT01 … HT0) -HT01 -HT0 -IH // #H1T #H2T #H3T + lapply (fsle_fwd_pair_sn … H2T) -H2T #H2T + lapply (fsle_fwd_pair_sn … H3T) -H3T #H3T + @and3_intro[ /3 width=5 by fsle_flat, fsle_bind/ ] (**) (* full auto too slow *) + @fsle_bind_sn_ge // + [1,3: /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/ + |2,4: /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/ + ] + ] +] +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma new file mode 100644 index 000000000..47f8eb859 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fsle.ma @@ -0,0 +1,134 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/fsle_drops.ma". +include "basic_2/static/lfxs_fsle.ma". +include "basic_2/rt_transition/lfpx_length.ma". +include "basic_2/rt_transition/lfpx_fqup.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) + +(* Forward lemmas with free variables inclusion for restricted closures *****) + +(* Note: "⦃L2, T1⦄ ⊆ ⦃L2, T0⦄" does not hold *) +(* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⬆*[1]V *) +(* Note: This invalidates lfpxs_cpx_conf: "∀h,G. s_r_confluent1 … (cpx h G) (lfpxs h G)" *) +(* Note: "⦃L2, T1⦄ ⊆ ⦃L0, T1⦄" may not hold *) +(* Basic_2A1: uses: lpx_cpx_frees_trans *) +lemma lfpx_cpx_conf_fsle: ∀h,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → + ∀L2. ⦃G, L0⦄ ⊢⬈[h, T0] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T0⦄. +#h #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓕ) … G0 L0 T0) -G0 -L0 -T0 +#G #L #T #IH #G0 #L0 * * +[ #s #HG #HL #HT #X #HX #Y #HY destruct -IH + elim (cpx_inv_sort1 … HX) -HX #H destruct + lapply (lfpx_fwd_length … HY) -HY #H0 + /2 width=1 by fsle_sort_bi/ +| * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct + [ elim (cpx_inv_zero1 … HX) -HX + [ #H destruct + elim (lfpx_inv_zero_length … HY) -HY * + [ #H1 #H2 destruct -IH // + | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct + lapply (lfpx_fwd_length … HK02) #H0 + /4 width=4 by fsle_pair_bi, fqu_fqup, fqu_lref_O/ + | #I #K0 #K2 #HK02 #H1 #H2 destruct -IH + /2 width=1 by fsle_unit_bi/ + ] + | * #I0 #K0 #V0 #V1 #HV01 #HV1X #H destruct + elim (lfpx_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct + lapply (lfpx_fwd_length … HK02) #H0 + /4 width=4 by fsle_lifts_SO_sn, fqu_fqup, fqu_lref_O/ + ] + | elim (cpx_inv_lref1 … HX) -HX + [ #H destruct + elim (lfpx_inv_lref … HY) -HY * + [ #H0 #H1 destruct // + | #I0 #I2 #K0 #K2 #HK02 #H1 #H2 destruct + lapply (lfpx_fwd_length … HK02) #H0 + /4 width=5 by fsle_lifts_SO, fqu_fqup/ + ] + | * #I0 #K0 #V1 #HV1 #HV1X #H0 destruct + elim (lfpx_inv_lref_bind_sn … HY) -HY #I2 #K2 #HK02 #H destruct + lapply (lfpx_fwd_length … HK02) #H0 + /4 width=5 by fsle_lifts_SO, fqu_fqup/ + ] + ] +| #l #HG #HL #HT #X #HX #Y #HY destruct -IH + >(cpx_inv_gref1 … HX) -X + lapply (lfpx_fwd_length … HY) -HY #H0 + /2 width=1 by fsle_gref_bi/ +| #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct + elim (lfpx_inv_bind … V0 ? HY) -HY #HV0 #HT0 + elim (cpx_inv_bind1 … HX) -HX * + [ #V1 #T1 #HV01 #HT01 #H destruct + lapply (lfpx_fwd_length … HV0) #H0 + /4 width=6 by fsle_bind_eq, fsle_fwd_pair_sn/ + | #T #HT #HXT #H1 #H2 destruct + lapply (lfpx_fwd_length … HV0) #H0 + /3 width=8 by fsle_inv_lifts_sn/ + ] +| #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct + elim (lfxs_inv_flat … HY) -HY #HV0 #HX0 + elim (cpx_inv_flat1 … HX) -HX * + [ #V1 #T1 #HV01 #HT01 #H destruct + /3 width=4 by fsle_flat/ + | #HX #H destruct + /4 width=4 by fsle_flat_dx_dx/ + | #HX #H destruct + /4 width=4 by fsle_flat_dx_sn/ + | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct + elim (lfpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0 + lapply (lfpx_fwd_length … HV0) #H0 + lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV + lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW + lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT + lapply (fsle_fwd_pair_sn … HT) -HT #HT + @fsle_bind_sn_ge // + [ /4 width=1 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, fsle_bind_dx_sn/ + | /3 width=1 by fsle_flat_dx_dx, fsle_shift/ + ] + | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct + elim (lfpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0 + lapply (lfpx_fwd_length … HV0) #H0 + lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV + lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW + lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT + lapply (fsle_fwd_pair_sn … HT) -HT #HT + @fsle_bind_sn_ge // + [ /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/ + | /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/ + ] + ] +] +qed. + +(* Basic_2A1: uses: cpx_frees_trans *) +lemma cpx_fsle_comp: ∀h,G. R_fsle_compatible (cpx h G). +/2 width=4 by lfpx_cpx_conf_fsle/ qed-. + +(* Basic_2A1: uses: lpx_frees_trans *) +lemma lfpx_fsle_comp: ∀h,G. lfxs_fsle_compatible (cpx h G). +/2 width=4 by lfpx_cpx_conf_fsle/ qed-. + +(* Properties with generic extension on referred entries ********************) + +(* Note: lemma 1000 *) +(* Basic_2A1: uses: cpx_llpx_sn_conf *) +lemma cpx_lfxs_conf: ∀R,h,G. s_r_confluent1 … (cpx h G) (lfxs R). +/3 width=3 by fsle_lfxs_trans, cpx_fsle_comp/ qed-. + +(* 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/lfpx_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma index d0ca2b90c..7b194bd71 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma @@ -22,3 +22,13 @@ include "basic_2/rt_transition/lfpx.ma". (* Basic_2A1: uses: lpx_fwd_length *) lemma lfpx_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → |L1| = |L2|. /2 width=3 by lfxs_fwd_length/ qed-. + +(* Inversion lemmas with length for local environments **********************) + +lemma lfpx_inv_zero_length: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ⬈[h, #0] Y2 → + ∨∨ ∧∧ Y1 = ⋆ & Y2 = ⋆ + | ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 & + ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2 + |∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. +/2 width=1 by lfxs_inv_zero_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index 8c997a9d3..c20039612 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -12,12 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lifts_tdeq.ma". -include "basic_2/static/lfxs_lfxs.ma". include "basic_2/static/lfdeq_fqup.ma". include "basic_2/static/lfdeq_lfdeq.ma". -include "basic_2/rt_transition/cpx_lfxs.ma". -include "basic_2/rt_transition/lfpx.ma". +include "basic_2/rt_transition/lfpx_fsle.ma". (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma deleted file mode 100644 index cfc4778db..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fle.ma +++ /dev/null @@ -1,20 +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/static/fsle.ma". - -(* FREE VARIABLES INCLUSION FOR TERMS ***************************************) - -interpretation "free variables inclusion (term)" - 'subseteq T1 T2 = (fsle LAtom T1 LAtom T2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma index 25fca9573..206ec63e4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees.ma @@ -172,33 +172,6 @@ lemma frees_inv_flat: ∀f,I,L,V,T. L ⊢ 𝐅*⦃ⓕ{I}V.T⦄ ≡ f → ∃∃f1,f2. L ⊢ 𝐅*⦃V⦄ ≡ f1 & L ⊢ 𝐅*⦃T⦄ ≡ f2 & f1 ⋓ f2 ≡ f. /2 width=4 by frees_inv_flat_aux/ qed-. -(* Advanced inversion lemmas ***********************************************) -(* -lemma frees_inv_zero_pair: ∀f,I,K,V. K.ⓑ{I}V ⊢ 𝐅*⦃#0⦄ ≡ f → - ∃∃g. K ⊢ 𝐅*⦃V⦄ ≡ g & f = ⫯g. -#f #I #K #V #H elim (frees_inv_zero … H) -H * -[ #H destruct -| #g #Z #Y #X #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/ -| #g #Z #Y #_ #H destruct -] -qed-. - -lemma frees_inv_zero_unit: ∀f,I,K. K.ⓤ{I} ⊢ 𝐅*⦃#0⦄ ≡ f → ∃∃g. 𝐈⦃g⦄ & f = ⫯g. -#f #I #K #H elim (frees_inv_zero … H) -H * -[ #H destruct -| #g #Z #Y #X #_ #H destruct -| /2 width=3 by ex2_intro/ -] -qed-. - -lemma frees_inv_lref_bind: ∀f,I,K,i. K.ⓘ{I} ⊢ 𝐅*⦃#(⫯i)⦄ ≡ f → - ∃∃g. K ⊢ 𝐅*⦃#i⦄ ≡ g & f = ↑g. -#f #I #K #i #H elim (frees_inv_lref … H) -H * -[ #H destruct -| #g #Z #Y #Hg #H1 #H2 destruct /3 width=3 by ex2_intro/ -] -qed-. -*) (* Basic properties ********************************************************) lemma frees_eq_repl_back: ∀L,T. eq_repl_back … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f). @@ -226,6 +199,12 @@ lemma frees_eq_repl_fwd: ∀L,T. eq_repl_fwd … (λf. L ⊢ 𝐅*⦃T⦄ ≡ f) #L #T @eq_repl_sym /2 width=3 by frees_eq_repl_back/ qed-. +lemma frees_lref_push: ∀f,i. ⋆ ⊢ 𝐅*⦃#i⦄ ≡ f → ⋆ ⊢ 𝐅*⦃#⫯i⦄ ≡ ↑f. +#f #i #H +elim (frees_inv_atom … H) -H #g #Hg #H destruct +/2 width=1 by frees_atom/ +qed. + (* Forward lemmas with test for finite colength *****************************) lemma frees_fwd_isfin: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f → 𝐅⦃f⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_append.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_append.ma new file mode 100644 index 000000000..56205c3db --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_append.ma @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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/syntax/append.ma". +include "basic_2/static/frees.ma". + +(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) + +(* Properties with append for local environments ****************************) + +lemma frees_append_void: ∀f,K,T. K ⊢ 𝐅*⦃T⦄ ≡ f → ⓧ.K ⊢ 𝐅*⦃T⦄ ≡ f. +#f #K #T #H elim H -f -K -T +[ /2 width=1 by frees_sort/ +| #f * /3 width=1 by frees_atom, frees_unit, frees_lref/ +| /2 width=1 by frees_pair/ +| /2 width=1 by frees_unit/ +| /2 width=1 by frees_lref/ +| /2 width=1 by frees_gref/ +| /3 width=5 by frees_bind/ +| /3 width=5 by frees_flat/ +] +qed. + +(* Inversion lemmas with append for local environments **********************) + +fact frees_inv_append_void_aux: ∀f,L,T. L ⊢ 𝐅*⦃T⦄ ≡ f → + ∀K. L = ⓧ.K → K ⊢ 𝐅*⦃T⦄ ≡ f. +#f #L #T #H elim H -f -L -T +[ /2 width=1 by frees_sort/ +| #f #i #_ #K #H + elim (append_inv_atom3_sn … H) -H #H1 #H2 destruct +| #f #I #L #V #_ #IH #K #H + elim (append_inv_bind3_sn … H) -H * [ | #Y ] #H1 #H2 destruct + /3 width=1 by frees_pair/ +| #f #I #L #Hf #K #H + elim (append_inv_bind3_sn … H) -H * [ | #Y ] #H1 #H2 destruct + /2 width=1 by frees_atom, frees_unit/ +| #f #I #L #i #Hf #IH #K #H + elim (append_inv_bind3_sn … H) -H * [ | #Y ] #H1 #H2 destruct + /3 width=1 by frees_lref, frees_lref_push/ +| /2 width=1 by frees_gref/ +| /3 width=5 by frees_bind/ +| /3 width=5 by frees_flat/ +] +qed-. + +lemma frees_inv_append_void: ∀f,K,T. ⓧ.K ⊢ 𝐅*⦃T⦄ ≡ f → K ⊢ 𝐅*⦃T⦄ ≡ f. +/2 width=3 by frees_inv_append_void_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma index 273a2755a..7ca1aa214 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_drops.ma @@ -29,6 +29,15 @@ lapply (frees_lifts_SO (Ⓣ) (L1.ⓧ) … HTU1 … Hf) @(ex4_4_intro … Hf Hg) /2 width=4 by lveq_void_sn/ (**) (* explict constructor *) qed-. +lemma fsle_lifts_SO_sn: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ → + ∀W1. ⬆*[1] V1 ≡ W1 → ∀I1,I2. ⦃K1.ⓘ{I1}, W1⦄ ⊆ ⦃K2.ⓑ{I2}V2, #O⦄. +#K1 #K2 #HK #V1 #V2 +* #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12 +#W1 #HVW1 #I1 #I2 +elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct +/5 width=12 by frees_lifts_SO, frees_pair, drops_refl, drops_drop, lveq_bind, sle_weak, ex4_4_intro/ +qed. + lemma fsle_lifts_SO: ∀K1,K2. |K1| = |K2| → ∀T1,T2. ⦃K1, T1⦄ ⊆ ⦃K2, T2⦄ → ∀U1,U2. ⬆*[1] T1 ≡ U1 → ⬆*[1] T2 ≡ U2 → ∀I1,I2. ⦃K1.ⓘ{I1}, U1⦄ ⊆ ⦃K2.ⓘ{I2}, U2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_length.ma index c2275e65f..9f54a92e4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/fsle_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/fsle_length.ma @@ -25,7 +25,7 @@ lemma fsle_sort_bi: ∀L1,L2,s1,s2. |L1| = |L2| → ⦃L1, ⋆s1⦄ ⊆ ⦃L2, lemma fsle_gref_bi: ∀L1,L2,l1,l2. |L1| = |L2| → ⦃L1, §l1⦄ ⊆ ⦃L2, §l2⦄. /3 width=8 by lveq_length_eq, frees_gref, sle_refl, ex4_4_intro/ qed. -lemma fsle_zero_bi: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ → +lemma fsle_pair_bi: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, V2⦄ → ∀I1,I2. ⦃K1.ⓑ{I1}V1, #O⦄ ⊆ ⦃K2.ⓑ{I2}V2, #O⦄. #K1 #K2 #HK #V1 #V2 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #HK12 #Hf12 @@ -33,3 +33,8 @@ lemma fsle_zero_bi: ∀K1,K2. |K1| = |K2| → ∀V1,V2. ⦃K1, V1⦄ ⊆ ⦃K2, elim (lveq_inj_length … HK12) // -HK #H1 #H2 destruct /3 width=12 by frees_pair, lveq_bind, sle_next, ex4_4_intro/ qed. + +lemma fsle_unit_bi: ∀K1,K2. |K1| = |K2| → + ∀I1,I2. ⦃K1.ⓤ{I1}, #O⦄ ⊆ ⦃K2.ⓤ{I2}, #O⦄. +/3 width=8 by frees_unit, lveq_length_eq, sle_refl, ex4_4_intro/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma index bf2f11a47..06fa93f19 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "basic_2/syntax/lveq_length.ma". include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/static/lfxs_length.ma". include "basic_2/static/lfxs_fsle.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma index e88b4397c..7326b418c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma @@ -14,7 +14,6 @@ include "basic_2/syntax/ext2_ext2.ma". include "basic_2/syntax/tdeq_tdeq.ma". -include "basic_2/static/lfxs_lfxs.ma". include "basic_2/static/lfdeq_length.ma". (* DEGREE-BASED EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ******) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma index 0f3d67132..cc7218982 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fsle.ma @@ -12,8 +12,10 @@ (* *) (**************************************************************************) -include "basic_2/static/fsle.ma". -include "basic_2/static/lfxs.ma". +include "basic_2/relocation/lexs_length.ma". +include "basic_2/static/frees_drops.ma". +include "basic_2/static/fsle_fsle.ma". +include "basic_2/static/lfxs_lfxs.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) @@ -22,3 +24,139 @@ definition R_fsle_compatible: predicate (relation3 …) ≝ λRN. definition lfxs_fsle_compatible: predicate (relation3 …) ≝ λRN. ∀L1,L2,T. L1 ⪤*[RN, T] L2 → ⦃L2, T⦄ ⊆ ⦃L1, T⦄. + +(* Basic inversions with free variables inclusion for restricted closures ***) + +lemma frees_lexs_conf: ∀R. lfxs_fsle_compatible R → + ∀L1,T,f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → + ∀L2. L1 ⪤*[cext2 R, cfull, f1] L2 → + ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. +#R #HR #L1 #T #f1 #Hf1 #L2 #H1L +lapply (HR L1 L2 T ?) /2 width=3 by ex2_intro/ #H2L +@(fsle_frees_trans_eq … H2L … Hf1) /3 width=4 by lexs_fwd_length, sym_eq/ +qed-. + +(* Properties with free variables inclusion for restricted closures *********) + +(* Note: we just need lveq_inv_refl: ∀L,n1,n2. L ≋ⓧ*[n1, n2] L → ∧∧ 0 = n1 & 0 = n2 *) +lemma fsle_lfxs_trans: ∀R,L1,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L1, T2⦄ → + ∀L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2. +#R #L1 #T1 #T2 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #Hn #Hf #L2 #HL12 +elim (lveq_inj_length … Hn ?) // #H1 #H2 destruct +/4 width=5 by lfxs_inv_frees, sle_lexs_trans, ex2_intro/ +qed-. + +lemma lfxs_sym: ∀R. lfxs_fsle_compatible R → + (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → + ∀T. symmetric … (lfxs R T). +#R #H1R #H2R #T #L1 #L2 +* #f1 #Hf1 #HL12 +elim (frees_lexs_conf … Hf1 … HL12) -Hf1 // +/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, ex2_intro/ +qed-. + +lemma lfxs_pair_sn_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → + lfxs_fsle_compatible R1 → + ∀L1,L2,V. L1 ⪤*[R1, V] L2 → ∀I,T. + ∃∃L. L1 ⪤*[R1, ②{I}V.T] L & L ⪤*[R2, V] L2. +#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #V * #f #Hf #HL12 * [ #p ] #I #T +[ elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg + elim (frees_inv_bind … Hg) #y1 #y2 #H #_ #Hy +| elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg + elim (frees_inv_flat … Hg) #y1 #y2 #H #_ #Hy +] +lapply(frees_mono … H … Hf) -H #H1 +lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy +lapply (sor_inv_sle_sn … Hy) -y2 #Hfg +elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 +lapply (sle_lexs_trans … HL1 … Hfg) // #H +elim (frees_lexs_conf … Hf … H) -Hf -H +/4 width=7 by sle_lexs_trans, ex2_intro/ +qed-. + +lemma lfxs_flat_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → + lfxs_fsle_compatible R1 → + ∀L1,L2,T. L1 ⪤*[R1, T] L2 → ∀I,V. + ∃∃L. L1 ⪤*[R1, ⓕ{I}V.T] L & L ⪤*[R2, T] L2. +#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #I #V +elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg +elim (frees_inv_flat … Hg) #y1 #y2 #_ #H #Hy +lapply(frees_mono … H … Hf) -H #H2 +lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy +lapply (sor_inv_sle_dx … Hy) -y1 #Hfg +elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 +lapply (sle_lexs_trans … HL1 … Hfg) // #H +elim (frees_lexs_conf … Hf … H) -Hf -H +/4 width=7 by sle_lexs_trans, ex2_intro/ +qed-. + +lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → + lfxs_fsle_compatible R1 → + ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⪤*[R1, T] L2 → ∀p. + ∃∃L,V. L1 ⪤*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⪤*[R2, T] L2 & R1 L1 V1 V. +#R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p +elim (frees_total L1 (ⓑ{p,I}V1.T)) #g #Hg +elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy +lapply(frees_mono … H … Hf) -H #H2 +lapply (tl_eq_repl … H2) -H2 #H2 +lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy +lapply (sor_inv_sle_dx … Hy) -y1 #Hfg +lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg +elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 +lapply (sle_lexs_trans … H … Hfg) // #H0 +elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H +elim (ext2_inv_pair_sn … H) -H #V #HV #H1 #H2 destruct +elim (frees_lexs_conf … Hf … H0) -Hf -H0 +/4 width=7 by sle_lexs_trans, ex3_2_intro, ex2_intro/ +qed-. + +lemma lfxs_bind_dx_split_void: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → + lfxs_fsle_compatible R1 → + ∀L1,L2,T. L1.ⓧ ⪤*[R1, T] L2 → ∀p,I,V. + ∃∃L. L1 ⪤*[R1, ⓑ{p,I}V.T] L & L.ⓧ ⪤*[R2, T] L2. +#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #p #I #V +elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg +elim (frees_inv_bind_void … Hg) #y1 #y2 #_ #H #Hy +lapply(frees_mono … H … Hf) -H #H2 +lapply (tl_eq_repl … H2) -H2 #H2 +lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy +lapply (sor_inv_sle_dx … Hy) -y1 #Hfg +lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg +elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 +lapply (sle_lexs_trans … H … Hfg) // #H0 +elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H +elim (ext2_inv_unit_sn … H) -H #H destruct +elim (frees_lexs_conf … Hf … H0) -Hf -H0 +/4 width=7 by sle_lexs_trans, ex2_intro/ (* note: 2 ex2_intro *) +qed-. + +(* Main properties with free variables inclusion for restricted closures ****) + +theorem lfxs_conf: ∀R1,R2. + lfxs_fsle_compatible R1 → + lfxs_fsle_compatible R2 → + R_confluent2_lfxs R1 R2 R1 R2 → + ∀T. confluent2 … (lfxs R1 T) (lfxs R2 T). +#R1 #R2 #HR1 #HR2 #HR12 #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02 +lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12 +lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01 +elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] +[ #L #HL1 #HL2 + elim (frees_lexs_conf … Hf … HL01) // -HR1 -HL01 #f1 #Hf1 #H1 + elim (frees_lexs_conf … Hf … HL02) // -HR2 -HL02 #f2 #Hf2 #H2 + lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1 + lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2 + /3 width=5 by ex2_intro/ +| #g * #I0 [2: #V0 ] #K0 #n #HLK0 #Hgf #Z1 #H1 #Z2 #H2 #K1 #HK01 #K2 #HK02 + [ elim (ext2_inv_pair_sn … H1) -H1 #V1 #HV01 #H destruct + elim (ext2_inv_pair_sn … H2) -H2 #V2 #HV02 #H destruct + elim (frees_inv_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0 + lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01 + lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02 + elim (HR12 … HV01 … HV02 K1 … K2) /3 width=3 by ext2_pair, ex2_intro/ + | lapply (ext2_inv_unit_sn … H1) -H1 #H destruct + lapply (ext2_inv_unit_sn … H2) -H2 #H destruct + /3 width=3 by ext2_unit, ex2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma index 2a090e642..5f8b62e08 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma @@ -36,3 +36,14 @@ elim (frees_total L1 U) #f2 #Hf2 lapply (frees_fwd_coafter … Hf2 … HLK1 … HTU … Hf1) -HTU #Hf /4 width=12 by lexs_length_cfull, lexs_liftable_co_dedropable_bi, cext2_d_liftable2_sn, cfull_lift_sn, ex2_intro/ qed-. + +(* Inversion lemmas with length for local environment ***********************) + +lemma lfxs_inv_zero_length: ∀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 + | ∃∃I,L1,L2. |L1| = |L2| & Y1 = L1.ⓤ{I} & Y2 = L2.ⓤ{I}. +#R #Y1 #Y2 #H elim (lfxs_inv_zero … H) -H * +/4 width=9 by lexs_fwd_length, ex4_5_intro, ex3_3_intro, or3_intro2, or3_intro1, or3_intro0, conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index cdf65c7c0..115d509ba 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -12,11 +12,9 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lexs_length.ma". include "basic_2/relocation/lexs_lexs.ma". -include "basic_2/static/frees_drops.ma". -include "basic_2/static/fsle_fsle.ma". -include "basic_2/static/lfxs_fsle.ma". +include "basic_2/static/frees_fqup.ma". +include "basic_2/static/lfxs.ma". (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****) @@ -27,36 +25,8 @@ lemma lfxs_inv_frees: ∀R,L1,L2,T. L1 ⪤*[R, T] L2 → #R #L1 #L2 #T * /3 width=6 by frees_mono, lexs_eq_repl_back/ qed-. -lemma frees_lexs_conf: ∀R. lfxs_fsle_compatible R → - ∀L1,T,f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 → - ∀L2. L1 ⪤*[cext2 R, cfull, f1] L2 → - ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1. -#R #HR #L1 #T #f1 #Hf1 #L2 #H1L -lapply (HR L1 L2 T ?) /2 width=3 by ex2_intro/ #H2L -@(fsle_frees_trans_eq … H2L … Hf1) /3 width=4 by lexs_fwd_length, sym_eq/ -qed-. - -(* Properties with free variables inclusion for restricted closures *********) - -(* Note: we just need lveq_inv_refl: ∀L,n1,n2. L ≋ⓧ*[n1, n2] L → ∧∧ 0 = n1 & 0 = n2 *) -lemma fle_lfxs_trans: ∀R,L1,T1,T2. ⦃L1, T1⦄ ⊆ ⦃L1, T2⦄ → - ∀L2. L1 ⪤*[R, T2] L2 → L1 ⪤*[R, T1] L2. -#R #L1 #T1 #T2 * #n1 #n2 #f1 #f2 #Hf1 #Hf2 #Hn #Hf #L2 #HL12 -elim (lveq_inj_length … Hn ?) // #H1 #H2 destruct -/4 width=5 by lfxs_inv_frees, sle_lexs_trans, ex2_intro/ -qed-. - (* Advanced properties ******************************************************) -lemma lfxs_sym: ∀R. lfxs_fsle_compatible R → - (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → - ∀T. symmetric … (lfxs R T). -#R #H1R #H2R #T #L1 #L2 -* #f1 #Hf1 #HL12 -elim (frees_lexs_conf … Hf1 … HL12) -Hf1 // -/5 width=5 by sle_lexs_trans, lexs_sym, cext2_sym, ex2_intro/ -qed-. - (* Basic_2A1: uses: llpx_sn_dec *) lemma lfxs_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → ∀L1,L2,T. Decidable (L1 ⪤*[R, T] L2). @@ -66,81 +36,6 @@ elim (lexs_dec (cext2 R) cfull … L1 L2 f) /4 width=3 by lfxs_inv_frees, cfull_dec, ext2_dec, ex2_intro, or_intror, or_introl/ qed-. -lemma lfxs_pair_sn_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lfxs_fsle_compatible R1 → - ∀L1,L2,V. L1 ⪤*[R1, V] L2 → ∀I,T. - ∃∃L. L1 ⪤*[R1, ②{I}V.T] L & L ⪤*[R2, V] L2. -#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #V * #f #Hf #HL12 * [ #p ] #I #T -[ elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg - elim (frees_inv_bind … Hg) #y1 #y2 #H #_ #Hy -| elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg - elim (frees_inv_flat … Hg) #y1 #y2 #H #_ #Hy -] -lapply(frees_mono … H … Hf) -H #H1 -lapply (sor_eq_repl_back1 … Hy … H1) -y1 #Hy -lapply (sor_inv_sle_sn … Hy) -y2 #Hfg -elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 -lapply (sle_lexs_trans … HL1 … Hfg) // #H -elim (frees_lexs_conf … Hf … H) -Hf -H -/4 width=7 by sle_lexs_trans, ex2_intro/ -qed-. - -lemma lfxs_flat_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lfxs_fsle_compatible R1 → - ∀L1,L2,T. L1 ⪤*[R1, T] L2 → ∀I,V. - ∃∃L. L1 ⪤*[R1, ⓕ{I}V.T] L & L ⪤*[R2, T] L2. -#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #I #V -elim (frees_total L1 (ⓕ{I}V.T)) #g #Hg -elim (frees_inv_flat … Hg) #y1 #y2 #_ #H #Hy -lapply(frees_mono … H … Hf) -H #H2 -lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy -lapply (sor_inv_sle_dx … Hy) -y1 #Hfg -elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #L #HL1 #HL2 -lapply (sle_lexs_trans … HL1 … Hfg) // #H -elim (frees_lexs_conf … Hf … H) -Hf -H -/4 width=7 by sle_lexs_trans, ex2_intro/ -qed-. - -lemma lfxs_bind_dx_split: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lfxs_fsle_compatible R1 → - ∀I,L1,L2,V1,T. L1.ⓑ{I}V1 ⪤*[R1, T] L2 → ∀p. - ∃∃L,V. L1 ⪤*[R1, ⓑ{p,I}V1.T] L & L.ⓑ{I}V ⪤*[R2, T] L2 & R1 L1 V1 V. -#R1 #R2 #HR1 #HR2 #HR #I #L1 #L2 #V1 #T * #f #Hf #HL12 #p -elim (frees_total L1 (ⓑ{p,I}V1.T)) #g #Hg -elim (frees_inv_bind … Hg) #y1 #y2 #_ #H #Hy -lapply(frees_mono … H … Hf) -H #H2 -lapply (tl_eq_repl … H2) -H2 #H2 -lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy -lapply (sor_inv_sle_dx … Hy) -y1 #Hfg -lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg -elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 -lapply (sle_lexs_trans … H … Hfg) // #H0 -elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H -elim (ext2_inv_pair_sn … H) -H #V #HV #H1 #H2 destruct -elim (frees_lexs_conf … Hf … H0) -Hf -H0 -/4 width=7 by sle_lexs_trans, ex3_2_intro, ex2_intro/ -qed-. - -lemma lfxs_bind_dx_split_void: ∀R1,R2. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → - lfxs_fsle_compatible R1 → - ∀L1,L2,T. L1.ⓧ ⪤*[R1, T] L2 → ∀p,I,V. - ∃∃L. L1 ⪤*[R1, ⓑ{p,I}V.T] L & L.ⓧ ⪤*[R2, T] L2. -#R1 #R2 #HR1 #HR2 #HR #L1 #L2 #T * #f #Hf #HL12 #p #I #V -elim (frees_total L1 (ⓑ{p,I}V.T)) #g #Hg -elim (frees_inv_bind_void … Hg) #y1 #y2 #_ #H #Hy -lapply(frees_mono … H … Hf) -H #H2 -lapply (tl_eq_repl … H2) -H2 #H2 -lapply (sor_eq_repl_back2 … Hy … H2) -y2 #Hy -lapply (sor_inv_sle_dx … Hy) -y1 #Hfg -lapply (sle_inv_tl_sn … Hfg) -Hfg #Hfg -elim (lexs_sle_split (cext2 R1) (cext2 R2) … HL12 … Hfg) -HL12 /2 width=1 by ext2_refl/ #Y #H #HL2 -lapply (sle_lexs_trans … H … Hfg) // #H0 -elim (lexs_inv_next1 … H) -H #Z #L #HL1 #H -elim (ext2_inv_unit_sn … H) -H #H destruct -elim (frees_lexs_conf … Hf … H0) -Hf -H0 -/4 width=7 by sle_lexs_trans, ex2_intro/ (* note: 2 ex2_intro *) -qed-. - (* Main properties **********************************************************) (* Basic_2A1: uses: llpx_sn_bind llpx_sn_bind_O *) @@ -168,35 +63,6 @@ lapply (lexs_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫱f2)) /3 width=7 by frees_fwd_isfin, frees_bind_void, lexs_join, isfin_tl, ex2_intro/ qed. -theorem lfxs_conf: ∀R1,R2. - lfxs_fsle_compatible R1 → - lfxs_fsle_compatible R2 → - R_confluent2_lfxs R1 R2 R1 R2 → - ∀T. confluent2 … (lfxs R1 T) (lfxs R2 T). -#R1 #R2 #HR1 #HR2 #HR12 #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02 -lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12 -lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01 -elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] -[ #L #HL1 #HL2 - elim (frees_lexs_conf … Hf … HL01) // -HR1 -HL01 #f1 #Hf1 #H1 - elim (frees_lexs_conf … Hf … HL02) // -HR2 -HL02 #f2 #Hf2 #H2 - lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1 - lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2 - /3 width=5 by ex2_intro/ -| #g * #I0 [2: #V0 ] #K0 #n #HLK0 #Hgf #Z1 #H1 #Z2 #H2 #K1 #HK01 #K2 #HK02 - [ elim (ext2_inv_pair_sn … H1) -H1 #V1 #HV01 #H destruct - elim (ext2_inv_pair_sn … H2) -H2 #V2 #HV02 #H destruct - elim (frees_inv_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0 - lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01 - lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02 - elim (HR12 … HV01 … HV02 K1 … K2) /3 width=3 by ext2_pair, ex2_intro/ - | lapply (ext2_inv_unit_sn … H1) -H1 #H destruct - lapply (ext2_inv_unit_sn … H2) -H2 #H destruct - /3 width=3 by ext2_unit, ex2_intro/ - ] -] -qed-. - theorem lfxs_trans_gen: ∀R1,R2,R3. c_reflexive … R1 → c_reflexive … R2 → lfxs_confluent R1 R2 → lfxs_transitive R1 R2 R3 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma index 3c91aa716..55e6e3472 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma @@ -75,6 +75,18 @@ qed. (* Basic inversion lemmas ***************************************************) +lemma append_inv_atom3_sn: ∀L,K. ⋆ = L @@ K → ∧∧ ⋆ = L & ⋆ = K. +#L * /2 width=1 by conj/ +#K #I >append_bind #H destruct +qed-. + +lemma append_inv_bind3_sn: ∀I0,L,L0,K. L0.ⓘ{I0} = L @@ K → + ∨∨ ∧∧ L0.ⓘ{I0} = L & ⋆ = K + | ∃∃K0. K = K0.ⓘ{I0} & L0 = L @@ K0. +#I0 #L #L0 * /3 width=1 by or_introl, conj/ +#K #I >append_bind #H destruct /3 width=3 by ex2_intro, or_intror/ +qed-. + lemma append_inj_sn: ∀K,L1,L2. L1@@K = L2@@K → L1 = L2. #K elim K -K // #K #I #IH #L1 #L2 >append_bind #H 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 13c02988a..3f4cb8fbf 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 @@ -66,7 +66,7 @@ table { class "blue" [ { "rt-conversion" * } { [ { "context-sensitive parallel r-conversion" * } { - [ [ "for terms" ] "cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ] + [ [ "for terms" ] "cpc" + "( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ] } ] } @@ -107,13 +107,14 @@ table { ] *) [ { "uncounted context-sensitive parallel rt-computation" * } { - [ [ "refinement for lenvs" ] "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] - [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] - [ [ "strongly normalizing for term vectors" ] "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] - [ [ "strongly normalizing for terms" ] "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] - [ [ "for lenvs on referred entries" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] - [ [ "for lenvs on all entries" ] "lpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? )" * ] - [ [ "for terms" ] "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] + [ [ "refinement for lenvs" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] + [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] + [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] + [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] + [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] + [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" * ] + [ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] + [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } @@ -121,30 +122,30 @@ table { class "cyan" [ { "rt-transition" * } { [ { "uncounted parallel rst-transition" * } { - [ [ "for closures" ] "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] - [ [ "proper for closures" ] "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] + [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] + [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] } ] [ { "context-sensitive parallel r-transition" * } { - [ [ "for lenvs on referred entries" ] "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] - [ [ "for binders" ] "cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ] - [ [ "for terms" ] "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ] + [ [ "for lenvs on referred entries" ] "lfpr" + "( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] + [ [ "for binders" ] "cpr_ext" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ] + [ [ "for terms" ] "cpr" + "( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ] } ] [ { "t-bound context-sensitive parallel rt-transition" * } { - [ [ "for terms" ] "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ] + [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_cpx" * ] } ] [ { "uncounted context-sensitive parallel rt-transition" * } { - [ [ "normal form for terms" ] "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] - [ [ "for lenvs on referred entries" ] "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ] - [ [ "for lenvs on all entries" ] "lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ] - [ [ "for binders" ] "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] - [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfeq" * ] + [ [ "normal form for terms" ] "cnx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] + [ [ "for lenvs on referred entries" ] "lfpx" + "( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ] + [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ] + [ [ "for binders" ] "cpx_ext" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] + [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" * ] } ] [ { "counted context-sensitive parallel rt-transition" * } { - [ [ "for terms" ] "cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ] + [ [ "for terms" ] "cpg" + "( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ] } ] } @@ -152,7 +153,7 @@ table { class "water" [ { "iterated static typing" * } { [ { "iterated generic extension of a context-sensitive relation" * } { - [ [ "for lenvs on referred entries" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] + [ [ "for lenvs on referred entries" ] "tc_lfxs" + "( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] } ] } @@ -160,37 +161,37 @@ table { class "green" [ { "static typing" * } { [ { "generic reducibility" * } { - [ [ "restricted refinement for lenvs" ] "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] - [ [ "candidates" ] "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] + [ [ "restricted refinement for lenvs" ] "lsubc" + "( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] + [ [ "candidates" ] "gcp_cr" + "( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] [ [ "computation properties" ] "gcp" *] } ] [ { "atomic arity assignment" * } { - [ [ "restricted refinement for lenvs" ] "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] - [ [ "for terms" ] "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ] + [ [ "restricted refinement for lenvs" ] "lsuba" + "( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] + [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ] } ] [ { "degree-based equivalence" * } { - [ [ "for closures on referred entries" ] "ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] - [ [ "for lenvs on referred entries" ] "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] + [ [ "for closures on referred entries" ] "ffdeq" + "( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] + [ [ "for lenvs on referred entries" ] "lfdeq" + "( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] } ] [ { "syntactic equivalence" * } { - [ [ "for lenvs on referred entries" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ] + [ [ "for lenvs on referred entries" ] "lfeq" + "( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ] } ] [ { "generic extension of a context-sensitive relation" * } { - [ [ "for lenvs on referred entries" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_lex" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] + [ [ "for lenvs on referred entries" ] "lfxs" + "( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_lex" + "lfxs_drops" + "lfxs_fqup" + "lfxs_fsle" + "lfxs_lfxs" * ] } ] [ { "context-sensitive free variables" * } { - [ [ "inclusion for restricted closures" ] "fle ( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fle_drops" + "fle_fqup" + "fle_fle" * ] - [ [ "restricted refinement for lenvs" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ] - [ [ "for terms" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ] + [ [ "inclusion for restricted closures" ] "fsle" + "( ⦃?,?⦄ ⊆ ⦃?,?⦄ )" "fsle_length" + "fsle_drops" + "fsle_fqup" + "fsle_fsle" * ] + [ [ "restricted refinement for lenvs" ] "lsubf" + "( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ] + [ [ "for terms" ] "frees" + "( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_append" + "frees_drops" + "frees_fqup" + "frees_frees" * ] } ] [ { "local environments" * } { - [ [ "restricted refinement" ] "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ] + [ [ "restricted refinement" ] "lsubr" + "( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ] } ] } @@ -198,8 +199,8 @@ table { class "grass" [ { "s-computation" * } { [ { "iterated structural successor" * } { - [ [ "for closures" ] "fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ] - [ [ "proper for closures" ] "fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ] + [ [ "for closures" ] "fqus" + "( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ] + [ [ "proper for closures" ] "fqup" + "( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ] } ] } @@ -207,8 +208,8 @@ table { class "yellow" [ { "s-transition" * } { [ { "structural successor" * } { - [ [ "for closures" ] "fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ] - [ [ "proper for closures" ] "fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ] + [ [ "for closures" ] "fquq" + "( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ] + [ [ "proper for closures" ] "fqu" + "( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ] } ] } @@ -216,22 +217,22 @@ table { class "orange" [ { "relocation" * } { [ { "generic slicing" * } { - [ [ "for lenvs" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ] + [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≡ ? )" + "( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ] } ] [ { "generic relocation" * } { - [ [ "for binders" ] "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] - [ [ "for term vectors" ] "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ] - [ [ "for terms" ] "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ] + [ [ "for binders" ] "lifts_bind" + "( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] + [ [ "for term vectors" ] "lifts_vector" + "( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ] + [ [ "for terms" ] "lifts" + "( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ] } ] [ { "syntactic equivalence" * } { - [ [ "for lenvs on selected entries" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ] + [ [ "for lenvs on selected entries" ] "lreq" + "( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ] } ] [ { "generic entrywise extension" * } { - [ [ "for lenvs of one contex-sensitive relation" ] "lex ( ? ⦻[?] ? )" "lex_tc" * ] - [ [ "for lenvs of two contex-sensitive relations" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ] + [ [ "for lenvs of one contex-sensitive relation" ] "lex" + "( ? ⦻[?] ? )" "lex_tc" + "lex_length" * ] + [ [ "for lenvs of two contex-sensitive relations" ] "lexs" + "( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ] } ] } @@ -239,25 +240,25 @@ table { class "red" [ { "syntax" * } { [ { "equivalence up to exclusion binders" * } { - [ [ "for lenvs" ] "lveq ( ? ≋ⓧ*[?,?] ? )" "lveq_length" + "lveq_lveq" * ] + [ [ "for lenvs" ] "lveq" + "( ? ≋ⓧ*[?,?] ? )" "lveq_length" + "lveq_lveq" * ] } ] [ { "append" * } { - [ [ "for lenvs" ] "append ( ? @@ ? )" "append_length" * ] + [ [ "for lenvs" ] "append" + "( ? @@ ? )" "append_length" * ] } ] [ { "head equivalence" * } { - [ [ "for terms" ] "theq ( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] + [ [ "for terms" ] "theq" + "( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] } ] [ { "degree-based equivalence" * } { - [ [ "" ] "tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )" * ] - [ [ "" ] "tdeq ( ? ≛[?,?] ? )" "tdeq_tdeq" * ] + [ [ "" ] "tdeq_ext" + "( ? ≛[?,?] ? )" + "( ? ⊢ ? ≛[?,?] ? )" * ] + [ [ "" ] "tdeq" + "( ? ≛[?,?] ? )" "tdeq_tdeq" * ] } ] [ { "closures" * } { - [ [ "" ] "cl_weight ( ♯{?,?,?} )" * ] - [ [ "" ] "cl_restricted_weight ( ♯{?,?} )" * ] + [ [ "" ] "cl_weight" + "( ♯{?,?,?} )" * ] + [ [ "" ] "cl_restricted_weight" + "( ♯{?,?} )" * ] } ] [ { "global environments" * } { @@ -267,8 +268,8 @@ table { [ { "local environments" * } { [ [ "" ] "ceq_ext" "ceq_ext_ceq_ext" * ] [ [ "" ] "cext2" * ] - [ [ "" ] "lenv_length ( |?| )" * ] - [ [ "" ] "lenv_weight ( ♯{?} )" * ] + [ [ "" ] "lenv_length" + "( |?| )" * ] + [ [ "" ] "lenv_weight" + "( ♯{?} )" * ] [ [ "" ] "lenv" * ] } ] @@ -278,9 +279,9 @@ table { } ] [ { "terms" * } { - [ [ "" ] "term_vector ( Ⓐ?.? )" * ] - [ [ "" ] "term_simple ( 𝐒⦃?⦄ )" * ] - [ [ "" ] "term_weight ( ♯{?} )" * ] + [ [ "" ] "term_vector" + "( Ⓐ?.? )" * ] + [ [ "" ] "term_simple" + "( 𝐒⦃?⦄ )" * ] + [ [ "" ] "term_weight" + "( ♯{?} )" * ] [ [ "" ] "term" * ] } ]