---

Step * of Lemma faster-sin_wf

∀[x:ℝ]. (faster-sin(x) ∈ {y:ℝ| y = rsin(x)} )
BY
{ (Auto
   THEN Unfold `faster-sin` 0
   THEN (GenConcl ⌜((((x/MachinPi4()))/8 1) ÷ 2) = M ∈ ℤ⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN CallByValueReduce 0
   THEN Auto
   THEN MemTypeCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (faster-sin(x)  \mmember{}  \{y:\mBbbR{}|  y  =  rsin(x)\}  )


By

---

Latex:
(Auto
  THEN  Unfold  `faster-sin`  0
  THEN  (GenConcl  \mkleeneopen{}((((x/MachinPi4()))/8  1)  \mdiv{}  2)  =  M\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  CallByValueReduce  0
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index