---

Step * 2 1 1 1 of Lemma evodd-induction2

.....subterm..... T:t
2:n
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)]
⊢ pW-sup(inr Ax ;f) = evodd-succ(f Ax) ∈ (pw-evenodd() b)
BY
{ (Unfolds ``evodd-succ pw-evenodd`` 0 THEN EqCD THEN Auto) }

1
.....subterm..... T:t
2:n
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)]
⊢ f = (λx.(f Ax)) ∈ (b@0:case inr Ax  of inl(x) => Void | inr(x) => Unit ⟶ (pW (¬bb)))

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
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]
9.  Q[\mneg{}\msubb{}\mneg{}\msubb{}b;evodd-succ(f  Ax)]
\mvdash{}  pW-sup(inr  Ax  ;f)  =  evodd-succ(f  Ax)


By

---

Latex:
(Unfolds  ``evodd-succ  pw-evenodd``  0  THEN  EqCD  THEN  Auto)

---

Home Index