---

Step * of Lemma sparse-signed-rep-exists-ext

∀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
{ xxxExtract of Obid: sparse-signed-rep-exists
     not unfolding  evalall listops sparse-rep-base special-mod4-decomp
     finishing with Auto
     normalizes to:
     
     λm.letrec rep(m)=... in
         rep(m)xxx }

---

Latex:

---

Latex:
\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:
xxxExtract  of  Obid:  sparse-signed-rep-exists
      not  unfolding    evalall  listops  sparse-rep-base  special-mod4-decomp
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}m.letrec  rep(m)=if  m=0
                                        then  []
                                        else  eval  p  =  special-mod4-decomp(m)  in
                                                  let  k,r  =  p 
                                                  in  eval  z  =  evalall(rep  k)  in
                                                        eval  L1  =  sparse-rep-base(r)  in
                                                            if  null(z)
                                                            then  if  L1[1]=0  then  if  L1[0]=0  then  []  else  [L1[0]]  else  L1
                                                            else  L1  @  z
                                                            fi    in
              rep(m)xxx

---

Home Index