---

Step * 2 of Lemma approx-iter-arcsine_wf


1. a : {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
2. n : ℤ
3. 0 < n
4. ∀[k:ℕ+]. (approx-iter-arcsine(a;k;n - 1) ∈ {y:ℤ| |arcsine-contraction^n - 1(a) - (r(y))/2 * k| ≤ (r(2)/r(k))} )
5. k : ℕ+
⊢ if (n =z 0)
  then a k
  else eval m = n - 1 in
       eval k6 = 6 * k in
       eval k12 = 2 * k6 in
       eval y = approx-iter-arcsine(a;k6;m) in
         arcsine-contraction(a;(r(y))/k12) k
  fi  ∈ {y:ℤ| |arcsine-contraction^n(a) - (r(y))/2 * k| ≤ (r(2)/r(k))} 
BY
{ ((Subst' (n =z 0) ~ ff 0 THENA Auto)
   THEN Reduce 0
   THEN RepeatFor 3 ((CallByValueReduce 0⋅ THENA Auto))
   THEN (InstHyp [⌜6 * k⌝] (-2)⋅ THENA Auto)
   THEN (GenConclTerm ⌜approx-iter-arcsine(a;6 * k;n - 1)⌝⋅ THENA Auto)
   THEN D -2
   THEN (CallByValueReduce 0⋅ THENA Auto)) }

1
1. a : {a:ℝ| (r(-1) < a) ∧ (a < r1)} 
2. n : ℤ
3. 0 < n
4. ∀[k:ℕ+]. (approx-iter-arcsine(a;k;n - 1) ∈ {y:ℤ| |arcsine-contraction^n - 1(a) - (r(y))/2 * k| ≤ (r(2)/r(k))} )
5. k : ℕ+
6. approx-iter-arcsine(a;6 * k;n - 1) ∈ {y:ℤ| |arcsine-contraction^n - 1(a) - (r(y))/2 * 6 * k| ≤ (r(2)/r(6 * k))} 
7. v : ℤ
8. |arcsine-contraction^n - 1(a) - (r(v))/2 * 6 * k| ≤ (r(2)/r(6 * k))
9. approx-iter-arcsine(a;6 * k;n - 1) = v ∈ {y:ℤ| |arcsine-contraction^n - 1(a) - (r(y))/2 * 6 * k| ≤ (r(2)/r(6 * k))} 
⊢ arcsine-contraction(a;(r(v))/2 * 6 * k) k ∈ {y:ℤ| |arcsine-contraction^n(a) - (r(y))/2 * k| ≤ (r(2)/r(k))} 

---

Latex:

---

Latex:

1.  a  :  \{a:\mBbbR{}|  (r(-1)  <  a)  \mwedge{}  (a  <  r1)\} 
2.  n  :  \mBbbZ{}
3.  0  <  n
4.  \mforall{}[k:\mBbbN{}\msupplus{}]
          (approx-iter-arcsine(a;k;n  -  1)  \mmember{}  \{y:\mBbbZ{}| 
                                                                                |arcsine-contraction\^{}n  -  1(a)  -  (r(y))/2
                                                                                *  k|  \mleq{}  (r(2)/r(k))\}  )
5.  k  :  \mBbbN{}\msupplus{}
\mvdash{}  if  (n  =\msubz{}  0)
    then  a  k
    else  eval  m  =  n  -  1  in
              eval  k6  =  6  *  k  in
              eval  k12  =  2  *  k6  in
              eval  y  =  approx-iter-arcsine(a;k6;m)  in
                  arcsine-contraction(a;(r(y))/k12)  k
    fi    \mmember{}  \{y:\mBbbZ{}|  |arcsine-contraction\^{}n(a)  -  (r(y))/2  *  k|  \mleq{}  (r(2)/r(k))\} 


By

---

Latex:
((Subst'  (n  =\msubz{}  0)  \msim{}  ff  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RepeatFor  3  ((CallByValueReduce  0\mcdot{}  THENA  Auto))
  THEN  (InstHyp  [\mkleeneopen{}6  *  k\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}approx-iter-arcsine(a;6  *  k;n  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  (CallByValueReduce  0\mcdot{}  THENA  Auto))

---

Home Index