---

Step * of Lemma ni-max-com

∀[x,y:ℕ∞].  (ni-max(x;y) = ni-max(y;x) ∈ ℕ∞)
BY
{ (Auto
   THEN (Assert ni-max(x;y) ∈ ℕ∞ BY
               Auto)
   THEN (MemTypeHD (-1) THENA Auto)
   THEN EqTypeCD
   THEN Auto
   THEN Thin (-1)) }

1
1. x : ℕ∞
2. y : ℕ∞
3. ni-max(x;y) = ni-max(x;y) ∈ (ℕ ⟶ 𝔹)
⊢ ni-max(x;y) = ni-max(y;x) ∈ (ℕ ⟶ 𝔹)

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbN{}\minfty{}].    (ni-max(x;y)  =  ni-max(y;x))


By

---

Latex:
(Auto
  THEN  (Assert  ni-max(x;y)  \mmember{}  \mBbbN{}\minfty{}  BY
                          Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  EqTypeCD
  THEN  Auto
  THEN  Thin  (-1))

---

Home Index