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=e6fd5b825a3e685d76e81e499d8431db586fd797;hb=bb246930370226dc96c9b9121f59853a0a2f1434;hp=b82479065b67b7c34876fb9253f7da9bc0406aad;hpb=cac0166656e08399eaaf1a1e19f0ccea28c36d39;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 b82479065..e6fd5b825 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
@@ -37,21 +37,15 @@ table {
 (*
              [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ]
 *)
-             [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "nv_drops" (* + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" *) * ]
+             [ [ "for terms" ] "nv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "nv_drops" + "nv_fqus" + "nv_aaa" + "snv_fsb" (* + "snv_lpr" + "snv_scpes" + "snv_preserve" *) * ]
           }
         ]
      }
    ]
    class "prune"
-   [ { "rt-equivalence" * } {
-(*
-        [ { "decomposed rt-equivalence" * } {
-             [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
-          }
-        ]
-*)        
+   [ { "rt-equivalence" * } {        
         [ { "context-sensitive parallel r-equivalence" * } {
-             [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" (* "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" *) * ]
+             [ [ "for terms" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌*[?] ? )" "cpcs_drops" + "cpcs_lsubr" + "cpcs_aaa" + "cpcs_cprs" + "cpcs_lprs" + "cpcs_cpc" + "cpcs_cpcs" * ]
           }
         ]
      }
@@ -66,12 +60,6 @@ table {
    ]
    class "sky"
    [ { "rt-computation" * } {
-(*
-        [ { "decomposed rt-computation" * } {
-             "scpds_scpds"
-          }
-        ]
-*)        
         [ { "context-sensitive parallel r-computation" * } {
              [ [ "for lenvs on all entries" ] "lprs ( ⦃?,?⦄ ⊢ ➡*[?] ? )" "lprs_tc" + "lprs_ctc" + "lprs_length" + "lprs_drops" + "lprs_aaa" + "lprs_lpr" + "lprs_lpxs" + "lprs_cpms" + "lprs_cprs" + "lprs_lprs" * ]
              [ [ "for binders" ] "cprs_ext" + "( ⦃?,?⦄ ⊢ ? ➡*[?] ?)" * ]
@@ -288,6 +276,10 @@ class "capitalize italic" { 0 1 }
 
 class "italic"            { 2 }
 (*
+        [ { "decomposed rt-equivalence" * } {
+             [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ]
+          }
+        ]
         [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ]
         [ [ "for lenvs on referred entries" ]
               "lfpr" + "( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ]