---

Step * 2 1 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]
9. Q[¬b¬bb;evodd-succ(f Ax)]
⊢ Q[b;pW-sup(inr Ax ;f)]
BY
{ (NthHypEq (-1) 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)]
⊢ pW-sup(inr Ax ;f) = evodd-succ(f Ax) ∈ (pw-evenodd() b)

---

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]
9.  Q[\mneg{}\msubb{}\mneg{}\msubb{}b;evodd-succ(f  Ax)]
\mvdash{}  Q[b;pW-sup(inr  Ax  ;f)]


By

---

Latex:
(NthHypEq  (-1)  THEN  EqCD  THEN  Auto)

---

Home Index