- notation change for tdeq and related notions

[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 7310545d7d791219557afa88cd5cb356c41b950d..77fe48710c6403c5bd6659963a1b001461f40dae 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" * ]
-             [ "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ]
+             [ "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,9 +105,10 @@ table {
              [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
           }
         ]
-*)        
+*)
         [ { "uncounted context-sensitive rt-computation" * } {
-             [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ]
+             [ "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" * ]
              [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
@@ -121,7 +121,7 @@ table {
    [ { "rt-transition" * } {
         [ { "uncounted rst-transition" * } {
              [ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
-             [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
+             [ "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
           }
         ]
         [ { "t-bound context-sensitive rt-transition" * } {
@@ -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" * } {
@@ -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" * } {