- some commutations between the rt-steps and the s-steps proved

[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 a0f7ae830b2ec60fa701a26ad93fcc406ec92c37..d98e42c5cd95ec75e1b07a5179f91373b7ec9125 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
@@ -139,7 +139,7 @@ table {
         ]
         [ { "context-sensitive rt-reduction" * } {
              [ "lpx_lleq" * ]
-             [ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ]
+             [ "cpx_lreq" + "cpx_llpx_sn" + "cpx_lleq" * ]
           }
         ]
 *)
@@ -151,7 +151,7 @@ table {
         ]
         [ { "uncounted context-sensitive rt-transition" * } {
              [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ]
-             [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
+             [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" * ]
           }
         ]
         [ { "counted context-sensitive rt-transition" * } {
@@ -223,7 +223,7 @@ table {
         ]
         [ { "generic relocation for terms" * } {
              [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ]
-             [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_lifts" * ]
+             [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]
           }
         ]
         [ { "ranged equivalence for local environments" * } {