---

Step * 2 of Lemma ni-max-nat


1. n : ℕ
2. m : ℕ
3. n@0 : ℕ@i
4. ↑(ni-max(n∞;m∞) (n@0 + 1))@i
⊢ ↑(ni-max(n∞;m∞) n@0)
BY
{ (RenameVar `i' (-2) THEN RepUR ``ni-max nat2inf`` -1 THEN RepUR ``ni-max nat2inf`` 0) }

1
1. n : ℕ
2. m : ℕ
3. i : ℕ@i
4. ↑(i + 1 <z n ∨bi + 1 <z m)@i
⊢ ↑(i <z n ∨bi <z m)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  n@0  :  \mBbbN{}@i
4.  \muparrow{}(ni-max(n\minfty{};m\minfty{})  (n@0  +  1))@i
\mvdash{}  \muparrow{}(ni-max(n\minfty{};m\minfty{})  n@0)


By

---

Latex:
(RenameVar  `i'  (-2)  THEN  RepUR  ``ni-max  nat2inf``  -1  THEN  RepUR  ``ni-max  nat2inf``  0)

---

Home Index