bugfix 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 40e94b86ffa7b7422823debc7494b6f94e798891..4da8d232f58b54bd8b344b3419311dd606680866 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
@@ -107,7 +107,7 @@ table {
         ]
 *)
         [ { "uncounted context-sensitive parallel rt-computation" * } {
-             [ [ "refinement for lenvs" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ]
+             [ [ "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" * ]
              [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
@@ -122,8 +122,8 @@ table {
    class "cyan"
    [ { "rt-transition" * } {
         [ { "uncounted parallel rst-transition" * } {
-             [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
-             [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
+             [ [ "for closures" ] "fpbq" + "( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpbq_aaa" * ]
+             [ [ "proper for closures" ] "fpb" + "( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ]
           }
         ]
         [ { "context-sensitive parallel r-transition" * } {
@@ -168,7 +168,7 @@ table {
         ]
         [ { "atomic arity assignment" * } {
              [ [ "restricted refinement for lenvs" ] "lsuba" + "( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ]
-             [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]
+             [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_ffdeq" + "aaa_aaa" * ]
           }
         ]
         [ { "degree-based equivalence" * } {
@@ -177,7 +177,7 @@ table {
           }
         ]
         [ { "syntactic equivalence" * } {
-             [ [ "for lenvs on referred entries" ] "lfeq" + "( ? â\89¡[?] ? )" "lfeq_fqup" + "lfeq_fsle" * ]
+             [ [ "for lenvs on referred entries" ] "lfeq" + "( ? â\89\90[?] ? )" "lfeq_fqup" + "lfeq_fsle" * ]
           }
         ]
         [ { "generic extension of a context-sensitive relation" * } {
@@ -227,7 +227,7 @@ table {
           }
         ]
         [ { "syntactic equivalence" * } {
-             [ [ "for lenvs on selected entries" ] "lreq" + "( ? â\89¡[?] ? )" "lreq_length" + "lreq_lreq" * ]
+             [ [ "for lenvs on selected entries" ] "lreq" + "( ? â\89\90[?] ? )" "lreq_length" + "lreq_lreq" * ]
           }
         ]
         [ { "generic entrywise extension" * } {