---

Step * 2 of Lemma qlog-lemma


1. e : {e:ℚ| 0 < e} 
2. q : {q:ℚ| (e ≤ q) ∧ q < 1} 
3. ∀[d:ℕ]
     ∀k:ℕ+. ∀r:{r:ℚ| (e ≤ r) ∧ (r = q ↑ k ∈ ℚ) ∧ q ↑ d * r < e} .
       {nz:ℕ × ℚ| let n,z = nz in (z = q ↑ n ∈ ℚ) ∧ (e ≤ z) ∧ z * z < e} 
⊢ {nr:ℕ × ℚ| let n,r = nr in (r = q ↑ n ∈ ℚ) ∧ (e ≤ r) ∧ r * r < e} 
BY
{ ((Assert ↓∃N:ℕ+. q ↑ N < e BY
          ((InstLemma `qlog-bound` [⌜e⌝;⌜q⌝]⋅ THENM D 0) THEN Auto))
   THEN D -1
   THEN InstHyp [⌜(fst(%)) - 1⌝;⌜1⌝;⌜q⌝] (-2)⋅
   THEN Try (Complete (Auto))
   THEN (D (-1) THEN Reduce 0 THEN Try (Complete (Auto)))
   THEN D 2
   THEN D 1
   THEN MemTypeCD
   THEN Auto
   THEN (RWW "exp_unroll_q< qexp1" 0 THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
2.  q  :  \{q:\mBbbQ{}|  (e  \mleq{}  q)  \mwedge{}  q  <  1\} 
3.  \mforall{}[d:\mBbbN{}]
          \mforall{}k:\mBbbN{}\msupplus{}.  \mforall{}r:\{r:\mBbbQ{}|  (e  \mleq{}  r)  \mwedge{}  (r  =  q  \muparrow{}  k)  \mwedge{}  q  \muparrow{}  d  *  r  <  e\}  .
              \{nz:\mBbbN{}  \mtimes{}  \mBbbQ{}|  let  n,z  =  nz  in  (z  =  q  \muparrow{}  n)  \mwedge{}  (e  \mleq{}  z)  \mwedge{}  z  *  z  <  e\} 
\mvdash{}  \{nr:\mBbbN{}  \mtimes{}  \mBbbQ{}|  let  n,r  =  nr  in  (r  =  q  \muparrow{}  n)  \mwedge{}  (e  \mleq{}  r)  \mwedge{}  r  *  r  <  e\} 


By

---

Latex:
((Assert  \mdownarrow{}\mexists{}N:\mBbbN{}\msupplus{}.  q  \muparrow{}  N  <  e  BY
                ((InstLemma  `qlog-bound`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENM  D  0)  THEN  Auto))
  THEN  D  -1
  THEN  InstHyp  [\mkleeneopen{}(fst(\%))  -  1\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]  (-2)\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  (D  (-1)  THEN  Reduce  0  THEN  Try  (Complete  (Auto)))
  THEN  D  2
  THEN  D  1
  THEN  MemTypeCD
  THEN  Auto
  THEN  (RWW  "exp\_unroll\_q<  qexp1"  0  THEN  Auto)\mcdot{})

---

Home Index