---

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

---

Home Index