---

Step * of Lemma efficient-exp-ext

∀i:ℤ. ∀n:ℕ.  (∃j:ℤ [(j = i^n ∈ ℤ)])
BY
{ Extract of Obid: efficient-exp
  not unfolding  genrec
  finishing with Auto
  normalizes to:
  
  λi.eval m = i in
     letrec rec(n)=if n=1
                   then m
                   else if n=0
                        then 1
                        else let x,r = divrem(n; 2) 
                             in eval m' = x in
                                eval e = rec m' in
                                  if r=0 then e * e else (m * e * e) in
      rec  }

---

Latex:

---

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}n:\mBbbN{}.    (\mexists{}j:\mBbbZ{}  [(j  =  i\^{}n)])


By

---

Latex:
Extract  of  Obid:  efficient-exp
not  unfolding    genrec
finishing  with  Auto
normalizes  to:

\mlambda{}i.eval  m  =  i  in
      letrec  rec(n)=if  n=1
                                  then  m
                                  else  if  n=0
                                            then  1
                                            else  let  x,r  =  divrem(n;  2) 
                                                      in  eval  m'  =  x  in
                                                            eval  e  =  rec  m'  in
                                                                if  r=0  then  e  *  e  else  (m  *  e  *  e)  in
        rec 

---

Home Index