---

Step * 1 2 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 + 1) - 1) in <¬bb, evodd-succ(z)> = <¬bb, evodd-succ(x)> ∈ (b:𝔹 × (pw-evenodd() b))
BY
{ (Subst ⌜(a + 1) - 1 ~ a⌝ 0⋅ THEN Auto) }

1
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))

---

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  +  1)  -  1)  in  <\mneg{}\msubb{}b,  evodd-succ(z)>  =  <\mneg{}\msubb{}b,  evodd-succ(x)>


By

---

Latex:
(Subst  \mkleeneopen{}(a  +  1)  -  1  \msim{}  a\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index