]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/web/home/basic_2_src.tbl
update in basic_2
[helm.git] / helm / www / lambdadelta / web / home / basic_2_src.tbl
index bfadcd379836cde8d529707cefc99d0cf3eb849b..fff49d93a78b08fef841f1cd21f2b116f41faddc 100644 (file)
@@ -40,7 +40,7 @@ table {
         ]
 *)
         [ { "stratified native validity" * } {
-             [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_ltpss_dx" + "snv_ltpss_sn" + "snv_aaa" + "snv_ssta" + "snv_fpr_ssta" + "snv_fpr" + "snv_fprs" * ]
+             [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_ltpss_dx" + "snv_ltpss_sn" + "snv_aaa" + "snv_ssta" + "snv_cpr_ssta" + "snv_cpr" + "snv_dxprs" * ]
           }
         ]
      }
@@ -77,13 +77,10 @@ table {
    ]
    class "cyan"
    [ { "computation" * } {
-(*        
-       [ { "hyper computation" * } {
-             [ "ysteps ( ? ⊢ ⦃?,?⦄ •⭃*[g] ⦃?,?⦄ )" "ysteps_csups" * ]
-             [ "yprs ( ? ⊢ ⦃?,?⦄ •⥸*[g] ⦃?,?⦄ )" "yprs_csups" + "yprs_xprs" + "yprs_yprs" * ]
+        [ { "big tree order" * } {
+             [ "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
           }
         ]
-*)
         [ { "decomposed extended computation" * } {
              [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxpr_lsubss" + "dxprs_dxprs" * ]
           }
@@ -122,7 +119,11 @@ table {
      }
    ]
    class "water"
-   [ { "reducibility" * } {
+   [ { "reducibility" * } {        
+        [ { "big tree successor" * } {
+             [ "ysucc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
+          }
+        ]
         [ { "context-sensitive focalized reduction" * } {
              [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
           }