---

Step * of Lemma arcsine-approx_wf

∀a:{a:ℝ| ((r(-3)/r(4)) < a) ∧ (a < (r(3)/r(4)))} . ∀n:ℕ+.  (arcsine-approx(a;n) ∈ {x:ℝ| |x - arcsine(a)| ≤ (r1/r(n))} )
BY
{ ((Auto THEN D 1)
   THEN Unfold `arcsine-approx` 0
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN (GenConclTerm ⌜cubic_converge(10;2 * n)⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN RenameVar `j' (-2)
   THEN (Assert r(-1) < r0 BY
               Auto)
   THEN ((Assert (r(3)/r(4)) < r1 BY Auto) THEN (Assert r(-1) < (r(-3)/r(4)) BY Auto))
   THEN (Assert a ∈ {a:ℝ| (r(-1) < a) ∧ (a < r1)}  BY
               Auto)
   THEN (Subst' 2 * 2 * n ~ 4 * n 0 THENA Auto)
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN (GenConclTerm ⌜approx-iter-arcsine(a;4 * n;j)⌝⋅ THENA Auto)
   THEN (CallByValueReduce 0⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN MoveToConcl (-1)
   THEN GenConcl ⌜(r(v))/2 * 4 * n = z ∈ ℝ⌝⋅
   THEN Auto
   THEN MemTypeCD
   THEN Auto) }

1
.....set predicate..... 
1. a : ℝ
2. (r(-3)/r(4)) < a
3. a < (r(3)/r(4))
4. n : ℕ+
5. j : ℕ
6. (2 * n) ≤ 10^3^j
7. r(-1) < r0
8. (r(3)/r(4)) < r1
9. r(-1) < (r(-3)/r(4))
10. a ∈ {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
11. v : ℤ
12. z : ℝ
13. (r(v))/2 * 4 * n = z ∈ ℝ
14. |arcsine-contraction^j(a) - z| ≤ (r(2)/r(4 * n))
⊢ |z - arcsine(a)| ≤ (r1/r(n))

---

Latex:

---

Latex:
\mforall{}a:\{a:\mBbbR{}|  ((r(-3)/r(4))  <  a)  \mwedge{}  (a  <  (r(3)/r(4)))\}  .  \mforall{}n:\mBbbN{}\msupplus{}.
    (arcsine-approx(a;n)  \mmember{}  \{x:\mBbbR{}|  |x  -  arcsine(a)|  \mleq{}  (r1/r(n))\}  )


By

---

Latex:
((Auto  THEN  D  1)
  THEN  Unfold  `arcsine-approx`  0
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}cubic\_converge(10;2  *  n)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  RenameVar  `j'  (-2)
  THEN  (Assert  r(-1)  <  r0  BY
                          Auto)
  THEN  ((Assert  (r(3)/r(4))  <  r1  BY  Auto)  THEN  (Assert  r(-1)  <  (r(-3)/r(4))  BY  Auto))
  THEN  (Assert  a  \mmember{}  \{a:\mBbbR{}|  (r(-1)  <  a)  \mwedge{}  (a  <  r1)\}    BY
                          Auto)
  THEN  (Subst'  2  *  2  *  n  \msim{}  4  *  n  0  THENA  Auto)
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}approx-iter-arcsine(a;4  *  n;j)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  MoveToConcl  (-1)
  THEN  GenConcl  \mkleeneopen{}(r(v))/2  *  4  *  n  =  z\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index