Nuprl Lemma : sparse-signed-rep-exists

∀m:ℤ
  (∃L:{-1..2-} List [((m = Σi<||L||.L[i]*2^i ∈ ℤ)
                    ∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
                    ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))])


Proof

Error : references
Latex:
\mforall{}m:\mBbbZ{}
    (\mexists{}L:\{-1..2\msupminus{}\}  List  [((m  =  \mSigma{}i<||L||.L[i]*2\^{}i)
                                        \mwedge{}  (0  <  ||L||  {}\mRightarrow{}  (\mneg{}(last(L)  =  0)))
                                        \mwedge{}  (\mforall{}i:\mBbbN{}||L||  -  1.  ((L[i]  =  0)  \mvee{}  (L[i  +  1]  =  0))))])


Date html generated: 2020_05_20-AM-08_42_08
Last ObjectModification: 2020_02_07-AM-09_15_59

Theory : general


Home Index