- bugfixed "aacr" allows to remove historical eta-conversions

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl

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 456a2b0e329badd42b2919a520d47746d52bb70d..81cd8e41dbc7c1dcb61037f41c25f7c51bedefaf 100644 (file)
--- 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_scpds" + "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" * ]
+             [ "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" "shnv_aaa" * ]
+             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_scpes" + "snv_preserve" * ]
           }
         ]
      }
@@ -59,7 +60,7 @@ table {
    class "blue"
    [ { "equivalence" * } {
         [ { "decomposed extended equivalence" * } {
-             [ "cpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?] ? )" "cpes_cpds" * ]
+             [ "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
           }
         ]
         [ { "context-sensitive equivalence" * } {
@@ -100,12 +101,12 @@ table {
         [ { "\"big tree\" parallel computation" * } {
              [ "fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ]
              [ "fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ]
-             [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" "fpbu_fleq" * ]
+             [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" + "fpbu_fleq" * ]
              [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_fpbs" + "fpbs_ext" * ]
           }
         ]
         [ { "decomposed extended computation" * } {
-             [ "cpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?] ? )" "cpds_lift" + "cpds_aaa" + "cpds_cpds" * ]
+             [ "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ]
           }
         ]
         [ { "context-sensitive extended computation" * } {
@@ -139,7 +140,7 @@ table {
           }
         ]
         [ { "context-sensitive extended reduction" * } {
-             [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" "lpx_lleq" + "lpx_aaa" * ]
+             [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ]
              [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ]
           }
         ]
@@ -185,7 +186,7 @@ table {
    class "grass"
    [ { "static typing" * } {
         [ { "local env. ref. for degree assignment" * } {
-             [ "lsubd ( ? â\8a¢ ? â\96ªâ«\83 ? )" "lsubd_da" + "lsubd_lsubd" * ]
+             [ "lsubd ( ? â\8a¢ ? â«\83â\96ª[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ]
           }
         ]
         [ { "degree assignment" * } {
@@ -201,7 +202,7 @@ table {
           }
         ]
         [ { "local env. ref. for atomic arity assignment" * } {
-             [ "lsuba ( ? â\8a¢ ? â\81\9dâ«\83 ? )" "lsuba_aaa" + "lsuba_lsuba" * ]
+             [ "lsuba ( ? â\8a¢ ? â«\83â\81\9d ? )" "lsuba_aaa" + "lsuba_lsuba" * ]
           }
         ]
         [ { "atomic arity assignment" * } {
@@ -273,7 +274,7 @@ table {
           }
         ]
         [ { "local env. ref. for extended substitution" * } {
-             [ "lsuby ( ? â\8a\91Ã\97[?,?] ? )" "lsuby_lsuby" * ]
+             [ "lsuby ( ? â\8a\86[?,?] ? )" "lsuby_lsuby" * ]
           }
         ]
         [ { "pointwise extension of a relation" * } {
@@ -308,7 +309,7 @@ table {
         [ { "internal syntax" * } {
              [ "genv" * ]
              [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" * ]
-             [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ]
+             [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector ( Ⓐ?.? )" * ]
              [ "item" * ]
           }
         ]
@@ -320,8 +321,8 @@ table {
    ]
 }
 
-class "component" { 0 }
+class "top"               { * }
 
-class "plane" { 1 }
+class "capitalize italic" { 0 }
 
-class "file" { 2 * }
+class "italic"            { 1 }