- ext2_tc added

[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 8ff7a521fcb2f95969a1744d2c6a633ffef0e923..4f947c2dccfbcedca4b021cef17eff4d5e973632 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
@@ -87,13 +87,12 @@ table {
           }
         ]
         [ { "strongly normalizing rt-computation" * } {
-             [ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
              [ "llsx_csx" * ]
              [ "csx_fpbs" * ]
           }
         ]
         [ { "parallel qrst-computation" * } {
-             [ "fpbg ( â¦\83?,?,?â¦\84 >â\89¡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
+             [ "fpbg ( â¦\83?,?,?â¦\84 >â\89\9b[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
              [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ]
           }
         ]
@@ -106,8 +105,9 @@ table {
              [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
           }
         ]
-*)        
+*)
         [ { "uncounted context-sensitive rt-computation" * } {
+             [ "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
              [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
              [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ]
              [ "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" * ]
@@ -166,8 +166,8 @@ table {
           }
         ]
         [ { "degree-based equivalence on referred entries" * } {
-             [ "ffdeq ( â¦\83?,?,?â¦\84 â\89¡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
-             [ "lfdeq ( ? â\89¡[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
+             [ "ffdeq ( â¦\83?,?,?â¦\84 â\89\9b[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
+             [ "lfdeq ( ? â\89\9b[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
           }
         ]
         [ { "generic extension on referred entries" * } {
@@ -221,7 +221,7 @@ table {
           }
         ]
         [ { "generic entrywise extension" * } {
-             [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_length" + "lexs_lexs" * ]
+             [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
           }
         ]
      }
@@ -237,8 +237,8 @@ table {
           }
         ]
         [ { "degree-based equivalence" * } {
-             [ "tdeq_ext ( ? â\89¡[?,?] ? ) ( ? â\8a¢ ? â\89¡[?,?] ? )" * ]
-             [ "tdeq ( ? â\89¡[?,?] ? )" "tdeq_tdeq" * ]
+             [ "tdeq_ext ( ? â\89\9b[?,?] ? ) ( ? â\8a¢ ? â\89\9b[?,?] ? )" * ]
+             [ "tdeq ( ? â\89\9b[?,?] ? )" "tdeq_tdeq" * ]
           }
         ]
         [ { "closures" * } {
@@ -258,7 +258,7 @@ table {
           }
         ]
         [ { "binders for local environments" * } {
-             [ "ext2" "ext2_ext2" * ]
+             [ "ext2" "ext2_tc" + "ext2_ext2" * ]
              [ "bind" "bind_weight" * ]
           }
         ]