---

Step * of Lemma rcos_wf1

∀[x:ℝ]. (rcos(x) ∈ {y:ℝ| cosine(x) = y} )
BY
{ (Auto
   THEN (InstLemma `approx-arg_wf` [⌜λ2x.cosine(x)⌝;⌜λ2x.-(sine(x))⌝;⌜1⌝;⌜x⌝]⋅ THENA Auto)
   THEN Try ((Unfold `so_lambda` -1 THEN Fold `rcos` (-1)⋅ THEN Auto))) }

1
1. x : ℝ
2. x1 : ℝ
⊢ |-(sine(x1))| ≤ r1

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (rcos(x)  \mmember{}  \{y:\mBbbR{}|  cosine(x)  =  y\}  )


By

---

Latex:
(Auto
  THEN  (InstLemma  `approx-arg\_wf`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.cosine(x)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.-(sine(x))\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Try  ((Unfold  `so\_lambda`  -1  THEN  Fold  `rcos`  (-1)\mcdot{}  THEN  Auto)))

---

Home Index