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 ca692ea2f2b5fbb643e9501330816989fcce70d2..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" * ]
         }
       ]
@@ -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" * ]
         }
       ]