]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
- lambdadelta: last recursive part of preservation finally proved!
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
index 8a80df07e0f7df1eaa3c51bd6bb51b0459f0dfd7..c4c962070dcc0d24c54ac2b57f2797705ac94abb 100644 (file)
@@ -64,8 +64,8 @@ table {
              [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ]
           }
         ]
-        [ { "local env. ref. for context-sensitive equivalence" * } {
-             [ "lsubse ( ? ⊢•⊑[?] ? )" "lsubse_ldrop" + "lsubse_ssta" + "lsubse_cpcs" * ]
+        [ { "local env. ref. for stratified static type assignment" * } {
+             [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_cpcs" * ]
           }
         ]
         [ { "context-sensitive equivalence" * } {
@@ -170,12 +170,6 @@ table {
    ]
    class "grass"
    [ { "static typing" * } {
-(*        
-       [ { "local env. ref. for stratified static type assignment" * } {
-             [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ]
-          }
-        ]
-*)
         [ { "stratified static type assignment" * } {
              [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ]
           }