---

Step * 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. x : b = tt
6. f : Void ⟶ (pw-evenodd() (¬bb))
7. ∀x:Void. Q[¬bb;f x]
⊢ pW-sup(inl Ax;f) = evodd-zero() ∈ (pw-evenodd() tt)
BY
{ (Unfolds ``evodd-zero pw-evenodd`` 0 THEN EqCD THEN Auto THEN Ext THEN All Reduce THEN Auto) }

---

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.  x  :  b  =  tt
6.  f  :  Void  {}\mrightarrow{}  (pw-evenodd()  (\mneg{}\msubb{}b))
7.  \mforall{}x:Void.  Q[\mneg{}\msubb{}b;f  x]
\mvdash{}  pW-sup(inl  Ax;f)  =  evodd-zero()


By

---

Latex:
(Unfolds  ``evodd-zero  pw-evenodd``  0  THEN  EqCD  THEN  Auto  THEN  Ext  THEN  All  Reduce  THEN  Auto)

---

Home Index