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=e7a665c668736d3f005cdc40d2063b162ddd1b1d;hb=12023ae1e3d075130b31d2d8559c85847ef06dee;hp=3b79088f2bb7be47c9c0a3bb5f9a43a61a48ea2a;hpb=fdb2c62b58006b82c015ba70b494d50c7860e28f;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 3b79088f2..e7a665c66 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
@@ -39,15 +39,6 @@ table {
           }
         ]
 *)
-        [ { "\"big tree\" parallel computation" * } {
-             [ "ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "ygt_lift" + "ygt_ygt" * ]
-             [ "yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "yprs_lift" + "yprs_yprs" * ]
-          }
-        ]
-        [ { "\"big tree\" parallel reduction" * } {
-             [ "ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ]
-          }
-        ]
         [ { "local env. ref. for stratified native validity" * } {
              [ "lsubsv ( ? ⊢ ? ¡⊑[?,?] ? )" "lsubsv_ldrop" + "lsubsv_lsubd" + "lsubsv_lsuba" + "lsubsv_lsstas" + "lsubsv_cpds" + "lsubsv_cpcs" + "lsubsv_snv" * ]
           }
@@ -89,8 +80,13 @@ table {
           }
         ]
         [ { "strongly normalizing computation" * } {
-             [ "csn_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csn_tstc_vector" + "csn_aaa" * ]
-             [ "csn ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csn_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csn_lift" + "csn_lpx" * ]
+             [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
+             [ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lpx" * ]
+          }
+        ]
+        [ { "\"big tree\" parallel computation" * } {
+             [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ]
+             [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ]
           }
         ]
         [ { "decomposed extended computation" * } {
@@ -119,6 +115,11 @@ table {
    ]
    class "water"
    [ { "reduction" * } {
+        [ { "\"big tree\" parallel reduction" * } {
+             [ "fpbc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbc_lift" * ]
+             [ "fpb ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "fpb_lift" * ]
+          }
+        ]
         [ { "context-sensitive extended normal forms" * } {
              [ "cnx ( ⦃?,?⦄ ⊢ 𝐍[?,?]⦃?⦄ )" "cnx_lift" + "cnx_crx" + "cnx_cix" * ]
           }
@@ -202,8 +203,8 @@ table {
           }
         ]
         [ { "iterated structural successor for closures" * } {
-             [ "fsups ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fsups_fsups" * ]
-             [ "fsupp ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fsupp_fsupp" * ]
+             [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_fqus" * ]
+             [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
           }
         ]
         [ { "generic local env. slicing" * } {
@@ -224,7 +225,7 @@ table {
    class "orange"
    [ { "relocation" * } {
         [ { "structural successor for closures" * } {
-             [ "fsup ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fsupq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fsupq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ]
+             [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ]
           }
         ]
         [ { "global env. slicing" * } {
@@ -253,6 +254,7 @@ table {
           }
         ]
         [ { "closures" * } {
+             [ "bteq ( ⦃?,?,?⦄ ⪴ ⦃?,?,?⦄ )" "bteq_bteq" * ]
              [ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?,?} )" * ]
           }
         ]