---

Step * 1 2 1 1 1 of Lemma evodd-enum-surjection


1. b : 𝔹
2. x : pw-evenodd() b
3. a : ℕ
4. a + 1 ≠ 0
5. evodd-enum(a) = <b, x> ∈ (b:𝔹 × (pw-evenodd() b))
⊢ let b,z = evodd-enum(a) in <¬bb, evodd-succ(z)> = <¬bb, evodd-succ(x)> ∈ (b:𝔹 × (pw-evenodd() b))
BY
{ (HypSubst' (-1) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  \mBbbB{}
2.  x  :  pw-evenodd()  b
3.  a  :  \mBbbN{}
4.  a  +  1  \mneq{}  0
5.  evodd-enum(a)  =  <b,  x>
\mvdash{}  let  b,z  =  evodd-enum(a)  in  <\mneg{}\msubb{}b,  evodd-succ(z)>  =  <\mneg{}\msubb{}b,  evodd-succ(x)>


By

---

Latex:
(HypSubst'  (-1)  0  THEN  Auto)

---

Home Index