---

Step * 3 of Lemma small-sparse-rep


1. r : ℤ
2. r = 0 ∈ ℤ
⊢ ∃L:{-1..2-} List [((0 = Σi<||L||.L[i]*2^i ∈ ℤ)
                   ∧ (||L|| = 2 ∈ ℤ)
                   ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))]
BY
{ TACTIC:((With ⌜[0; 0]⌝ (D 0)⋅ THENA Auto)
          THEN Reduce 0
          THEN RepUR ``power-sum last`` 0
          THEN Auto
          THEN IntSegCases (-1)
          THEN Reduce 0
          THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  \mBbbZ{}
2.  r  =  0
\mvdash{}  \mexists{}L:\{-1..2\msupminus{}\}  List  [((0  =  \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:
TACTIC:((With  \mkleeneopen{}[0;  0]\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
                THEN  Reduce  0
                THEN  RepUR  ``power-sum  last``  0
                THEN  Auto
                THEN  IntSegCases  (-1)
                THEN  Reduce  0
                THEN  Auto)

---

Home Index