---

Step * of Lemma less-efficient-exp-ext

∀i:ℤ. ∀n:ℕ.  (∃j:ℤ [(j = i^n ∈ ℤ)])
BY
{ Extract of Obid: less-efficient-exp
  normalizes to:
  
  λi.fix((λrec,n. if n=1
                  then i
                  else if n=0
                       then 1
                       else let q,r = divrem(n; 2) 
                            in if r=0 then (rec q) * (rec q) else (i * (rec q) * (rec q))))
  finishing with Auto }

---

Latex:

---

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


By

---

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

\mlambda{}i.fix((\mlambda{}rec,n.  if  n=1
                                then  i
                                else  if  n=0
                                          then  1
                                          else  let  q,r  =  divrem(n;  2) 
                                                    in  if  r=0  then  (rec  q)  *  (rec  q)  else  (i  *  (rec  q)  *  (rec  q))))
finishing  with  Auto

---

Home Index