---

Step * 2 1 of Lemma small-ctrex1-bounds

.....equality..... 
1. |small-ctrex1() - (r(23)/r(2 * 10^1143))| ≤ (r1/r(10^1143))
⊢ 10^1143 ~ 100 * 10^1141
BY
{ TACTIC:(RW (SubC (TagC (mk_tag_term 1000))) 0 THEN Trivial) }

---

Latex:

---

Latex:
.....equality..... 
1.  |small-ctrex1()  -  (r(23)/r(2  *  10\^{}1143))|  \mleq{}  (r1/r(10\^{}1143))
\mvdash{}  10\^{}1143  \msim{}  100  *  10\^{}1141


By

---

Latex:
TACTIC:(RW  (SubC  (TagC  (mk\_tag\_term  1000)))  0  THEN  Trivial)

---

Home Index