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