---

Step * of Lemma sparse-signed-rep_wf

∀[m:ℤ]
  (sparse-signed-rep(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
{ (Auto
   THEN Fold `sq_exists` 0
   THEN Unfold `sparse-signed-rep` 0
   THEN GenConclAtAddr [2;1]
   THEN Subst' evalall(v) ~ v 0
   THEN Try (Trivial)
   THEN D 2
   THEN All Thin) }

1
1. v : {-1..2-} List
⊢ evalall(v) ~ v

---

Latex:

---

Latex:
\mforall{}[m:\mBbbZ{}]
    (sparse-signed-rep(m)  \mmember{}  \{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:
(Auto
  THEN  Fold  `sq\_exists`  0
  THEN  Unfold  `sparse-signed-rep`  0
  THEN  GenConclAtAddr  [2;1]
  THEN  Subst'  evalall(v)  \msim{}  v  0
  THEN  Try  (Trivial)
  THEN  D  2
  THEN  All  Thin)

---

Home Index