---

Step * 1 1 of Lemma fastpi-converges


1. k : ℕ+
⊢ k ≤ 10^20 * 3^eval b = 10^20 in cubic_converge(b;k)
BY
{ ((CallByValueReduce 0⋅ THENA Auto) THEN (GenConclTerm ⌜cubic_converge(10^20;k)⌝⋅ THENA Auto)) }

1
1. k : ℕ+
2. v : {n:ℕ| k ≤ 10^20^3^n} 
3. cubic_converge(10^20;k) = v ∈ {n:ℕ| k ≤ 10^20^3^n} 
⊢ k ≤ 10^20 * 3^v

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  k  \mleq{}  10\^{}20  *  3\^{}eval  b  =  10\^{}20  in  cubic\_converge(b;k)


By

---

Latex:
((CallByValueReduce  0\mcdot{}  THENA  Auto)  THEN  (GenConclTerm  \mkleeneopen{}cubic\_converge(10\^{}20;k)\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index