---

Step * 1 of Lemma odd-or-even


1. n : ℤ@i
2. 0 ≤ (n mod 2)
3. n mod 2 < 2
⊢ (↑isOdd(n)) ∨ (↑isEven(n))
BY
{ (RepUR ``isOdd isEven`` 0 THEN RW assert_pushdownC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}@i
2.  0  \mleq{}  (n  mod  2)
3.  n  mod  2  <  2
\mvdash{}  (\muparrow{}isOdd(n))  \mvee{}  (\muparrow{}isEven(n))


By

---

Latex:
(RepUR  ``isOdd  isEven``  0  THEN  RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index