---

Step * of Lemma qlog-lemma-ext

∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (e ≤ q) ∧ q < 1} .  {nr:ℕ × ℚ| let n,r = nr in (r = q ↑ n ∈ ℚ) ∧ (e ≤ r) ∧ r * r < e} 
BY
{ xxxExtract of Obid: qlog-lemma
     not unfolding  qrep qeq q_less qmul qdiv qadd qpositive qsub
     finishing with Auto
     normalizes to:
     
     λe,q. (letrec loglemma(k)=λr.eval m = 2 * k in
                                  eval rr = r * r in
                                    if qpositive(e - rr) then <k, r> else loglemma m rr fi  in
             loglemma(1) 
            q)xxx }

---

Latex:

---

Latex:
\mforall{}e:\{e:\mBbbQ{}|  0  <  e\}  .  \mforall{}q:\{q:\mBbbQ{}|  (e  \mleq{}  q)  \mwedge{}  q  <  1\}  .
    \{nr:\mBbbN{}  \mtimes{}  \mBbbQ{}|  let  n,r  =  nr  in  (r  =  q  \muparrow{}  n)  \mwedge{}  (e  \mleq{}  r)  \mwedge{}  r  *  r  <  e\} 


By

---

Latex:
xxxExtract  of  Obid:  qlog-lemma
      not  unfolding    qrep  qeq  q\_less  qmul  qdiv  qadd  qpositive  qsub
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}e,q.  (letrec  loglemma(k)=\mlambda{}r.eval  m  =  2  *  k  in
                                                                eval  rr  =  r  *  r  in
                                                                    if  qpositive(e  -  rr)  then  <k,  r>  else  loglemma  m  rr  fi    in
                      loglemma(1) 
                    q)xxx

---

Home Index