---

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

∀m:ℤ. (∃p:ℤ × {-2..3-} [let k,b = p in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))])
BY
{ Extract of Obid: sparse-signed-rep-lemma1
  not unfolding  remainder
  finishing with Auto
  normalizes to:
  
  λm.eval qr = divrem(m; 4) in
     let q1,q2 = qr 
     in if q2=3
        then <q1 + 1, -1>
        else if q2=-3
             then <q1 - 1, 1>
             else eval x = q1 rem 2 in
                  if (x) < (0)
                     then if 2 + x=0
                          then <q1, q2>
                          else if q2=2 then <q1 + 1, -2> else if q2=-2 then <q1 - 1, 2> else <q1, q2>
                     else if x=0
                          then <q1, q2>
                          else if q2=2 then <q1 + 1, -2> else if q2=-2 then <q1 - 1, 2> else <q1, q2> }

---

Latex:

---

Latex:
\mforall{}m:\mBbbZ{}.  (\mexists{}p:\mBbbZ{}  \mtimes{}  \{-2..3\msupminus{}\}  [let  k,b  =  p  in  (m  =  ((4  *  k)  +  b))  \mwedge{}  ((|b|  =  2)  {}\mRightarrow{}  (\muparrow{}isEven(k)))])


By

---

Latex:
Extract  of  Obid:  sparse-signed-rep-lemma1
not  unfolding    remainder
finishing  with  Auto
normalizes  to:

\mlambda{}m.eval  qr  =  divrem(m;  4)  in
      let  q1,q2  =  qr 
      in  if  q2=3
            then  <q1  +  1,  -1>
            else  if  q2=-3
                      then  <q1  -  1,  1>
                      else  eval  x  =  q1  rem  2  in
                                if  (x)  <  (0)
                                      then  if  2  +  x=0
                                                then  <q1,  q2>
                                                else  if  q2=2  then  <q1  +  1,  -2>  else  if  q2=-2  then  <q1  -  1,  2>  else  <q1,  q2>
                                      else  if  x=0
                                                then  <q1,  q2>
                                                else  if  q2=2  then  <q1  +  1,  -2>  else  if  q2=-2  then  <q1  -  1,  2>  else  <q1,  q2>

---

Home Index