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=784332f15c893c4aa287420488c83d13a2ea53b1;hb=f38fd769279794d0ca73c8945eac30e8b42e59be;hp=fdfa71e69c69d4bfee82c6b8b9072418756fd6c7;hpb=c0d38a82464481e3c8fd68e4b00d7b9b448df462;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 fdfa71e69..784332f15 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
@@ -12,7 +12,7 @@ table {
    class "wine"
    [ { "iterated dynamic typing" * } {
         [ { "context-sensitive iterated native type assignment" * } {
-             [ [ "for terms" ] "ntas" + "( ⦃?,?⦄ ⊢ ? :[?,?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?,?] ? )" * ] 
+             [ [ "for terms" ] "ntas" + "( ⦃?,?⦄ ⊢ ? :*[?,?,?] ? )" "ntas_cpcs" + "ntas_nta" + "ntas_nta_ind" + " ntas_ntas" + "ntas_preserve" * ]
           }
         ]
      }
@@ -20,12 +20,12 @@ table {
    class "magenta"
    [ { "dynamic typing" * } {
         [ { "context-sensitive native type assignment" * } {
-             [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_aaa" + "nta_fsb" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_preserve_cpcs" + "nta_ind" + "nta_eval" * ]
+             [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" "nta_drops" + "nta_aaa" + "nta_fsb" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_preserve_cpcs" + "nta_ind" + "nta_eval" * ]
           }
         ]
         [ { "context-sensitive native validity" * } {
              [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
-             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_acle" + "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpmuwe" + "cnv_cpmuwe_cpme" + "cnv_eval" + "cnv_cpce" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ]
           }
         ]
      }
@@ -92,6 +92,10 @@ table {
    ]
    class "cyan"
    [ { "rt-transition" * } {
+        [ { "context-sensitive parallel t-transition" * } {
+             [ [ "for terms" ] "cpt" + "( ⦃?,?⦄ ⊢ ? ⬆[?,?] ? )" "cpt_drops" + "cpt_fqu" + "cpt_cpm" * ]
+          }
+        ]
         [ { "context-sensitive parallel r-transition" * } {
              [ [ "normal form for terms" ] "cnr ( ⦃?,?⦄ ⊢ ➡[?] 𝐍⦃?⦄ )" "cnr_simple" + "cnr_tdeq" + "cnr_drops" * ]
              [ [ "for lenvs on all entries" ] "lpr" + "( ⦃?,?⦄ ⊢ ➡[?] ? )" "lpr_length" + "lpr_drops" + "lpr_fquq" + "lpr_aaa" + "lpr_lpx" + "lpr_lpr" * ]
@@ -192,7 +196,7 @@ class "italic"            { 2 }
           }
         ]
         [ { "global env. slicing" * } {
-             [ [ "" ] "gget ( ⬇[?] ? ≘ ? )" "gget_gget" * ]
+             [ [ "" ] "gget ( ⇩[?] ? ≘ ? )" "gget_gget" * ]
           }
         ]
         [ { "context-sensitive ordinary rt-substitution" * } {