---

Step * of Lemma sparse-rep-base_wf

∀[r:{-2..3-}]
  (sparse-rep-base(r) ∈ {L:{-1..2-} List| 
                         (r = Σi<||L||.L[i]*2^i ∈ ℤ)
                         ∧ (||L|| = 2 ∈ ℤ)
                         ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ)))} )
BY
{ xxxProveWfLemmaxxx }

---

Latex:

---

Latex:
\mforall{}[r:\{-2..3\msupminus{}\}]
    (sparse-rep-base(r)  \mmember{}  \{L:\{-1..2\msupminus{}\}  List| 
                                                  (r  =  \mSigma{}i<||L||.L[i]*2\^{}i)
                                                  \mwedge{}  (||L||  =  2)
                                                  \mwedge{}  (\mforall{}i:\mBbbN{}||L||  -  1.  ((L[i]  =  0)  \mvee{}  (L[i  +  1]  =  0)))\}  )


By

---

Latex:
xxxProveWfLemmaxxx

---

Home Index