---

Step * of Lemma small-sparse-rep-ext

∀r:{-2..3-}
  (∃L:{-1..2-} List [((r = Σi<||L||.L[i]*2^i ∈ ℤ)
                    ∧ (||L|| = 2 ∈ ℤ)
                    ∧ (∀i:ℕ||L|| - 1. ((L[i] = 0 ∈ ℤ) ∨ (L[i + 1] = 0 ∈ ℤ))))])
BY
{ xxxExtract of Obid: small-sparse-rep
     not unfolding  listops
     finishing with Auto
     normalizes to:
     
     λr.if r=-2
        then [0; -1]
        else if r=-1 then [-1; 0] else if r=0 then [0; 0] else if r=1 then [1; 0] else if r=2 then [0; 1] else Axxxx }

---

Latex:

---

Latex:
\mforall{}r:\{-2..3\msupminus{}\}
    (\mexists{}L:\{-1..2\msupminus{}\}  List  [((r  =  \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:
xxxExtract  of  Obid:  small-sparse-rep
      not  unfolding    listops
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}r.if  r=-2
            then  [0;  -1]
            else  if  r=-1
                      then  [-1;  0]
                      else  if  r=0  then  [0;  0]  else  if  r=1  then  [1;  0]  else  if  r=2  then  [0;  1]  else  Axxxx

---

Home Index