---

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


1. b : 𝔹
2. x : pw-evenodd() b
3. a : ℕ
4. evodd-enum(a) = <b, x> ∈ (b:𝔹 × (pw-evenodd() b))
⊢ evodd-enum(a + 1) = <¬bb, evodd-succ(x)> ∈ (b:𝔹 × (pw-evenodd() b))
BY
{ (Unfold `evodd-enum` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN Fold `evodd-enum` 0⋅
   THEN Reduce 0
   THEN AutoSplit) }

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 + 1) - 1) 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.  evodd-enum(a)  =  <b,  x>
\mvdash{}  evodd-enum(a  +  1)  =  <\mneg{}\msubb{}b,  evodd-succ(x)>


By

---

Latex:
(Unfold  `evodd-enum`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  Fold  `evodd-enum`  0\mcdot{}
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index