---

Step * of Lemma evodd-induction2

∀[Q:b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ]
  (Q[tt;evodd-zero()]
  ⇒ (∀b:𝔹. ∀x:pw-evenodd() b.  (Q[b;x] ⇒ Q[¬bb;evodd-succ(x)]))
  ⇒ (∀b:𝔹. ∀n:pw-evenodd() b.  Q[b;n]))
BY
{ (InstLemma `evodd-induction` []
   THEN ParallelLast'
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (D -3 THENM Trivial)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN D -1
   THEN Reduce 0
   THEN Auto
   THEN D -3) }

1
1. [Q] : b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ
2. Q[tt;evodd-zero()]
3. ∀b:𝔹. ∀x:pw-evenodd() b.  (Q[b;x] ⇒ Q[¬bb;evodd-succ(x)])
4. b : 𝔹
5. x : b = tt
6. f : Void ⟶ (pw-evenodd() (¬bb))
7. ∀x:Void. Q[¬bb;f x]
⊢ Q[b;pW-sup(inl Ax;f)]

2
1. [Q] : b:𝔹 ⟶ (pw-evenodd() b) ⟶ ℙ
2. Q[tt;evodd-zero()]
3. ∀b:𝔹. ∀x:pw-evenodd() b.  (Q[b;x] ⇒ Q[¬bb;evodd-succ(x)])
4. b : 𝔹
5. y : 0 = 0 ∈ ℤ
6. f : Unit ⟶ (pw-evenodd() (¬bb))
7. ∀x:Unit. Q[¬bb;f x]
⊢ Q[b;pW-sup(inr Ax ;f)]

---

Latex:

---

Latex:
\mforall{}[Q:b:\mBbbB{}  {}\mrightarrow{}  (pw-evenodd()  b)  {}\mrightarrow{}  \mBbbP{}]
    (Q[tt;evodd-zero()]
    {}\mRightarrow{}  (\mforall{}b:\mBbbB{}.  \mforall{}x:pw-evenodd()  b.    (Q[b;x]  {}\mRightarrow{}  Q[\mneg{}\msubb{}b;evodd-succ(x)]))
    {}\mRightarrow{}  (\mforall{}b:\mBbbB{}.  \mforall{}n:pw-evenodd()  b.    Q[b;n]))


By

---

Latex:
(InstLemma  `evodd-induction`  []
  THEN  ParallelLast'
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (D  -3  THENM  Trivial)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto
  THEN  D  -3)

---

Home Index