From 68e028d053806177e218ee1a5f8778d3011bef83 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 4 Jan 2021 21:33:13 +0100
Subject: [PATCH] =?utf8?q?arithmetics=20for=20=CE=BB=CE=B4?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

+ maximum for non-negative integers
+ minor corrections
---
 .../contribs/lambdadelta/ground/arith/nat.ma  |  4 +-
 .../contribs/lambdadelta/ground/arith/nat.txt |  5 +-
 .../lambdadelta/ground/arith/nat_le.ma        |  4 +-
 .../lambdadelta/ground/arith/nat_lt.ma        | 14 ++--
 .../lambdadelta/ground/arith/nat_lt_minus.ma  |  2 +-
 .../ground/arith/nat_lt_minus_plus.ma         |  2 +-
 .../lambdadelta/ground/arith/nat_max.ma       | 73 +++++++++++++++++++
 .../lambdadelta/ground/arith/nat_minus.ma     |  2 +-
 .../lambdadelta/ground/arith/nat_plus.ma      |  3 +-
 .../lambdadelta/ground/arith/nat_pred.ma      |  3 +-
 .../lambdadelta/ground/arith/nat_pred_succ.ma |  2 +-
 .../lambdadelta/ground/arith/nat_succ.ma      |  2 +-
 .../lambdadelta/ground/arith/nat_succ_tri.ma  | 25 +++++++
 .../lambdadelta/ground/arith/nat_tri.ma       | 58 +++++++++++++++
 .../lambdadelta/ground/arith/pnat_plus.ma     |  2 +-
 .../lambdadelta/ground/arith/pnat_tri.ma      | 53 ++++++++++++++
 .../lambdadelta/ground/web/ground_src.tbl     |  7 +-
 17 files changed, 238 insertions(+), 23 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
 create mode 100644 matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat.ma
index 1bc7286b6..80a2aa200 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.ma
@@ -25,7 +25,9 @@ inductive nat: Type[0] ≝
 
 coercion ninj.
 
-interpretation "zero (non-negative integers" 'Zero = nzero.
+interpretation
+  "zero (non-negative integers)"
+  'Zero = nzero.
 
 (* Basic inversions *********************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
index 2bd0eabca..915a45dbf 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt
@@ -117,17 +117,18 @@
 "cic:/matita/arithmetics/nat/lt_inv_plus_l.con"
 "cic:/matita/arithmetics/nat/lt_minus_to_plus.con"
 "cic:/matita/arithmetics/nat/lt_minus_to_plus_r.con"
+#
+"cic:/matita/arithmetics/nat/max.con"
+"cic:/matita/arithmetics/nat/commutative_max.con"
 
 ####################################
 
 "cic:/matita/arithmetics/nat/to_max.con"
-"cic:/matita/arithmetics/nat/commutative_max.con"
 "cic:/matita/arithmetics/nat/leb.con"
 "cic:/matita/arithmetics/nat/leb_elim.con"
 "cic:/matita/arithmetics/nat/le_maxl.con"
 "cic:/matita/arithmetics/nat/le_maxr.con"
 "cic:/matita/arithmetics/nat/le_to_leb_true.con"
-"cic:/matita/arithmetics/nat/max.con"
 "cic:/matita/arithmetics/nat/not_le_to_leb_false.con"
 
 "cic:/matita/arithmetics/nat/nat_discr.con"
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
index 73c143964..ae98e3a5e 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
@@ -45,7 +45,7 @@ lemma nle_succ_bi (m) (n): m ≤ n → ↑m ≤ ↑n.
 qed.
 
 (*** le_or_ge *)
-lemma nle_ge_e (m) (n): ∨∨ m ≤ n | n ≤ m.
+lemma nle_ge_dis (m) (n): ∨∨ m ≤ n | n ≤ m.
 #m @(nat_ind … m) -m [ /2 width=1 by or_introl/ ]
 #m #IH #n @(nat_ind … n) -n [ /2 width=1 by or_intror/ ]
 #n #_ elim (IH n) -IH /3 width=2 by nle_succ_bi, or_introl, or_intror/
@@ -117,7 +117,7 @@ qed-.
 
 (*** decidable_le *)
 lemma nle_dec (m) (n): Decidable … (m ≤ n).
-#m #n elim (nle_ge_e m n) [ /2 width=1 by or_introl/ ]
+#m #n elim (nle_ge_dis m n) [ /2 width=1 by or_introl/ ]
 #Hnm elim (eq_nat_dec m n) [ #H destruct /2 width=1 by nle_refl, or_introl/ ]
 /4 width=1 by nle_antisym, or_intror/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
index 388c8aace..a8ffe2e4c 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt.ma
@@ -40,25 +40,25 @@ lemma nlt_succ_bi (m) (n): m < n → ↑m < ↑n.
 /2 width=1 by nle_succ_bi/ qed.
 
 (*** le_to_or_lt_eq *)
-lemma nle_lt_eq_e (m) (n): m ≤ n → ∨∨ m < n | m = n.
+lemma nle_lt_eq_dis (m) (n): m ≤ n → ∨∨ m < n | m = n.
 #m #n * -n /3 width=1 by nle_succ_bi, or_introl/
 qed-.
 
 (*** eq_or_gt *)
-lemma eq_gt_e (n): ∨∨ 𝟎 = n | 𝟎 < n.
-#n elim (nle_lt_eq_e (𝟎) n ?)
+lemma eq_gt_dis (n): ∨∨ 𝟎 = n | 𝟎 < n.
+#n elim (nle_lt_eq_dis (𝟎) n ?)
 /2 width=1 by or_introl, or_intror/
 qed-.
 
 (*** lt_or_ge *)
-lemma nlt_ge_e (m) (n): ∨∨ m < n | n ≤ m.
-#m #n elim (nle_ge_e m n) /2 width=1 by or_intror/
-#H elim (nle_lt_eq_e … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
+lemma nlt_ge_dis (m) (n): ∨∨ m < n | n ≤ m.
+#m #n elim (nle_ge_dis m n) /2 width=1 by or_intror/
+#H elim (nle_lt_eq_dis … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
 qed-.
 
 (*** not_le_to_lt *)
 lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n.
-#m #n elim (nlt_ge_e m n) [ // ]
+#m #n elim (nlt_ge_dis m n) [ // ]
 #H #Hn elim Hn -Hn // 
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
index 5ee4b80eb..bf889def7 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
@@ -38,7 +38,7 @@ qed.
 
 (* Destructions with nminus *************************************************)
 
-lemma nlt_fwd_minus_dx (o) (m) (n): m < n - o → o < n.
+lemma nlt_des_minus_dx (o) (m) (n): m < n - o → o < n.
 #o elim o -o
 [ #m #n <nminus_zero_dx
   /2 width=3 by le_nlt_trans/
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus_plus.ma
index 0f0106021..61cc525ad 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus_plus.ma
@@ -47,5 +47,5 @@ qed-.
 lemma nlt_inv_minus_dx (o) (m) (n): m < n - o → m + o < n.
 #o #m #n #Ho
 lapply (nle_inv_minus_dx ???? Ho) //
-/3 width=2 by nlt_fwd_minus_dx, nlt_des_le/
+/3 width=2 by nlt_des_minus_dx, nlt_des_le/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
new file mode 100644
index 000000000..0032637b1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
@@ -0,0 +1,73 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/notation/functions/zero_0.ma".
+include "ground/arith/nat_succ_tri.ma".
+
+(* MAXIMUM FOR NON-NEGATIVE INTEGERS ****************************************)
+
+(*** max *)
+definition nmax: nat → nat → nat ≝
+           λm,n. ntri … m n n n m.
+
+interpretation
+  "maximum (non-negative integers)"
+  'or m n = (nmax m n).
+
+(* Basic rewrites ***********************************************************)
+
+(*** max_O1 *)
+lemma nmax_zero_sn (n2): n2 = (𝟎 ∨ n2).
+* //
+qed.
+
+(*** max_O2 *)
+lemma nmax_zero_dx (n1): n1 = (n1 ∨ 𝟎).
+* //
+qed.
+
+(*** max_SS *)
+lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2).
+#n1 #n2
+@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because δ-expansion  gets in the way *)
+<ntri_f_tri //
+qed.
+
+(* Advanced rewrites ********************************************************)
+
+(*** idempotent_max *)
+lemma nmax_idem (n): n = (n ∨ n).
+/2 width=1 by ntri_eq/ qed.
+
+(*** commutative_max *)
+lemma nmax_comm: commutative … nmax.
+#m #n @(nat_ind_2 … m n) -m -n //
+qed-.
+
+(*** associative_max *)
+lemma nmax_assoc: associative … nmax.
+#n1 elim n1 -n1 //
+#n1 #IH #n2 elim n2 -n2 //
+#n2 #_ #n3 elim n3 -n3 //
+qed-.
+
+(* Basic inversions *********************************************************)
+
+(*** max_inv_O3 *)
+lemma nmax_inv_zero (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
+#n1 elim n1 -n1 [ /2 width=1 by conj/ ]
+#n1 #_ #n2 elim n2 -n2 [ /2 width=1 by conj/ ]
+#n2 #_ <nmax_succ_bi #H
+elim (eq_inv_nzero_succ … H)
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
index 8129ad55c..788435570 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_minus.ma
@@ -22,7 +22,7 @@ definition nminus: nat → nat → nat ≝
            λm,n. npred^n m.
 
 interpretation
-  "minus (positive integers"
+  "minus (positive integers)"
   'minus m n = (nminus m n).
 
 (* Basic rewrites ***********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
index 75349d2da..d9c82ae33 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_plus.ma
@@ -21,7 +21,7 @@ definition nplus: nat → nat → nat ≝
            λm,n. nsucc^n m.
 
 interpretation
-  "plus (positive integers"
+  "plus (positive integers)"
   'plus m n = (nplus m n).
 
 (* Basic rewrites ***********************************************************)
@@ -40,6 +40,7 @@ lemma nplus_succ_dx (m) (n): ↑(m+n) = m + ↑n.
 #m #n @(niter_succ … nsucc)
 qed.
 
+(*** plus_S1 *)
 lemma nplus_succ_sn (m) (n): ↑(m+n) = ↑m + n.
 #m #n @(niter_appl … nsucc)
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
index 4fcab387d..3d6655065 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred.ma
@@ -25,10 +25,11 @@ definition npred (m): nat ≝ match m with
 ].
 
 interpretation
-  "predecessor (non-negative integers"
+  "predecessor (non-negative integers)"
   'DownArrow m = (npred m).
 
 (* Basic rewrites ***********************************************************)
 
+(*** pred_O *)
 lemma npred_zero: 𝟎 = ↓𝟎.
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
index 26f5f9152..f21156455 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_pred_succ.ma
@@ -19,7 +19,7 @@ include "ground/arith/nat_pred.ma".
 
 (* Rewrites with nsucc ******************************************************)
 
-(*** pred_Sn *)
+(*** pred_Sn pred_S *)
 lemma npred_succ (n): n = ↓↑n.
 * //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
index a1532adeb..923b235e6 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ.ma
@@ -22,7 +22,7 @@ definition nsucc: nat → nat ≝ λm. match m with
 ].
 
 interpretation
-  "successor (non-negative integers"
+  "successor (non-negative integers)"
   'UpArrow m = (nsucc m).
 
 (* Basic rewrites ***********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma
new file mode 100644
index 000000000..e3be44c68
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_succ_tri.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/arith/nat_tri.ma".
+include "ground/arith/nat_succ.ma".
+
+(* SUCCESSOR FOR NON-NEGATIVE INTEGERS **************************************)
+
+(* Rewrites with ntri *******************************************************)
+
+lemma ntri_succ_bi (A) (a1) (a2) (a3) (n1) (n2):
+      ntri A (n1) (n2) a1 a2 a3 = ntri A (↑n1) (↑n2) a1 a2 a3.
+#A #a1 #a2 #a3 * [| #p1 ] * //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
new file mode 100644
index 000000000..b5be40624
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/arith/pnat_tri.ma".
+include "ground/arith/nat.ma".
+
+(* TRICHOTOMY OPERATOR FOR NON-NEGATIVE INTEGERS ****************************)
+
+(* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
+(*** tri *)
+definition ntri (A:Type[0]) (n1) (n2) (a1) (a2) (a3): A ≝
+  match n1 with
+  [ nzero    ⇒ match n2 with [ nzero ⇒ a2 | ninj p2 ⇒ a1 ]
+  | ninj  p1 ⇒ match n2 with [ nzero ⇒ a3 | ninj p2 ⇒ ptri A p1 p2 a1 a2 a3 ]
+  ].
+
+(* Basic rewrites ***********************************************************)
+
+lemma ntri_zero_bi (A) (a1) (a2) (a3):
+      a2 = ntri A (𝟎) (𝟎) a1 a2 a3.
+// qed.
+
+lemma ntri_zero_inj (A) (a1) (a2) (a3) (p):
+      a1 = ntri A (𝟎) (ninj p) a1 a2 a3.
+// qed.
+
+lemma ntri_inj_zero (A) (a1) (a2) (a3) (p):
+      a3 = ntri A (ninj p) (𝟎) a1 a2 a3.
+// qed.
+
+lemma ntri_inj_bi (A) (a1) (a2) (a3) (p1) (p2):
+      ptri A (p1) (p2) a1 a2 a3 = ntri A (p1) (p2) a1 a2 a3.
+// qed.
+
+(* Advanced rewrites ********************************************************)
+
+(*** tri_eq *)
+lemma ntri_eq (A) (a1) (a2) (a3) (n): a2 = ntri A n n a1 a2 a3.
+#A #a1 #a2 #a3 * //
+qed.
+
+lemma ntri_f_tri (A) (B) (f) (a1) (a2) (a3) (n1) (n2):
+      f (ntri A n1 n2 a1 a2 a3) = ntri B n1 n2 (f a1) (f a2) (f a3).
+#A #B #f #a1 #a2 #a3
+* [| #p1 ] * // #p2
+<ntri_inj_bi <ntri_inj_bi //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
index 53d5236f3..e6db03ac4 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_plus.ma
@@ -20,7 +20,7 @@ definition pplus: pnat → pnat → pnat ≝
            λp,q. psucc^q p.
 
 interpretation
-  "plus (positive integers"
+  "plus (positive integers)"
   'plus p q = (pplus p q).
 
 (* Basic rewrites ***********************************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma
new file mode 100644
index 000000000..617849d8f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_tri.ma
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "ground/arith/pnat.ma".
+
+(* TRICHOTOMY OPERATOR FOR POSITIVE INTEGERS ********************************)
+
+rec definition ptri (A:Type[0]) p1 p2 a1 a2 a3 on p1 : A ≝
+  match p1 with
+  [ punit    ⇒ match p2 with [ punit ⇒ a2 | psucc p2 ⇒ a1 ]
+  | psucc p1 ⇒ match p2 with [ punit ⇒ a3 | psucc p2 ⇒ ptri A p1 p2 a1 a2 a3 ]
+  ].
+
+(* Basic rewrites ***********************************************************)
+
+lemma ptri_unit_bi (A) (a1) (a2) (a3):
+      a2 = ptri A (𝟏) (𝟏) a1 a2 a3.
+// qed.
+
+lemma ptri_unit_succ (A) (a1) (a2) (a3) (p):
+      a1 = ptri A (𝟏) (↑p) a1 a2 a3.
+// qed.
+
+lemma ptri_succ_unit (A) (a1) (a2) (a3) (p):
+      a3 = ptri A (↑p) (𝟏) a1 a2 a3.
+// qed.
+
+lemma ptri_succ_bi (A) (a1) (a2) (a3) (p1) (p2):
+      ptri A (p1) (p2) a1 a2 a3 = ptri A (↑p1) (↑p2) a1 a2 a3.
+// qed.
+
+(* Advanced rewrites ********************************************************)
+
+lemma ptri_eq (A) (a1) (a2) (a3) (p): a2 = ptri A p p a1 a2 a3.
+#A #a1 #a2 #a3 #p elim p -p //
+qed.
+
+lemma ptri_f_tri (A) (B) (f) (a1) (a2) (a3) (p1) (p2):
+      f (ptri A p1 p2 a1 a2 a3) = ptri B p1 p2 (f a1) (f a2) (f a3).
+#A #B #f #a1 #a2 #a3 #p1
+elim p1 -p1 [| #p1 #IH ] * //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 0cf803bce..ce8d9855c 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -61,16 +61,17 @@ table {
       [ { "non-negative integers" * } {
           [ "nat_lt ( ?&lt;? )" "nat_lt_pred" "nat_lt_plus" "nat_lt_minus" "nat_lt_minus_plus" * ]
           [ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" * ]
+          [ "nat_max ( ?∨? )" * ]
           [ "nat_minus ( ?-? )" "nat_minus_plus" * ]
           [ "nat_plus ( ?+? )" * ]
           [ "nat_pred ( ↓? )" "nat_pred_succ" * ]
-          [ "nat_succ ( ↑? )" "nat_succ_iter" * ]
-          [ "nat ( 𝟎 )" "nat_iter ( ?^{?}? )" * ]
+          [ "nat_succ ( ↑? )" "nat_succ_iter" "nat_succ_tri" * ]
+          [ "nat ( 𝟎 )" "nat_iter ( ?^{?}? )" *"nat_tri"  ]
         }
       ]
       [ { "positive integers" * } {
           [ "pnat_plus ( ?+? )" * ]
-          [ "pnat ( 𝟏 ) ( ↑? )" "pnat_dis" "pnat_iter ( ?^{?}? )" * ]
+          [ "pnat ( 𝟏 ) ( ↑? )" "pnat_dis" "pnat_iter ( ?^{?}? )" *"pnat_tri"  ]
         }
       ]
     }
-- 
2.39.2