- substitution lemma for native type assignmenr proved!

[helm.git] / helm / www / lambda_delta / web / home / basic_2_src.tbl

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 a8c6d34b95feafb0afbfeb58544232c8f1321086..254dfcc969e420989ef6a41ddf2072ffc51edb6e 100644 (file)
--- a/helm/www/lambda_delta/web/home/basic_2_src.tbl
+++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl
@@ -126,8 +126,8 @@ table {
           }
        ]
        [ { "partial unfold" * } {
-             [ "ltpss ( ? [?,?] ▶* ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_tpss" "ltpss_ltpss" * ] 
-            [ "tpss ( ? ⊢ ? [?,?] ▶* ? )" "tpss_alt ( ? ⊢ ? [?,?] ▶▶* ? )" "tpss_lift" "tpss_tpss" * ]
+             [ "ltpss ( ? ▶*[?,?] ? )" "ltpss_ldrop" "ltpss_tps" "ltpss_tpss" "ltpss_ltpss" * ] 
+            [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ]
           }
        ]
        [ { "generic local env. slicing" * } { 
@@ -148,7 +148,7 @@ table {
    class "orange"   
    [ { "substitution" * } { 
         [ { "parallel substitution" * } {
-            [ "tps ( ? ⊢ ? [?,?] ▶ ? )" "tps_lift" "tps_tps" * ]
+            [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" "tps_tps" * ]
           }
        ]
        [ { "global env. slicing" * } {
@@ -156,7 +156,11 @@ table {
           }
        ]
        [ { "basic local env. slicing" * } {
-             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" * ]
+             [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_ldrop" "ldrop_sfr" * ]
+          }
+       ]
+        [ { "local env. ref. for substitution" * } {
+             [ "lsubs ( ? ≼[?,?] ? )" "lsubs_lsubs" "lsubs_sfr ( ≼[?,?] ? )" * ]
           }
        ]
         [ { "basic term relocation" * } {
@@ -168,10 +172,6 @@ table {
    ]
    class "red"   
    [ { "grammar" * } {
-        [ { "local env. ref. for substitution" * } {
-             [ "lsubs ( ? [?,?] ≼ ? )" "lsubs_lsubs" * ]
-          }
-       ]
        [ { "same head term form" * } {
              [ "tshf ( ? ≈ ? )" "tshf_tshf" * ]
           }