---

Step * of Lemma qlog-ext

∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (0 ≤ q) ∧ q < 1} .  {n:ℕ+| ((e ≤ 1) ⇒ (e ≤ q ↑ n - 1)) ∧ q ↑ n < e} 
BY
{ xxxExtract of Obid: qlog-exists
     not unfolding  qrep qeq q_less qmul qdiv qadd qpositive qsub
     finishing with Auto
     normalizes to:
     
     λe,q. if qpositive(q - e)
             then letrec qlog(e)=if qpositive(q - e)
                                   then let n1,n2 = 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 
                                        in if n1=1 then 2 else (n1 + (qlog (e/n2)))
                  if qeq(e;q)
                    then let n1,n2 = 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 
                         in if n1=1 then 2 else (n1 + (qlog (e/n2)))
                  else 1
                  fi  in
                   qlog(e)
          if qeq(e;q)
            then letrec qlog(e)=if qpositive(q - e)
                                  then let n1,n2 = 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 
                                       in if n1=1 then 2 else (n1 + (qlog (e/n2)))
                 if qeq(e;q)
                   then let n1,n2 = 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 
                        in if n1=1 then 2 else (n1 + (qlog (e/n2)))
                 else 1
                 fi  in
                  qlog(e)
          else 1
          fi xxx }

---

Latex:

---

Latex:
\mforall{}e:\{e:\mBbbQ{}|  0  <  e\}  .  \mforall{}q:\{q:\mBbbQ{}|  (0  \mleq{}  q)  \mwedge{}  q  <  1\}  .    \{n:\mBbbN{}\msupplus{}|  ((e  \mleq{}  1)  {}\mRightarrow{}  (e  \mleq{}  q  \muparrow{}  n  -  1))  \mwedge{}  q  \muparrow{}  n  <  e\} 


By

---

Latex:
xxxExtract  of  Obid:  qlog-exists
      not  unfolding    qrep  qeq  q\_less  qmul  qdiv  qadd  qpositive  qsub
      finishing  with  Auto
      normalizes  to:
     
      \mlambda{}e,q.  if  qpositive(q  -  e)
                      then  letrec  qlog(e)=if  qpositive(q  -  e)
                                                                  then  let  n1,n2  =  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 
                                                                            in  if  n1=1  then  2  else  (n1  +  (qlog  (e/n2)))
                                if  qeq(e;q)
                                    then  let  n1,n2  =  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 
                                              in  if  n1=1  then  2  else  (n1  +  (qlog  (e/n2)))
                                else  1
                                fi    in
                                  qlog(e)
                if  qeq(e;q)
                    then  letrec  qlog(e)=if  qpositive(q  -  e)
                                                                then  let  n1,n2  =  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 
                                                                          in  if  n1=1  then  2  else  (n1  +  (qlog  (e/n2)))
                              if  qeq(e;q)
                                  then  let  n1,n2  =  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 
                                            in  if  n1=1  then  2  else  (n1  +  (qlog  (e/n2)))
                              else  1
                              fi    in
                                qlog(e)
                else  1
                fi  xxx

---

Home Index