---

Step * of Lemma sparse-signed-rep-exists

No Annotations
∀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 ∈ ℤ))))])
BY
{ ((Assert ⌜∀[sz:ℕ]
              ∀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 ∈ ℤ))))] 
                supposing |m| ≤ sz⌝⋅
   THENM ((D 0 THENA Auto) THEN InstHyp [⌜|m|⌝;⌜m⌝] 1⋅ THEN Auto)
   )
   THEN UniformCompNatInd
   THEN Auto) }

1
1. [n] : ℕ
2. ∀[m:ℕn]
     ∀m@0:ℤ
       ∃L:{-1..2-} List [((m@0 = Σi<||L||.L[i]*2^i ∈ ℤ)
                        ∧ (0 < ||L|| ⇒ (¬(last(L) = 0 ∈ ℤ)))
                        ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))] 
       supposing |m@0| ≤ m
3. m : ℤ
4. |m| ≤ n
⊢ ∃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 ∈ ℤ))))]

---

Latex:

---

Latex:
No  Annotations
\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))))])


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}[sz:\mBbbN{}]
                        \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))))] 
                            supposing  |m|  \mleq{}  sz\mkleeneclose{}\mcdot{}
  THENM  ((D  0  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}|m|\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  1\mcdot{}  THEN  Auto)
  )
  THEN  UniformCompNatInd
  THEN  Auto)

---

Home Index