X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fwww%2Flambda_delta%2Fweb%2Fhome%2Fbasic_2_src.tbl;h=30591ab8905badf3574f0c46b25789b9029152ea;hb=c66eccc53d2b3000a905f9172b66cf6f9e2131a6;hp=698c8b1fafafa2469d75e691689f90bf5021c206;hpb=386e673720c99be50c1463e430763d630f9ca5d1;p=helm.git

diff --git a/helm/www/lambda_delta/web/home/basic_2_src.tbl b/helm/www/lambda_delta/web/home/basic_2_src.tbl
index 698c8b1fa..30591ab89 100644
--- a/helm/www/lambda_delta/web/home/basic_2_src.tbl
+++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl
@@ -117,12 +117,17 @@ table {
              [ "crf ( ? ⊢ 𝐑⦃?⦄ )" "crf_append" "cif ( ? ⊢ 𝐈⦃?⦄ )" "cif_append" * ]
           }
         ]
+        [ { "focalized reduction" * } {
+             [ "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" * ]
+             [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" * ]
+          }
+        ]
         [ { "context-free normal forms" * } {
              [ "thnf ( 𝐇𝐍⦃?⦄ )"   * ]
           }
         ]
         [ { "context-free reduction" * } {
-             [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" "ltpr_ltpss" "ltpr_aaa" "ltpr_ltpr" * ]
+             [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" "ltpr_tps" "ltpr_ltpss_dx" "ltpr_ltpss_sn" "ltpr_aaa" "ltpr_ltpr" * ]
              [ "tpr ( ? ➡ ? )"  "tpr_lift" "tpr_tpss" "tpr_delift" "tpr_tpr" * ]
           }
         ]
@@ -149,7 +154,7 @@ table {
           }
         ]
         [ { "stratified static type assignment" * } {
-             [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" "ssta_ltpss" "ssta_aaa" "ssta_ssta" * ]
+             [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" "ssta_ltpss_dx" "ssta_ltpss_sn" "ssta_aaa" "ssta_ssta" * ]
           }
         ]
         [ { "local env. ref. for atomic arity assignment" * } {
@@ -157,7 +162,7 @@ table {
           }
         ]
         [ { "atomic arity assignment" * } {
-             [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" "aaa_lifts" "aaa_ltpss" "aaa_aaa" * ]
+             [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" "aaa_lifts" "aaa_ltpss_dx" "aaa_ltpss_sn" "aaa_aaa" * ]
           }
         ]
         [ { "parameters" * } {
@@ -177,7 +182,8 @@ table {
           }
         ]
         [ { "partial unfold" * } {
-             [ "ltpss ( ? ▶*[?,?] ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_tpss" "ltpss_ltpss" * ] 
+             [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_ldrop" "ltpss_sn_tps" "ltpss_sn_tpss" "ltpss_sn_ltpss_sn" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" * ]
+             [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" "ltpss_dx_tps" "ltpss_dx_tpss" "ltpss_dx_ltpss_dx" * ]
              [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
           }
         ]
@@ -211,7 +217,7 @@ table {
           }
         ]
         [ { "local env. ref. for substitution" * } {
-             [ "lsubs ( ? ≼[?,?] ? )" "lsubs_lsubs" "lsubs_sfr ( ≽[?,?] ? )" * ]
+             [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ]
           }
         ]
         [ { "basic term relocation" * } {
@@ -224,7 +230,7 @@ table {
    class "red"   
    [ { "grammar" * } {
         [ { "same head term form" * } {
-             [ "tshf ( ? ≈ ? )" "tshf_tshf" * ]
+             [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ]
           }
         ]
         [ { "same top term constructor" * } {
@@ -237,7 +243,7 @@ table {
         ]
         [ { "internal syntax" * } {
              [ "genv" * ]
-             [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" * ]
+             [ "lenv" "lenv_weight ( #{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" "lenv_px_bi" * ]
              [ "term" "term_weight ( #{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
              [ "item" * ]
           }