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=147978606d6d532f2697da12adde26f797430d8d;hb=99573d95dbebe2ec3dac5eda7b1dde2fe819ce3f;hp=456a2b0e329badd42b2919a520d47746d52bb70d;hpb=127be10fa95b5b347887241e046d72e432944e61;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 456a2b0e3..147978606 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
@@ -11,7 +11,7 @@ table {
    ]
    class "wine"
    [ { "examples" * } {
-        [ { "" * } {
+        [ { "terms with special features" * } {
              [ "ex_cpr_omega" * ]
           }
         ]
@@ -47,11 +47,12 @@ table {
         ]
 *)
         [ { "local env. ref. for stratified native validity" * } {
-             [ "lsubsv ( ? ⊢ ? ¡⫃[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
+             [ "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
           }
         ]
         [ { "stratified native validity" * } {
-             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_cpcs" + "snv_preserve" * ]
+             [ "hsnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" "hsnv_aaa" * ]
+             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_cpes" + "snv_preserve" * ]
           }
         ]
      }
@@ -59,7 +60,7 @@ table {
    class "blue"
    [ { "equivalence" * } {
         [ { "decomposed extended equivalence" * } {
-             [ "cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )" "cpes_cpds" * ]
+             [ "cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "cpes_aaa" + "cpes_cpcs" + "cpes_cpes" * ]
           }
         ]
         [ { "context-sensitive equivalence" * } {
@@ -105,7 +106,7 @@ table {
           }
         ]
         [ { "decomposed extended computation" * } {
-             [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ]
+             [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ]
           }
         ]
         [ { "context-sensitive extended computation" * } {
@@ -185,7 +186,7 @@ table {
    class "grass"
    [ { "static typing" * } {
         [ { "local env. ref. for degree assignment" * } {
-             [ "lsubd ( ? ⊢ ? ▪⫃ ? )" "lsubd_da" + "lsubd_lsubd" * ]
+             [ "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ]
           }
         ]
         [ { "degree assignment" * } {
@@ -201,7 +202,7 @@ table {
           }
         ]
         [ { "local env. ref. for atomic arity assignment" * } {
-             [ "lsuba ( ? ⊢ ? ⁝⫃ ? )" "lsuba_aaa" + "lsuba_lsuba" * ]
+             [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_aaa" + "lsuba_lsuba" * ]
           }
         ]
         [ { "atomic arity assignment" * } {
@@ -273,7 +274,7 @@ table {
           }
         ]
         [ { "local env. ref. for extended substitution" * } {
-             [ "lsuby ( ? ⊑×[?,?] ? )" "lsuby_lsuby" * ]
+             [ "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ]
           }
         ]
         [ { "pointwise extension of a relation" * } {