]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/www/lambdadelta/web/home/basic_2_src.tbl
- xhtbl: now double quotes can appear in string literals
[helm.git] / helm / www / lambdadelta / web / home / basic_2_src.tbl
index fff49d93a78b08fef841f1cd21f2b116f41faddc..12f91aff4518b7e6ca3317e25b1054b463dcf17b 100644 (file)
@@ -77,7 +77,12 @@ table {
    ]
    class "cyan"
    [ { "computation" * } {
-        [ { "big tree order" * } {
+        [ { "focalized computation" * } {
+             [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ]
+             [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
+          }
+        ]
+        [ { "\"big tree\" order" * } {
              [ "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
           }
         ]
@@ -94,11 +99,6 @@ table {
              [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_cpr" + "csn_lfpr" * ]
           }
         ]
-        [ { "focalized computation" * } {
-             [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ]
-             [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ]
-          }
-        ]
         [ { "context-sensitive computation" * } {
              [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_tpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_delift" + "cprs_aaa" + "cprs_ltpr" + "cprs_lfpr" + "cprs_cprs" + "cprs_lfprs" + "cprs_tstc" + "cprs_tstc_vector" * ]
           }
@@ -120,10 +120,6 @@ table {
    ]
    class "water"
    [ { "reducibility" * } {        
-        [ { "big tree successor" * } {
-             [ "ysucc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
-          }
-        ]
         [ { "context-sensitive focalized reduction" * } {
              [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ]
           }
@@ -133,6 +129,10 @@ table {
              [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ]
           }
         ]
+        [ { "\"big tree\" successor" * } {
+             [ "ysucc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
+          }
+        ]
         [ { "context-sensitive normal forms" * } {
              [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ]
           }