some resuls on pointwise extensions (all of them are now in the

[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 a5f14f1960a533e701a0457ac134e46c5040d183..f65ec6eee8d79675e0337967c4585c4551baf2a0 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
@@ -213,7 +213,7 @@ table {
    [ { "substitution" * } {
         [ { "lazy equivalence" * } {
              [ "fleq ( ⦃?,?,?⦄ ⋕[?] ⦃?,?,?⦄ )" "fleq_fleq" * ]
-             [ "lleq ( ? ⋕[?,?] ? )" "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ]
+             [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt" + "lleq_leq" + "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ]
           }
         ]
         [ { "iterated structural successor for closures" * } {
@@ -248,7 +248,7 @@ table {
           }
         ]
         [ { "lazy pointwise extension of a relation" * } {
-             [ "llpx_sn" "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ]
+             [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_tc" + "llpx_sn_leq" + "llpx_sn_ldrop" + "llpx_sn_lpx_sn" * ]
           }
         ]
         [ { "basic local env. slicing" * } {
@@ -257,7 +257,7 @@ table {
         ]
         [ { "basic term relocation" * } {
              [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
-             [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]
+             [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_neq" + "lift_lift" * ]
           }
         ]
      }
@@ -269,7 +269,7 @@ table {
           }
         ]
         [ { "pointwise extension of a relation" * } {
-             [ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ]
+             [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_tc" + "lpx_sn_lpx_sn" * ]
           }
         ]
         [ { "same top term constructor" * } {