X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2_src.tbl;h=dd6ed3880e5e92d284ae8bc752559f41bb7da237;hb=c44a7c4d35c1bb9651c3596519d8262e52e90ff4;hp=bfc628f284a4b57b20af9c272e2fa22f28f331e3;hpb=d7c5846e4a362a366f5600d079e08f8a75b9d566;p=helm.git

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 bfc628f28..dd6ed3880 100644
--- 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,9 +111,9 @@ table {
              [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "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_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ]
-             [ [ "for lenvs on referred entries" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ]
+             [ [ "for lenvs on referred entries" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
              [ [ "for lenvs on all entries" ] "lpxs ( ⦃?,?⦄ ⊢ ⬈*[?] ? )" * ]
-             [ [ "for terms" ] "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] 
+             [ [ "for terms" ] "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] 
           }
         ]
      }
@@ -140,7 +140,7 @@ table {
              [ [ "for lenvs on referred entries" ] "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ]
              [ [ "for lenvs on all entries" ] "lpx ( ⦃?,?⦄ ⊢ ⬈[?] ? )" * ]
              [ [ "for binders" ] "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ]
-             [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ]
+             [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" + "cpx_lfeq" * ]
           }
         ]
         [ { "counted context-sensitive parallel rt-transition" * } {
@@ -214,24 +214,23 @@ table {
    ]
    class "orange"
    [ { "relocation" * } {
-        [ { "generic slicing for local environments" * } {
-             [ [ "" ] "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ]
-             [ [ "" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ]
+        [ { "generic slicing" * } {
+             [ [ "for lenvs" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ]
           }
         ]
         [ { "generic relocation" * } {
-             [ [ "" ] "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
-             [ [ "" ] "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ]
-             [ [ "" ] "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]
+             [ [ "for binders" ] "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ]
+             [ [ "for term vectors" ] "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ]
+             [ [ "for terms" ] "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ]
           }
         ]
-        [ { "ranged equivalence for local environments" * } {
-             [ [ "" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ]
+        [ { "syntactic equivalence" * } {
+             [ [ "for lenvs on selected entries" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ]
           }
         ]
         [ { "generic entrywise extension" * } {
-             [ [ "" ] "lex ( ? ⦻[?] ? )" * ]
-             [ [ "" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
+             [ [ "for lenvs of one contex-sensitive relation" ] "lex ( ? ⦻[?] ? )" "lex_tc" * ]
+             [ [ "for lenvs of two contex-sensitive relations" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ]
           }
         ]
      }