propagating the arithmetics library, partial commit

[helm.git] / matita / matita / contribs / lambdadelta / ground / web / ground_src.tbl

diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index e79511f7cf2eda76b9f7847f87e0042157150f04..54733490fd2067df6116a3bbf51f7b5eb6c08d12 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -13,7 +13,7 @@ table {
   [ { "generic rt-transition counter" * } {
       [ { "" * } {
           [ "rtc_ist ( 𝐓❪?,?❫ )" "rtc_ist_shift" "rtc_ist_plus" "rtc_ist_max" * ]
-          [ "rtc_isrc ( 𝐑𝐓❪?,?❫ )" "rtc_isrt_shift" "rtc_isrt_plus" "rtc_isrt_max" "rtc_isrt_max_shift" * ]
+          [ "rtc_ism ( 𝐌❪?,?❫ )" "rtc_ism_shift" "rtc_ism_plus" "rtc_ism_max" "rtc_ism_max_shift" * ]
           [ "rtc ( 〈?,?,?,?〉 ) ( 𝟘𝟘 ) ( 𝟙𝟘 ) ( 𝟘𝟙 )" "rtc_shift ( ↕*? )" "rtc_plus ( ? + ? )" "rtc_max ( ? ∨ ? )" "rtc_max_shift" * ]
         }
       ]
@@ -57,9 +57,9 @@ table {
         }
       ]
       [ { "non-negative integers with infinity" * } {
-          [ "ynat_lt ( ?<? )" "ynat_lt_succ" "ynat_lt_pred" "ynat_lt_pred_succ" "ynat_lt_plus" "ynat_lt_plus_pred" "ynat_lt_minus1" "ynat_lt_minus1_plus" "ynat_lt_le" "ynat_lt_le_succ" "ynat_lt_le_pred" "ynat_lt_le_pred_succ" "ynat_lt_le_plus" "ynat_lt_le_minus1" "ynat_lt_le_minus1_plus" * ]
-          [ "ynat_le ( ?≤? )" "ynat_le_succ" "ynat_le_pred" "ynat_le_pred_succ" "ynat_le_plus" "ynat_le_minus1" "ynat_le_minus1_succ" "ynat_le_minus1_plus" * ]
-          [ "ynat_minus1 ( ?-? )" "ynat_minus1_succ" "ynat_minus1_plus" * ]
+          [ "ynat_lt ( ?<? )" "ynat_lt_succ" "ynat_lt_pred" "ynat_lt_pred_succ" "ynat_lt_plus" "ynat_lt_plus_pred" "ynat_lt_lminus" "ynat_lt_lminus_plus" "ynat_lt_le" "ynat_lt_le_succ" "ynat_lt_le_pred" "ynat_lt_le_pred_succ" "ynat_lt_le_plus" "ynat_lt_le_lminus" "ynat_lt_le_lminus_plus" * ]
+          [ "ynat_le ( ?≤? )" "ynat_le_succ" "ynat_le_pred" "ynat_le_pred_succ" "ynat_le_plus" "ynat_le_lminus" "ynat_le_lminus_succ" "ynat_le_lminus_plus" * ]
+          [ "ynat_lminus ( ?-? )" "ynat_lminus_succ" "ynat_lminus_plus" * ]
           [ "ynat_plus ( ?+? )" * ]
           [ "ynat_pred ( ↓? )" "ynat_pred_succ" * ]
           [ "ynat_succ ( ↑? )" * ]
@@ -71,14 +71,18 @@ table {
           [ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" "nat_le_max" * ]
           [ "nat_max ( ?∨? )" * ]
           [ "nat_minus ( ?-? )" "nat_minus_plus" * ]
-          [ "nat_plus ( ?+? )" "nat_plus_pred" * ]
+          [ "nat_plus ( ?+? )" "nat_plus_pred" "nat_plus_rplus" * ]
+          [ "nat_rplus ( ?+? )" "nat_rplus_succ" * ]
           [ "nat_pred ( ↓? )" "nat_pred_succ" * ]
           [ "nat_succ ( ↑? )" "nat_succ_iter" "nat_succ_tri" * ]
           [ "nat ( 𝟎 )" "nat_iter ( ?^{?}? )" *"nat_tri"  ]
         }
       ]
       [ { "positive integers" * } {
+          [ "nat_lt ( ?<? )" "pnat_lt_pred" * ]
+          [ "pnat_le ( ?≤? )" "pnat_le_pred" "pnat_le_plus" * ]
           [ "pnat_plus ( ?+? )" * ]
+          [ "nat_pred ( ↓? )" * ]
           [ "pnat ( 𝟏 ) ( ↑? )" "pnat_dis" "pnat_iter ( ?^{?}? )" "pnat_tri" * ]
         }
       ]
@@ -88,8 +92,8 @@ table {
   [ { "extensions to the library" * } {
       [ { "" * } {
           [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
-          [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ]
-          [ "bool ( Ⓕ ) ( Ⓣ )" * ]
+          [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" "list_length ( |?| )" * ]
+          [ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ]
           [ "ltc" "ltc_ctc" * ]
           [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ]
         }