---

Step * of Lemma efficient-exp-ext

∀i:ℤ. ∀n:ℕ.  (∃j:{ℤ| (j = i^n ∈ ℤ)})
BY
{ Extract of Obid: efficient-exp
  normalizes to:
  
  λi.fix((λrec,n. if n=1
                     then i
                     else if n=0
                             then 1
                             else eval m = n ÷ 2 in
                                  eval e = rec m in
                                    if n rem 2=0  then e * e  else (i * e * e)))
  finishing with Auto }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  efficient-exp
normalizes  to:

\mlambda{}i.fix((\mlambda{}rec,n.  if  n=1
                                      then  i
                                      else  if  n=0
                                                      then  1
                                                      else  eval  m  =  n  \mdiv{}  2  in
                                                                eval  e  =  rec  m  in
                                                                    if  n  rem  2=0    then  e  *  e    else  (i  *  e  *  e)))
finishing  with  Auto

---

Home Index