---

Step * 1 of Lemma odd-implies


1. n : ℤ@i
2. ↑isOdd(n)@i
⊢ ↑isEven(n - 1)
BY
{ ((RWO "assert-isOdd" (-1) THEN Auto) THEN RWO "assert-isEven" 0 THEN Auto THEN ParallelLast THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}@i
2.  \muparrow{}isOdd(n)@i
\mvdash{}  \muparrow{}isEven(n  -  1)


By

---

Latex:
((RWO  "assert-isOdd"  (-1)  THEN  Auto)
  THEN  RWO  "assert-isEven"  0
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto)

---

Home Index