]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
- notation change for tdeq and related notions
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / web / basic_2_src.tbl
index 5719d23daf97fd6f6191e0963396de0a69b9f328..77fe48710c6403c5bd6659963a1b001461f40dae 100644 (file)
@@ -92,7 +92,7 @@ table {
           }
         ]
         [ { "parallel qrst-computation" * } {
-             [ "fpbg ( â¦\83?,?,?â¦\84 >â\89¡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
+             [ "fpbg ( â¦\83?,?,?â¦\84 >â\89\9b[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ]
              [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ]
           }
         ]
@@ -166,8 +166,8 @@ table {
           }
         ]
         [ { "degree-based equivalence on referred entries" * } {
-             [ "ffdeq ( â¦\83?,?,?â¦\84 â\89¡[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
-             [ "lfdeq ( ? â\89¡[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
+             [ "ffdeq ( â¦\83?,?,?â¦\84 â\89\9b[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ]
+             [ "lfdeq ( ? â\89\9b[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ]
           }
         ]
         [ { "generic extension on referred entries" * } {
@@ -237,8 +237,8 @@ table {
           }
         ]
         [ { "degree-based equivalence" * } {
-             [ "tdeq_ext ( ? â\89¡[?,?] ? ) ( ? â\8a¢ ? â\89¡[?,?] ? )" * ]
-             [ "tdeq ( ? â\89¡[?,?] ? )" "tdeq_tdeq" * ]
+             [ "tdeq_ext ( ? â\89\9b[?,?] ? ) ( ? â\8a¢ ? â\89\9b[?,?] ? )" * ]
+             [ "tdeq ( ? â\89\9b[?,?] ? )" "tdeq_tdeq" * ]
           }
         ]
         [ { "closures" * } {