---

Step * 1 of Lemma near-arcsine_wf

.....equality..... 
1. a : {a:ℝ| a ∈ (r(-1), r1)} 
2. N : ℕ+
⊢ near-arcsine(a;N) ~ TERMOF{near-arcsine-exists-ext:o, 1:l} a N
BY
{ (RW (SubC (TagC (mk_tag_term 1))) 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....equality..... 
1.  a  :  \{a:\mBbbR{}|  a  \mmember{}  (r(-1),  r1)\} 
2.  N  :  \mBbbN{}\msupplus{}
\mvdash{}  near-arcsine(a;N)  \msim{}  TERMOF\{near-arcsine-exists-ext:o,  1:l\}  a  N


By

---

Latex:
(RW  (SubC  (TagC  (mk\_tag\_term  1)))  0  THEN  Reduce  0  THEN  Auto)

---

Home Index