- some commutations between the rt-steps and the s-steps proved

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl

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 14974f02be078c91dfeb0fe92035ba978816f23a..d98e42c5cd95ec75e1b07a5179f91373b7ec9125 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -138,20 +138,20 @@ table {
           }
         ]
         [ { "context-sensitive rt-reduction" * } {
-             [ "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ]
-             [ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ]
+             [ "lpx_lleq" * ]
+             [ "cpx_lreq" + "cpx_llpx_sn" + "cpx_lleq" * ]
           }
         ]
 *)
         [ { "t-bound context-sensitive rt-transition" * } {
-             [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_lfpx" + "lfpr_lfpr" * ]
+             [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]
              [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" (* + "cpr_llpx_sn" + "cpr_cir" *) * ]
              [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_cpx" * ]
           }
         ]
         [ { "uncounted context-sensitive rt-transition" * } {
-             [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" * ]
-             [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
+             [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ]
+             [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" * ]
           }
         ]
         [ { "counted context-sensitive rt-transition" * } {
@@ -162,24 +162,20 @@ table {
    ]
    class "green"
    [ { "static typing" * } {
-        [ { "parameters" * } {
-             [ "sh" "sd" * ]
-          }
-        ]
         [ { "restricted ref. for atomic arity assignment" * } {
              [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
           }
         ]
         [ { "atomic arity assignment" * } {
-             [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfeq" + "aaa_aaa" * ]
+             [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
           }
         ]
-        [ { "equivalence for closures on referred entries" * } {
-             [ "ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )" "ffeq_freq" * ]
+        [ { "degree-based equivalence for closures on referred entries" * } {
+             [ "ffdeq ( ⦃?,?,?⦄ ≡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
           }
         ]
-        [ { "equivalence for local environments on referred entries" * } {
-             [ "lfeq ( ? ≡[?] ? )" "lfeq_length" + "lfeq_lreq" + "lfeq_fqup" + "lfeq_lfeq" * ]
+        [ { "degree-based equivalence for local environments on referred entries" * } {
+             [ "lfdeq ( ? ≡[?,?,?] ? )" "lfdeq_length" + "lfdeq_fqup" + "lfdeq_lfdeq" * ]
           }
         ]
         [ { "generic extension on referred entries" * } {
@@ -191,7 +187,7 @@ table {
           }
         ]        
         [ { "context-sensitive free variables" * } {
-             [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_drops" + "frees_fqup" + "frees_fqus" + "frees_frees" * ]
+             [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_drops" + "frees_fqup" + "frees_frees" * ]
           }
         ]
         [ { "restricted ref. for local env." * } {
@@ -227,7 +223,7 @@ table {
         ]
         [ { "generic relocation for terms" * } {
              [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ]
-             [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_lifts" * ]
+             [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]
           }
         ]
         [ { "ranged equivalence for local environments" * } {
@@ -241,13 +237,13 @@ table {
      }
    ]
    class "red"
-   [ { "grammar" * } {
+   [ { "syntax" * } {
         [ { "append for local environments" * } {
              [ "append ( ? @@ ? )" "append_length" * ]
           }
         ]
-        [ { "context-sensitive equivalences for terms" * } {
-             [ "ceq" "ceq_ceq" * ]
+        [ { "degree-based equivalence for terms" * } {
+             [ "deq ( ? ≡[?,?] ? ) " "deq_deq" * ]
           }
         ]
         [ { "same top term structure" * } {
@@ -255,17 +251,34 @@ table {
           }
         ]
         [ { "closures" * } {
-             [ "cl_weight ( ♯{?,?,?} )" "cl_restricted_weight ( ♯{?,?} )" * ]
+             [ "cl_weight ( ♯{?,?,?} )" * ]
+             [ "cl_restricted_weight ( ♯{?,?} )" * ]
           }
         ]
-        [ { "internal syntax" * } {
+        [ { "global environments" * } {
              [ "genv" * ]
-             [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" * ]
-             [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector ( Ⓐ?.? )" * ]
+          }
+        ]
+        [ { "local environments" * } {
+             [ "lenv_length ( |?| )" * ]
+             [ "lenv_weight ( ♯{?} )" * ]
+             [ "lenv" * ]
+          }
+        ]
+        [ { "terms" * } {
+             [ "term_vector ( Ⓐ?.? )" * ]
+             [ "term_simple ( 𝐒⦃?⦄ )"  * ]
+             [ "term_weight ( ♯{?} )" * ]
+             [ "term" * ]
+          }
+        ]
+        [ { "items" * } {
+             [ "item_sd" * ]
+             [ "item_sh" * ]
              [ "item" * ]
           }
         ]
-        [ { "external syntax" * } {
+        [ { "atomic arities" * } {
              [ "aarity" * ]
           }
         ]