---

Step * 1 2 of Lemma sparse-signed-rep-exists


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
5. ¬(m = 0 ∈ ℤ)
⊢ ∃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 0 < n BY
          ((RWO  "absval_ifthenelse" (-2) THENA Auto) THEN SplitOnHypITE -2  THEN Auto'))
   THEN (With ⌜n - 1⌝ (D 2)⋅ THENA Auto)
   ) }

1
1. [n] : ℕ
2. m : ℤ
3. |m| ≤ n
4. ¬(m = 0 ∈ ℤ)
5. 0 < n
6. ∀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| ≤ (n - 1)
⊢ ∃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:

1.  [n]  :  \mBbbN{}
2.  \mforall{}[m:\mBbbN{}n]
          \mforall{}m@0:\mBbbZ{}
              \mexists{}L:\{-1..2\msupminus{}\}  List  [((m@0  =  \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@0|  \mleq{}  m
3.  m  :  \mBbbZ{}
4.  |m|  \mleq{}  n
5.  \mneg{}(m  =  0)
\mvdash{}  \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  0  <  n  BY
                ((RWO    "absval\_ifthenelse"  (-2)  THENA  Auto)  THEN  SplitOnHypITE  -2    THEN  Auto'))
  THEN  (With  \mkleeneopen{}n  -  1\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)
  )

---

Home Index