From: Ferruccio Guidi Date: Fri, 24 Nov 2017 12:29:14 +0000 (+0000) Subject: - lpx and lpxs restored to prove equivalene between lfpxs and lpxs + lfeq X-Git-Tag: make_still_working~399 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d7c5846e4a362a366f5600d079e08f8a75b9d566 - lpx and lpxs restored to prove equivalene between lfpxs and lpxs + lfeq - Makefile: number of objects and intrinsic loss factor added in summary for web page - basic_2_src.tbl: more descriptions --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 6bb435082..e5a76486a 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -192,7 +192,9 @@ define SUMMARY_TEMPLATE $$(SUM_$(1)): C0 = $$(shell cat $(1)/$(1)_probe.txt) $$(SUM_$(1)): S1 = $$(word 1, $$(C0)) $$(SUM_$(1)): S2 = $$(word 2, $$(C0)) + $$(SUM_$(1)): S3 = $$(word 3, $$(C0)) $$(SUM_$(1)): S4 = $$(word 4, $$(C0)) + $$(SUM_$(1)): S5 = $$(shell printf "%.1f" `echo "scale=2;$$(S4)/$$(S2)"|bc`) $$(SUM_$(1)): C1 = $$(word 5, $$(C0)) $$(SUM_$(1)): C2 = $$(word 7, $$(C0)) $$(SUM_$(1)): C3 = $$(shell echo "$$(C1)+$$(C2)"|bc) @@ -200,32 +202,32 @@ define SUMMARY_TEMPLATE $$(SUM_$(1)): P2 = $$(word 9, $$(C0)) $$(SUM_$(1)): P3 = $$(shell echo "$$(P1)+$$(P2)"|bc) - $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt + $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt Makefile @printf ' SUMMARY $(1)\n' - @printf 'name "$$(basename $$(@F))"\n\n' > $$@ - @printf 'table {\n' >> $$@ - @printf ' class "gray" [ "category"\n' >> $$@ - @printf ' [ "objects" * ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf ' class "water" [ "sizes"\n' >> $$@ - @printf ' [ "files" "$$(S1)" ]\n' >> $$@ - @printf ' [ "characters" "$$(S2)" ]\n' >> $$@ - @printf ' [ "nodes" "$$(S4)" ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf ' class "green" [ "propositions"\n' >> $$@ - @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ - @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@ - @printf ' [ "total" "$$(P3)" ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf ' class "grass" [ "concepts"\n' >> $$@ - @printf ' [ "declared" "$$(C1)" ]\n' >> $$@ - @printf ' [ "defined" "$$(C2)" ]\n' >> $$@ - @printf ' [ "total" "$$(C3)" ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf '}\n\n' >> $$@ - @printf 'class "capitalize italic" { 0 }\n\n' >> $$@ - @printf 'class "italic" { 1 } { 3 } { 5 }\n\n' >> $$@ - @printf 'class "right italic" { 2 } { 4 } { 6 }\n' >> $$@ + @printf 'name "$$(basename $$(@F))"\n\n' > $$@ + @printf 'table {\n' >> $$@ + @printf ' class "gray" [ "category"\n' >> $$@ + @printf ' [ "units" * ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "water" [ "sizes"\n' >> $$@ + @printf ' [ "characters (files)" "$$(S2) ($$(S1))" ]\n' >> $$@ + @printf ' [ "nodes (objects)" "$$(S4) ($$(S3))" ]\n' >> $$@ + @printf ' [ "intrinsic loss factor" "$$(S5)" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "green" [ "propositions"\n' >> $$@ + @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ + @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@ + @printf ' [ "total" "$$(P3)" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "grass" [ "concepts"\n' >> $$@ + @printf ' [ "declared" "$$(C1)" ]\n' >> $$@ + @printf ' [ "defined" "$$(C2)" ]\n' >> $$@ + @printf ' [ "total" "$$(C3)" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf '}\n\n' >> $$@ + @printf 'class "capitalize italic" { 0 }\n\n' >> $$@ + @printf 'class "italic" { 1 } { 3 } { 5 }\n\n' >> $$@ + @printf 'class "right italic" { 2 } { 4 } { 6 }\n' >> $$@ .PHONY: $$(SUM_$(1)) endef diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_4.ma new file mode 100644 index 000000000..5c028b6d2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysn_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈[ break term 46 h ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedTySn $h $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_4.ma new file mode 100644 index 000000000..b6e63229e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈*[ break term 46 h ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedTySnStar $h $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma index 5c8b23e55..3067deb2a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma @@ -31,3 +31,45 @@ interpretation "generic extension (local environment)" (* Basic_2A1: was: lpx_sn_refl *) lemma lex_refl: ∀R. c_reflexive … R → reflexive … (lex R). /4 width=3 by lexs_refl, ext2_refl, ex2_intro/ qed. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_2A1: was: lpx_sn_inv_atom1: *) +lemma lex_inv_atom_sn: ∀R,L2. ⋆ ⪤[R] L2 → L2 = ⋆. +#R #L2 * #f #Hf #H >(lexs_inv_atom1 … H) -L2 // +qed-. + +(* Basic_2A1: was: lpx_sn_inv_pair1 *) +lemma lex_inv_pair_sn: ∀R,I,L2,K1,V1. K1.ⓑ{I}V1 ⪤[R] L2 → + ∃∃K2,V2. K1 ⪤[R] K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2. +#R #I #L2 #K1 #V1 * #f #Hf #H +lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H +elim (lexs_inv_push1 … H) -H #Z2 #K2 #HK12 #HZ2 #H destruct +elim (ext2_inv_pair_sn … HZ2) -HZ2 #V2 #HV12 #H destruct +/3 width=5 by ex3_2_intro, ex2_intro/ +qed-. + +(* Basic_2A1: was: lpx_sn_inv_atom2 *) +lemma lex_inv_atom_dx: ∀R,L1. L1 ⪤[R] ⋆ → L1 = ⋆. +#R #L1 * #f #Hf #H >(lexs_inv_atom2 … H) -L1 // +qed-. + +(* Basic_2A1: was: lpx_sn_inv_pair2 *) +lemma lex_inv_pair_dx: ∀R,I,L1,K2,V2. L1 ⪤[R] K2.ⓑ{I}V2 → + ∃∃K1,V1. K1 ⪤[R] K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1. +#R #I #L1 #K2 #V2 * #f #Hf #H +lapply (lexs_eq_repl_fwd … H (↑f) ?) -H /2 width=1 by eq_push_inv_isid/ #H +elim (lexs_inv_push2 … H) -H #Z1 #K1 #HK12 #HZ1 #H destruct +elim (ext2_inv_pair_dx … HZ1) -HZ1 #V1 #HV12 #H destruct +/3 width=5 by ex3_2_intro, ex2_intro/ +qed-. + +(* Advanced inversion lemmas ************************************************) + +(* Basic_2A1: was: lpx_sn_inv_pair *) +lemma lex_inv_pair: ∀R,I1,I2,L1,L2,V1,V2. + L1.ⓑ{I1}V1 ⪤[R] L2.ⓑ{I2}V2 → + ∧∧ L1 ⪤[R] L2 & R L1 V1 V2 & I1 = I2. +#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lex_inv_pair_sn … H) -H +#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma new file mode 100644 index 000000000..98f23aff9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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/i_static/tc_lfxs_lex.ma". +include "basic_2/rt_transition/lfpx_frees.ma". +include "basic_2/rt_computation/lpxs.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +(* Properties with uncounted parallel rt-computation for local environments *) + +lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → + ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by tc_lfxs_lex_lfeq/ qed. + +(* Inversion lemmas with uncounted parallel rt-computation for local envs ***) + +lemma lpx_cpxs_ext_trans: ∀h,G. s_rs_transitive_isid cfull (cpx_ext h G). +#H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 + + +lemma tc_lfxs_inv_lex_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → + ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2. +#h #G @tc_lfxs_inv_lex_lfeq // +[ @lfpx_frees_conf +| @lpx_cpxs_ext_trans \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma new file mode 100644 index 000000000..d520aa6c2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/predtysnstar_4.ma". +include "basic_2/relocation/lex.ma". +include "basic_2/rt_computation/cpxs.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************) + +definition lpxs: ∀h. relation3 genv lenv lenv ≝ + λh,G. lex (cpxs h G). + +interpretation + "uncounted parallel rt-computation (local environment)" + 'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2). 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 acdc797e9..66da92c66 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,5 @@ 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_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma +lpxs.ma lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.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/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma new file mode 100644 index 000000000..cde540dcc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx.ma @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/predtysn_4.ma". +include "basic_2/relocation/lex.ma". +include "basic_2/rt_transition/cpx.ma". + +(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENVIRONMENTS ******************) + +definition lpx: sh → genv → relation lenv ≝ + λh,G. lex (cpx h G). + +interpretation + "uncounted parallel rt-transition (local environment)" + 'PRedTySn h G L1 L2 = (lpx h G L1 L2). + +(* Basic properties *********************************************************) + +(* +lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ⬈[h] K2 → ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 → + ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2. +/2 width=1 by lpx_sn_pair/ qed. +*) + +lemma lpx_refl: ∀h,G. reflexive … (lpx h G). +/2 width=1 by lex_refl/ qed. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_2A1: was: lpx_inv_atom1 *) +lemma lpx_inv_atom_sn: ∀h,G,L2. ⦃G, ⋆⦄ ⊢ ⬈[h] L2 → L2 = ⋆. +/2 width=2 by lex_inv_atom_sn/ qed-. + +(* Basic_2A1: was: lpx_inv_pair1 *) +lemma lpx_inv_pair_sn: ∀h,I,G,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈[h] L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 & + L2 = K2.ⓑ{I}V2. +/2 width=1 by lex_inv_pair_sn/ qed-. + +(* Basic_2A1: was: lpx_inv_atom2 *) +lemma lpx_inv_atom_dx: ∀h,G,L1. ⦃G, L1⦄ ⊢ ⬈[h] ⋆ → L1 = ⋆. +/2 width=2 by lex_inv_atom_dx/ qed-. + +(* Basic_2A1: was: lpx_inv_pair2 *) +lemma lpx_inv_pair2_dx: ∀h,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ⬈[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 & + L1 = K1.ⓑ{I}V1. +/2 width=1 by lex_inv_pair_dx/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lpx_inv_pair: ∀h,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ⬈[h] L2.ⓑ{I2}V2 → + ∧∧ ⦃G, L1⦄ ⊢ ⬈[h] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 & I1 = I2. +/2 width=1 by lex_inv_pair/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index c2bfdf883..bfc628f28 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 @@ -108,10 +108,11 @@ table { *) [ { "uncounted context-sensitive parallel rt-computation" * } { [ [ "refinement for lenvs" ] "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] - [ [ "strongly normalizing on referred entries for lenvs" ] "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] + [ [ "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" * ] - [ [ "on referred entries for lenvs" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] + [ [ "for lenvs on referred entries" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "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_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] @@ -137,6 +138,7 @@ table { [ { "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_frees" + "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" * ] } @@ -149,8 +151,8 @@ table { ] class "water" [ { "iterated static typing" * } { - [ { "iterated extension on referred entries" * } { - [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_lex" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] + [ { "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" * ] } ] } @@ -158,54 +160,54 @@ table { class "green" [ { "static typing" * } { [ { "generic reducibility" * } { - [ [ "" ] "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] - [ [ "" ] "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] - [ [ "" ] "gcp" *] + [ [ "restricted refinement for lenvs" ] "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] + [ [ "candidates" ] "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] + [ [ "computation properties" ] "gcp" *] } ] [ { "atomic arity assignment" * } { - [ [ "" ] "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] - [ [ "" ] "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 on referred entries" * } { - [ [ "" ] "ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] - [ [ "" ] "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] + [ { "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" * ] } ] - [ { "syntactic equivalence on referred entries" * } { - [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ] + [ { "syntactic equivalence" * } { + [ [ "for lenvs on referred entries" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" + "lfeq_lfeq" * ] } ] - [ { "generic extension on referred entries" * } { - [ [ "" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] + [ { "generic extension of a context-sensitive relation" * } { + [ [ "for lenvs on referred entries" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] } ] [ { "context-sensitive free variables" * } { - [ [ "" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ] - [ [ "" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ] + [ [ "restricted refinement for lenvs" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ] + [ [ "for terms" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ] } ] - [ { "restricted ref. for local env." * } { - [ [ "" ] "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ] + [ { "local environments" * } { + [ [ "restricted refinement" ] "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ] } ] } ] class "grass" [ { "s-computation" * } { - [ { "iterated structural successor for closures" * } { - [ [ "" ] "fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ] - [ [ "" ] "fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ] + [ { "iterated structural successor" * } { + [ [ "for closures" ] "fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ] + [ [ "proper for closures" ] "fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ] } ] } ] class "yellow" [ { "s-transition" * } { - [ { "structural successor for closures" * } { - [ [ "" ] "fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ] - [ [ "" ] "fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ] + [ { "structural successor" * } { + [ [ "for closures" ] "fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ] + [ [ "proper for closures" ] "fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ] } ] }