update in basic_2

[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 11112816b08512a2afad239d6fad073a23b0a808..ff9b216278ece0c67338780b15bda9f3916708f4 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
@@ -84,13 +84,17 @@ table {
           }
         ]
 *)
-        [ { "uncounted context-sensitive parallel rst-computation" * } {
+        [ { "t-bound context-sensitive parallel rt-computation" * } {
+             [ [ "for terms" ] "cpms" + "( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" * ]
+          }
+        ]
+        [ { "unbound context-sensitive parallel rst-computation" * } {
              [ [ "strongly normalizing for closures" ] "fsb" + "( ≥[?,?] 𝐒⦃?,?,?⦄ )" "fsb_ffdeq" + "fsb_aaa" + "fsb_csx" + "fsb_fpbg" * ]
              [ [ "proper for closures" ] "fpbg" + "( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_fqup" + "fpbg_cpxs" + "fpbg_lfpxs" + "fpbg_fpbs" + "fpbg_fpbg" * ]
              [ [ "for closures" ] "fpbs" + "( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_fqup" + "fpbs_fqus" + "fpbs_aaa" + "fpbs_cpx" + "fpbs_fpb" + "fpbs_cpxs" + "fpbs_lpxs" + "fpbs_lfpxs" + "fpbs_csx" + "fpbs_fpbs" * ]
           }
         ]
-        [ { "uncounted context-sensitive parallel rt-computation" * } {
+        [ { "unbound context-sensitive parallel rt-computation" * } {
              [ [ "refinement for lenvs on selected entries" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
              [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
              [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
@@ -105,7 +109,7 @@ table {
    ]
    class "cyan"
    [ { "rt-transition" * } {
-        [ { "uncounted parallel rst-transition" * } {
+        [ { "unbound parallel rst-transition" * } {
              [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_aaa" + "fpbq_fpb" * ]
              [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" + "fpb_ffdeq" * ]
           }
@@ -120,7 +124,7 @@ table {
              [ [ "for terms" ] "cpm" + "( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_fsle" + "cpm_cpx" * ]
           }
         ]
-        [ { "uncounted context-sensitive parallel rt-transition" * } {
+        [ { "unbound 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_fquq" + "lfpx_fqup" + "lfpx_fsle" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lpx" + "lfpx_lfpx" * ]
              [ [ "for lenvs on all entries" ] "lpx" + "( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ]
@@ -128,7 +132,7 @@ table {
              [ [ "for terms" ] "cpx" + "( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfeq" + "cpx_lfdeq" + "cpx_ffdeq" * ]
           }
         ]
-        [ { "counted context-sensitive parallel rt-transition" * } {
+        [ { "bound context-sensitive parallel rt-transition" * } {
              [ [ "for terms" ] "cpg" + "( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
           }
         ]
@@ -201,7 +205,7 @@ 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_ctc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
           }
         ]
         [ { "generic relocation" * } {
@@ -228,7 +232,7 @@ table {
           }
         ]
         [ { "append" * } {
-             [ [ "for lenvs" ] "append" + "( ? @@ ? )" "append_length" * ]
+             [ [ "for lenvs" ] "append" + "( ? + ? )" "append_length" * ]
           }
         ]
         [ { "head equivalence" * } {
@@ -246,6 +250,8 @@ table {
           }
         ]
         [ { "global environments" * } {
+             [ [ "" ] "genv_length" + "( |?| )" * ]
+             [ [ "" ] "genv_weight" + "( ♯{?} )" * ]
              [ [ "" ] "genv" * ]
           }
         ]