]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
partial commit: "conversion" and "equivalence" components ...
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
index 7a7d92d1786704efd459c935eefbfe45dd6cb3f5..0bd584cac4478ea27481c60e74dbf899e6a387fa 100644 (file)
@@ -40,19 +40,19 @@ table {
         ]
 *)
         [ { "\"big tree\" parallel computation" * } {
-             [ "yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )" "yprs_yprs"  "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ]
+             [ "yprs ( ? ⊢ ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "yprs_yprs"  "ygt ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "ygt_ygt" * ]
           }
         ]
         [ { "\"big tree\" parallel reduction" * } {
-             [ "ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )" "ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ]
+             [ "ypr ( ⦃?,?,?⦄ ≽[?,?] ⦃?,?,?⦄ )" "ysc ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" * ]
           }
         ]
         [ { "local env. ref. for stratified native validity" * } {
-             [ "lsubsv ( ? ⊢ ? ¡⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ]
+             [ "lsubsv ( ? ⊢ ? ¡⊑[?,?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ]
           }
         ]
         [ { "stratified native validity" * } {
-             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?] )" "snv_lift" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_lpr" + "snv_lpr" + "snv_cpcs" * ]
+             [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_lpr" + "snv_lpr" + "snv_cpcs" * ]
           }
         ]
      }
@@ -60,7 +60,7 @@ table {
    class "blue"
    [ { "equivalence" * } {
         [ { "context-sensitive equivalence" * } {
-             [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ]
+             [ "cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ]
           }
         ]
      }
@@ -68,7 +68,7 @@ table {
    class "sky"
    [ { "conversion" * } {
         [ { "context-sensitive conversion" * } {
-             [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ]
+             [ "cpc ( ⦃?,?⦄ ⊢ ? ⬌ ? )" "cpc_cpc" * ]
           }
         ]
      }