(* *)
(**************************************************************************)
-include "ground/notation/functions/zero_0.ma".
include "ground/arith/nat_succ_tri.ma".
(* MAXIMUM FOR NON-NEGATIVE INTEGERS ****************************************)
"maximum (non-negative integers)"
'or m n = (nmax m n).
-(* Basic rewrites ***********************************************************)
+(* Basic constructions ******************************************************)
(*** max_O1 *)
lemma nmax_zero_sn (n2): n2 = (๐ โจ n2).
(*** 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 *)
+@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because ฮด-expansion gets in the way *)
<ntri_f_tri //
qed.
-(* Advanced rewrites ********************************************************)
+(* Advanced constructions ***************************************************)
(*** idempotent_max *)
lemma nmax_idem (n): n = (n โจ n).
(*** commutative_max *)
lemma nmax_comm: commutative โฆ nmax.
-#m #n @(nat_ind_2 โฆ m n) -m -n //
+#m #n @(nat_ind_2_succ โฆ 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-.
+#n1 #n2 @(nat_ind_2_succ โฆ n1 n2) -n1 -n2 //
+#n1 #n2 #IH #n3 @(nat_ind_succ โฆ n3) -n3 //
+qed.
+
+lemma nmax_max_comm_23 (o:nat) (m) (n): (o โจ m โจ n) = (o โจ n โจ m).
+#o #m #n >nmax_assoc >nmax_assoc <nmax_comm in โข (??(??%)?); //
+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)
+lemma eq_inv_zero_nmax (n1) (n2): ๐ = (n1 โจ n2) โ โงโง ๐ = n1 & ๐ = n2.
+#n1 #n2 @(nat_ind_2_succ โฆ n1 n2) -n1 -n2 /2 width=1 by conj/
+#n1 #n2 #_ <nmax_succ_bi #H
+elim (eq_inv_zero_nsucc โฆ H)
qed-.
+
+(*** max_inv_O3 *)
+lemma eq_inv_nmax_zero (n1) (n2): (n1 โจ n2) = ๐ โ โงโง ๐ = n1 & ๐ = n2.
+/2 width=1 by eq_inv_zero_nmax/ qed-.