---

Step * 2 1 of Lemma evodd-induction2


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]
8. Q[¬bb;f Ax]
⊢ Q[b;pW-sup(inr Ax ;f)]
BY
{ (InstHyp [⌜¬bb⌝;⌜f Ax⌝] 3⋅ THENA Auto) }

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. y : 0 = 0 ∈ ℤ
6. f : Unit ⟶ (pw-evenodd() (¬bb))
7. ∀x:Unit. Q[¬bb;f x]
8. Q[¬bb;f Ax]
9. Q[¬b¬bb;evodd-succ(f Ax)]
⊢ Q[b;pW-sup(inr Ax ;f)]

---

Latex:

---

Latex:

1.  [Q]  :  b:\mBbbB{}  {}\mrightarrow{}  (pw-evenodd()  b)  {}\mrightarrow{}  \mBbbP{}
2.  Q[tt;evodd-zero()]
3.  \mforall{}b:\mBbbB{}.  \mforall{}x:pw-evenodd()  b.    (Q[b;x]  {}\mRightarrow{}  Q[\mneg{}\msubb{}b;evodd-succ(x)])
4.  b  :  \mBbbB{}
5.  y  :  0  =  0
6.  f  :  Unit  {}\mrightarrow{}  (pw-evenodd()  (\mneg{}\msubb{}b))
7.  \mforall{}x:Unit.  Q[\mneg{}\msubb{}b;f  x]
8.  Q[\mneg{}\msubb{}b;f  Ax]
\mvdash{}  Q[b;pW-sup(inr  Ax  ;f)]


By

---

Latex:
(InstHyp  [\mkleeneopen{}\mneg{}\msubb{}b\mkleeneclose{};\mkleeneopen{}f  Ax\mkleeneclose{}]  3\mcdot{}  THENA  Auto)

---

Home Index