cpx_tsts completed

[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 20b1e11d6c66ba4373f7caaa016cd253dc8ad14b..305dbb057f44e943ac19d7c9b8d5295692b8f5d9 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
@@ -111,12 +111,12 @@ table {
         [ { "uncounted context-sensitive rt-transition" * } {
 (*
              [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
-             [ "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_lreq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
+             [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ]
 *)
              [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )"  * ]
              [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx" + "csx_cpxs" + "csx_csx" * ]
              [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ]
-             [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_drops" + "cpxs_lfpx" + "cpxs_cpxs" * ] 
+             [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] 
           }
         ]
      }
@@ -142,7 +142,7 @@ table {
           }
         ]
         [ { "uncounted context-sensitive rt-transition" * } {
-             [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" * ]
+             [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" *+ "cnx_cnx"  ]
              [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ]
              [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
           }
@@ -240,12 +240,12 @@ table {
              [ "append ( ? @@ ? )" "append_length" * ]
           }
         ]
-        [ { "degree-based equivalence for terms" * } {
-             [ "deq ( ? ≡[?,?] ? ) " "deq_deq" * ]
+        [ { "same top term structure" * } {
+             [ "tsts ( ? ⩳[?,?] ? )" "tsts_simple" + "tsts_tdeq" + "tsts_tsts" + "tsts_vector" * ]
           }
         ]
-        [ { "same top term structure" * } {
-             [ "tsts ( ? ≂ ? )" "tsts_tsts" + "tsts_vector" * ]
+        [ { "degree-based equivalence for terms" * } {
+             [ "deq ( ? ≡[?,?] ? ) " "deq_deq" * ]
           }
         ]
         [ { "closures" * } {