---

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 if n rem 2=0
                                     then (rec (n ÷ 2)) * (rec (n ÷ 2))
                                     else (i * (rec (n ÷ 2)) * (rec (n ÷ 2)))))
  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  if  n  rem  2=0
                                                                      then  (rec  (n  \mdiv{}  2))  *  (rec  (n  \mdiv{}  2))
                                                                      else  (i  *  (rec  (n  \mdiv{}  2))  *  (rec  (n  \mdiv{}  2)))))
finishing  with  Auto

---

Home Index