---

Step * 3 of Lemma even-implies


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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "assert-isEven"  (-1)  THEN  Auto)
  THEN  RWO  "assert-isOdd"  0
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto)\mcdot{}

---

Home Index