nug fix in the location of images

[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 13506e6ea056228251684db66daf50b5fad43ce8..28aacba879eaaf7f0bb01c00db59d38f612ede4b 100644 (file)
--- a/helm/www/lambda_delta/web/home/basic_2_src.tbl
+++ b/helm/www/lambda_delta/web/home/basic_2_src.tbl
@@ -40,7 +40,7 @@ table {
         ]
 *)
         [ { "stratified native validity" * } {
-             [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_aaa" * ]
+             [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_aaa" + "snv_ssta" * ]
           }
         ]
      }
@@ -49,6 +49,11 @@ table {
    [ { "equivalence" * } {
         [ { "focalized equivalence" * } {
              [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ]
+             [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ]
+          }
+        ]
+        [ { "local env. ref. for context-sensitive equivalence" * } {
+             [ "lsubse ( ? ⊢•⊑[?] ? )" "lsubse_ldrop" + "lsubse_ssta" + "lsubse_cpcs" * ]
           }
         ]
         [ { "context-sensitive equivalence" * } {
@@ -60,7 +65,8 @@ table {
    class "sky"
    [ { "conversion" * } {
         [ { "focalized conversion" * } {
-             [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]        
+             [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ]
+             [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ]
           }
         ]
         [ { "context-sensitive conversion" * } {
@@ -71,8 +77,15 @@ table {
    ]
    class "cyan"
    [ { "computation" * } {
+(*        
+       [ { "hyper computation" * } {
+             [ "ysteps ( ? ⊢ ⦃?,?⦄ •⭃*[g] ⦃?,?⦄ )" "ysteps_csups" * ]
+             [ "yprs ( ? ⊢ ⦃?,?⦄ •⥸*[g] ⦃?,?⦄ )" "yprs_csups" + "yprs_xprs" + "yprs_yprs" * ]
+          }
+        ]
+*)
         [ { "extended computation" * } {
-             [ "xprs ( â¦\83?,?â¦\84 â\8a¢ ? â\9e¸*[?] ? )" "xprs_lift" + "xprs_aaa" + "xprs_cprs" * ]
+             [ "xprs ( â¦\83?,?â¦\84 â\8a¢ ? â\80¢â\9e¡*[?] ? )" "xprs_lift" + "xprs_aaa" + "xpr_lsubss" + "xprs_cprs" + "xprs_xprs" * ]
           }
         ]
         [ { "weakly normalizing computation" * } {
@@ -86,6 +99,7 @@ table {
         ]
         [ { "focalized computation" * } {
              [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_cprs" + "lfprs_lfprs" * ]
+             [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
           }
         ]
         [ { "context-sensitive computation" * } {
@@ -109,12 +123,18 @@ table {
    ]
    class "water"
    [ { "reducibility" * } {
+(*        
+       [ { "hyper reduction" * } {
+             [ "ypr ( ? ⊢ ⦃?,?⦄ •⥸[g] ⦃?,?⦄ )" * ]
+          }
+        ]
+*)
         [ { "extended reduction" * } {
-             [ "xpr ( â¦\83?,?â¦\84 â\8a¢ ? â\9e¸[?] ? )" "xpr_lift" + "xpr_aaa" * ]
+             [ "xpr ( â¦\83?,?â¦\84 â\8a¢ ? â\80¢â\9e¡[?] ? )" "xpr_lift" + "xpr_aaa" + "xpr_lsubss" * ]
           }
         ]
         [ { "context-sensitive focalized reduction" * } {
-             [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" * ]
+             [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
           }
         ]
         [ { "context-free focalized reduction" * } {
@@ -140,7 +160,7 @@ table {
         ]
         [ { "context-free reduction" * } {
              [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ]
-             [ "tpr ( ? ➡ ? )"  "tpr_lift" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ]
+             [ "tpr ( ? ➡ ? )"  "tpr_lift" + "tpr_tps" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ]
           }
         ]
      }
@@ -162,7 +182,7 @@ table {
    class "grass"
    [ { "static typing" * } {
         [ { "local env. ref. for stratified static type assignment" * } {
-             [ "lsubss ( ? â\81\9dâ\8a\91 ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
+             [ "lsubss ( ? â\80¢â\8a\91[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
           }
         ]
         [ { "stratified static type assignment" * } {
@@ -203,6 +223,11 @@ table {
              [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
           }
         ]
+        [ { "iterated restricted structural predecessor for closures" * } {
+             [ "frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )" "frsups_frsups" * ]
+             [ "frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )" "frsupp_frsupp" * ]
+          }
+        ]
         [ { "generic term relocation" * } {
              [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ]
              [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ] 
@@ -232,6 +257,10 @@ table {
              [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ]
           }
         ]
+        [ { "restricted structural predecessor for closures" * } {
+             [ "frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )" * ]
+          }
+        ]
         [ { "basic term relocation" * } {
              [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ]
              [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ]