Error

Target

Derivation

1. Initial program 59.9

   \[\frac{1}{x} - \frac{1}{\tan x}\]

2. Taylor expanded around 0 0.4

   \[\leadsto \color{blue}{\frac{1}{3} \cdot x + \left(\frac{1}{45} \cdot {x}^{3} + \frac{2}{945} \cdot {x}^{5}\right)}\]

3. Simplified0.4

   \[\leadsto \color{blue}{(\frac{2}{945} \cdot \left({x}^{5}\right) + \left((\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_* \cdot x\right))_*}\]
4. Using strategy rm

5. Applied add-sqr-sqrt0.4

   \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \left(\color{blue}{\left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}\right)} \cdot x\right))_*\]

6. Applied associate-*l*0.7

   \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \color{blue}{\left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot x\right)\right)})_*\]
7. Using strategy rm

8. Applied add-sqr-sqrt0.7

   \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \left(\sqrt{\color{blue}{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}} \cdot x\right)\right))_*\]

9. Applied sqrt-prod0.7

   \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \left(\color{blue}{\left(\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}} \cdot \sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}\right)} \cdot x\right)\right))_*\]

10. Applied associate-*l*0.5

    \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \color{blue}{\left(\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}} \cdot \left(\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}} \cdot x\right)\right)}\right))_*\]
11. Using strategy rm

12. Applied add-sqr-sqrt0.5

    \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \left(\sqrt{\sqrt{\color{blue}{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}}} \cdot \left(\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}} \cdot x\right)\right)\right))_*\]

13. Applied sqrt-prod0.5

    \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \left(\sqrt{\color{blue}{\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}} \cdot \sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}}} \cdot \left(\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}} \cdot x\right)\right)\right))_*\]

14. Applied sqrt-prod0.5

    \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \left(\color{blue}{\left(\sqrt{\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}} \cdot \sqrt{\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}}\right)} \cdot \left(\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}} \cdot x\right)\right)\right))_*\]

15. Applied associate-*l*0.4

    \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \left(\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*} \cdot \color{blue}{\left(\sqrt{\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}} \cdot \left(\sqrt{\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}} \cdot \left(\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}} \cdot x\right)\right)\right)}\right))_*\]

16. Final simplification0.4

    \[\leadsto (\frac{2}{945} \cdot \left({x}^{5}\right) + \left(\left(\left(\sqrt{\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}} \cdot \left(x \cdot \sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}\right)\right) \cdot \sqrt{\sqrt{\sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}}}\right) \cdot \sqrt{(\frac{1}{45} \cdot \left(x \cdot x\right) + \frac{1}{3})_*}\right))_*\]

Reproduce

herbie shell --seed 2019068 +o rules:numerics
(FPCore (x)
  :name "invcot (example 3.9)"
  :pre (and (< -0.026 x) (< x 0.026))

  :herbie-target
  (if (< (fabs x) 0.026) (* (/ x 3) (+ 1 (/ (* x x) 15))) (- (/ 1 x) (/ 1 (tan x))))

  (- (/ 1 x) (/ 1 (tan x))))