Average Error: 27.6 → 2.4
Time: 1.2m
Precision: 64
Internal Precision: 576
\[\frac{\cos \left(2 \cdot x\right)}{{cos}^{2} \cdot \left(\left(x \cdot {sin}^{2}\right) \cdot x\right)}\]
↓
\[\begin{array}{l} \mathbf{if}\;x \le 9.532002265524216 \cdot 10^{-246}:\\ \;\;\;\;(\left(\frac{\cos x}{\left(sin \cdot x\right) \cdot cos}\right) \cdot \left(\frac{\cos x}{\left(sin \cdot x\right) \cdot cos}\right) + \left(\frac{\frac{-\sin x}{\left(sin \cdot x\right) \cdot cos}}{\frac{\left(sin \cdot x\right) \cdot cos}{\sin x}}\right))_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\cos x \cdot \cos x\right) \cdot \left(\frac{1}{\left(x \cdot \left(cos \cdot sin\right)\right) \cdot \left(x \cdot \left(cos \cdot sin\right)\right)}\right) + \left(-\frac{\frac{\sin x}{x}}{cos \cdot sin} \cdot \frac{\frac{\sin x}{x}}{cos \cdot sin}\right))_*\\ \end{array}\]

Error

Bits error versus x

Bits error versus cos

Bits error versus sin

Derivation

  1. Split input into 2 regimes

  2. if x < 9.532002265524216e-246

    1. Initial program 28.2

      \[\frac{\cos \left(2 \cdot x\right)}{{cos}^{2} \cdot \left(\left(x \cdot {sin}^{2}\right) \cdot x\right)}\]

    2. Initial simplification3.1

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}\]
    3. Using strategy rm

    4. Applied cos-23.2

      \[\leadsto \frac{\color{blue}{\cos x \cdot \cos x - \sin x \cdot \sin x}}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}\]

    5. Applied div-sub3.2

      \[\leadsto \color{blue}{\frac{\cos x \cdot \cos x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)} - \frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\]
    6. Using strategy rm

    7. Applied add-cube-cbrt3.3

      \[\leadsto \frac{\cos x \cdot \cos x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)} - \color{blue}{\left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}}\]

    8. Applied div-inv3.3

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos x\right) \cdot \frac{1}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} - \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\]

    9. Applied prod-diff3.3

      \[\leadsto \color{blue}{(\left(\cos x \cdot \cos x\right) \cdot \left(\frac{1}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}\right) + \left(-\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right)\right))_* + (\left(-\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) + \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right)\right))_*}\]

    10. Simplified4.9

      \[\leadsto \color{blue}{\left(\frac{\cos x \cdot \cos x}{\left(\left(sin \cdot cos\right) \cdot x\right) \cdot \left(\left(sin \cdot cos\right) \cdot x\right)} - \frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right)} + (\left(-\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) + \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right)\right))_*\]

    11. Simplified3.7

      \[\leadsto \left(\frac{\cos x \cdot \cos x}{\left(\left(sin \cdot cos\right) \cdot x\right) \cdot \left(\left(sin \cdot cos\right) \cdot x\right)} - \frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right) + \color{blue}{0}\]
    12. Using strategy rm

    13. Applied *-un-lft-identity3.7

      \[\leadsto \left(\color{blue}{1 \cdot \frac{\cos x \cdot \cos x}{\left(\left(sin \cdot cos\right) \cdot x\right) \cdot \left(\left(sin \cdot cos\right) \cdot x\right)}} - \frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right) + 0\]

    14. Applied prod-diff3.7

      \[\leadsto \color{blue}{\left((1 \cdot \left(\frac{\cos x \cdot \cos x}{\left(\left(sin \cdot cos\right) \cdot x\right) \cdot \left(\left(sin \cdot cos\right) \cdot x\right)}\right) + \left(-\frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right))_* + (\left(-\frac{\frac{\sin x}{x}}{sin \cdot cos}\right) \cdot \left(\frac{\frac{\sin x}{x}}{sin \cdot cos}\right) + \left(\frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right))_*\right)} + 0\]

    15. Simplified3.6

      \[\leadsto \left(\color{blue}{(\left(\frac{\cos x}{\left(x \cdot sin\right) \cdot cos}\right) \cdot \left(\frac{\cos x}{\left(x \cdot sin\right) \cdot cos}\right) + \left(\frac{\frac{-\sin x}{\left(x \cdot sin\right) \cdot cos}}{\frac{\left(x \cdot sin\right) \cdot cos}{\sin x}}\right))_*} + (\left(-\frac{\frac{\sin x}{x}}{sin \cdot cos}\right) \cdot \left(\frac{\frac{\sin x}{x}}{sin \cdot cos}\right) + \left(\frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right))_*\right) + 0\]

    16. Simplified2.4

      \[\leadsto \left((\left(\frac{\cos x}{\left(x \cdot sin\right) \cdot cos}\right) \cdot \left(\frac{\cos x}{\left(x \cdot sin\right) \cdot cos}\right) + \left(\frac{\frac{-\sin x}{\left(x \cdot sin\right) \cdot cos}}{\frac{\left(x \cdot sin\right) \cdot cos}{\sin x}}\right))_* + \color{blue}{0}\right) + 0\]

    if 9.532002265524216e-246 < x

    1. Initial program 26.9

      \[\frac{\cos \left(2 \cdot x\right)}{{cos}^{2} \cdot \left(\left(x \cdot {sin}^{2}\right) \cdot x\right)}\]

    2. Initial simplification2.5

      \[\leadsto \frac{\cos \left(2 \cdot x\right)}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}\]
    3. Using strategy rm

    4. Applied cos-22.6

      \[\leadsto \frac{\color{blue}{\cos x \cdot \cos x - \sin x \cdot \sin x}}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}\]

    5. Applied div-sub2.6

      \[\leadsto \color{blue}{\frac{\cos x \cdot \cos x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)} - \frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\]
    6. Using strategy rm

    7. Applied add-cube-cbrt2.7

      \[\leadsto \frac{\cos x \cdot \cos x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)} - \color{blue}{\left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}}\]

    8. Applied div-inv2.7

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos x\right) \cdot \frac{1}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} - \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\]

    9. Applied prod-diff2.7

      \[\leadsto \color{blue}{(\left(\cos x \cdot \cos x\right) \cdot \left(\frac{1}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}\right) + \left(-\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right)\right))_* + (\left(-\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) + \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right)\right))_*}\]

    10. Simplified3.1

      \[\leadsto \color{blue}{\left(\frac{\cos x \cdot \cos x}{\left(\left(sin \cdot cos\right) \cdot x\right) \cdot \left(\left(sin \cdot cos\right) \cdot x\right)} - \frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right)} + (\left(-\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right) + \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \left(\sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}} \cdot \sqrt[3]{\frac{\sin x \cdot \sin x}{\left(\left(x \cdot cos\right) \cdot sin\right) \cdot \left(\left(x \cdot cos\right) \cdot sin\right)}}\right)\right))_*\]

    11. Simplified2.5

      \[\leadsto \left(\frac{\cos x \cdot \cos x}{\left(\left(sin \cdot cos\right) \cdot x\right) \cdot \left(\left(sin \cdot cos\right) \cdot x\right)} - \frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right) + \color{blue}{0}\]
    12. Using strategy rm

    13. Applied div-inv2.5

      \[\leadsto \left(\color{blue}{\left(\cos x \cdot \cos x\right) \cdot \frac{1}{\left(\left(sin \cdot cos\right) \cdot x\right) \cdot \left(\left(sin \cdot cos\right) \cdot x\right)}} - \frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right) + 0\]

    14. Applied fma-neg2.5

      \[\leadsto \color{blue}{(\left(\cos x \cdot \cos x\right) \cdot \left(\frac{1}{\left(\left(sin \cdot cos\right) \cdot x\right) \cdot \left(\left(sin \cdot cos\right) \cdot x\right)}\right) + \left(-\frac{\frac{\sin x}{x}}{sin \cdot cos} \cdot \frac{\frac{\sin x}{x}}{sin \cdot cos}\right))_*} + 0\]
  3. Recombined 2 regimes into one program.

  4. Final simplification2.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \le 9.532002265524216 \cdot 10^{-246}:\\ \;\;\;\;(\left(\frac{\cos x}{\left(sin \cdot x\right) \cdot cos}\right) \cdot \left(\frac{\cos x}{\left(sin \cdot x\right) \cdot cos}\right) + \left(\frac{\frac{-\sin x}{\left(sin \cdot x\right) \cdot cos}}{\frac{\left(sin \cdot x\right) \cdot cos}{\sin x}}\right))_*\\ \mathbf{else}:\\ \;\;\;\;(\left(\cos x \cdot \cos x\right) \cdot \left(\frac{1}{\left(x \cdot \left(cos \cdot sin\right)\right) \cdot \left(x \cdot \left(cos \cdot sin\right)\right)}\right) + \left(-\frac{\frac{\sin x}{x}}{cos \cdot sin} \cdot \frac{\frac{\sin x}{x}}{cos \cdot sin}\right))_*\\ \end{array}\]

Runtime

Time bar (total: 1.2m)Debug logProfile

herbie shell --seed 2018250 +o rules:numerics
(FPCore (x cos sin)
  :name "cos(2*x)/(cos^2(x)*sin^2(x))"
  (/ (cos (* 2 x)) (* (pow cos 2) (* (* x (pow sin 2)) x))))