---

Step * of Lemma special-mod4-decomp_wf

∀[m:ℤ]
  (special-mod4-decomp(m) ∈ {p:ℤ × {-2..3-}| let k,b = p in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))} )
BY
{ xxxProveWfLemmaxxx }

---

Latex:

---

Latex:
\mforall{}[m:\mBbbZ{}]
    (special-mod4-decomp(m)  \mmember{}  \{p:\mBbbZ{}  \mtimes{}  \{-2..3\msupminus{}\}| 
                                                          let  k,b  =  p 
                                                          in  (m  =  ((4  *  k)  +  b))  \mwedge{}  ((|b|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k)))\}  )


By

---

Latex:
xxxProveWfLemmaxxx

---

Home Index