lfpx_drops 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 a5aeb85db0691b032c2b7bb18a86132720ae0a44..2aa5021d164dc9832dd0e911284aa60db95426f2 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
@@ -138,8 +138,8 @@ table {
           }
         ]
         [ { "context-sensitive rt-reduction" * } {
-             [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ]
-             [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lreq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
+             [ "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ]
+             [ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ]
           }
         ]
         [ { "context-sensitive reduction" * } {
@@ -149,11 +149,12 @@ table {
         ]
 *)
         [ { "uncounted context-sensitive rt-transition" * } {
-             [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
+             [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" * ]
+             [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ]
           }
         ]
         [ { "counted context-sensitive rt-transition" * } {
-             [ "cpg ( â¦\83?,?â¦\84 â\8a¢ ? â\9e¡[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
+             [ "cpg ( â¦\83?,?â¦\84 â\8a¢ ? â¬\88[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ]
           }
         ]
      }
@@ -185,11 +186,11 @@ table {
           }
         ]
         [ { "generic extension on referred entries" * } {
-             [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_fqup" + "lfxs_lfxs" * ]
+             [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ]
           }
         ]
         [ { "context-sensitive free variables" * } {
-             [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_frees" * ]
+             [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_drops" + "frees_frees" * ]
           }
         ]
      }
@@ -215,8 +216,8 @@ table {
    class "orange"
    [ { "relocation" * } {
         [ { "generic slicing for local environments" * } {
-             [ "drops_vector ( ⬇*[?,?] ? ≡ ? )" * ]
-             [ "drops ( ⬇*[?,?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_ceq" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
+             [ "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ]
+             [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_ceq" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
           }
         ]
         [ { "generic relocation for terms" * } {