---

Step * 3 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 ExRepD
   THEN With ⌜k + 1⌝ (D 0)⋅
   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  ExRepD
  THEN  With  \mkleeneopen{}k  +  1\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index