2cos (problem 3.3.5)

Percentage Accurate: 38.3% → 99.2%
Time: 17.2s
Alternatives: 17
Speedup: TODO×

Specification

?
\[\cos \left(x + \varepsilon\right) - \cos x \]

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 17 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Alternative 1?

\[\begin{array}{l} t_0 := -\sin x\\ \mathbf{if}\;\varepsilon \leq -0.0029:\\ \;\;\;\;\mathsf{fma}\left(\sin \varepsilon, t_0, \cos \varepsilon \cdot \cos x\right) - \cos x\\ \mathbf{elif}\;\varepsilon \leq 0.002:\\ \;\;\;\;\mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, -0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) + \sin x \cdot \left(0.16666666666666666 \cdot {\varepsilon}^{3} - \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\cos x, \cos \varepsilon, \sin \varepsilon \cdot t_0\right) - \cos x\\ \end{array} \]
Derivation
  1. Split input into 3 regimes

  2. if eps < -0.0029

    1. Initial program 53.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. cos-sum98.7%

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

      2. sub-neg98.7%

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

    3. Applied egg-rr98.7%

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon + \left(-\sin x \cdot \sin \varepsilon\right)\right)} - \cos x \]
    4. Step-by-step derivation

      1. +-commutative98.7%

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

      2. distribute-lft-neg-in98.7%

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

      3. *-commutative98.7%

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

      4. fma-def98.7%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\sin \varepsilon, -\sin x, \cos x \cdot \cos \varepsilon\right)} - \cos x \]

      5. *-commutative98.7%

        \[\leadsto \mathsf{fma}\left(\sin \varepsilon, -\sin x, \color{blue}{\cos \varepsilon \cdot \cos x}\right) - \cos x \]

    5. Simplified98.7%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\sin \varepsilon, -\sin x, \cos \varepsilon \cdot \cos x\right)} - \cos x \]

    if -0.0029 < eps < 2e-3

    1. Initial program 20.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 99.8%

      \[\leadsto \color{blue}{0.041666666666666664 \cdot \left({\varepsilon}^{4} \cdot \cos x\right) + \left(0.16666666666666666 \cdot \left({\varepsilon}^{3} \cdot \sin x\right) + \left(-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)\right)\right)} \]
    3. Step-by-step derivation

      1. fma-def99.8%

        \[\leadsto \color{blue}{\mathsf{fma}\left(0.041666666666666664, {\varepsilon}^{4} \cdot \cos x, 0.16666666666666666 \cdot \left({\varepsilon}^{3} \cdot \sin x\right) + \left(-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)\right)\right)} \]

      2. *-commutative99.8%

        \[\leadsto \mathsf{fma}\left(0.041666666666666664, \color{blue}{\cos x \cdot {\varepsilon}^{4}}, 0.16666666666666666 \cdot \left({\varepsilon}^{3} \cdot \sin x\right) + \left(-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)\right)\right) \]

      3. +-commutative99.8%

        \[\leadsto \mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, \color{blue}{\left(-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)\right) + 0.16666666666666666 \cdot \left({\varepsilon}^{3} \cdot \sin x\right)}\right) \]

      4. associate-+l+99.8%

        \[\leadsto \mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \left(-1 \cdot \left(\varepsilon \cdot \sin x\right) + 0.16666666666666666 \cdot \left({\varepsilon}^{3} \cdot \sin x\right)\right)}\right) \]

      5. unpow299.8%

        \[\leadsto \mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, -0.5 \cdot \left(\color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot \cos x\right) + \left(-1 \cdot \left(\varepsilon \cdot \sin x\right) + 0.16666666666666666 \cdot \left({\varepsilon}^{3} \cdot \sin x\right)\right)\right) \]

      6. associate-*l*99.8%

        \[\leadsto \mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, -0.5 \cdot \color{blue}{\left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right)} + \left(-1 \cdot \left(\varepsilon \cdot \sin x\right) + 0.16666666666666666 \cdot \left({\varepsilon}^{3} \cdot \sin x\right)\right)\right) \]

      7. associate-*r*99.8%

        \[\leadsto \mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, -0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) + \left(\color{blue}{\left(-1 \cdot \varepsilon\right) \cdot \sin x} + 0.16666666666666666 \cdot \left({\varepsilon}^{3} \cdot \sin x\right)\right)\right) \]

      8. associate-*r*99.8%

        \[\leadsto \mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, -0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) + \left(\left(-1 \cdot \varepsilon\right) \cdot \sin x + \color{blue}{\left(0.16666666666666666 \cdot {\varepsilon}^{3}\right) \cdot \sin x}\right)\right) \]

      9. distribute-rgt-out99.8%

        \[\leadsto \mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, -0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) + \color{blue}{\sin x \cdot \left(-1 \cdot \varepsilon + 0.16666666666666666 \cdot {\varepsilon}^{3}\right)}\right) \]

      10. mul-1-neg99.8%

        \[\leadsto \mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, -0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) + \sin x \cdot \left(\color{blue}{\left(-\varepsilon\right)} + 0.16666666666666666 \cdot {\varepsilon}^{3}\right)\right) \]

    4. Simplified99.8%

      \[\leadsto \color{blue}{\mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, -0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) + \sin x \cdot \left(\left(-\varepsilon\right) + 0.16666666666666666 \cdot {\varepsilon}^{3}\right)\right)} \]

    if 2e-3 < eps

    1. Initial program 56.8%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. cos-sum99.0%

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

      2. cancel-sign-sub-inv99.0%

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

      3. fma-def99.1%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\cos x, \cos \varepsilon, \left(-\sin x\right) \cdot \sin \varepsilon\right)} - \cos x \]

    3. Applied egg-rr99.1%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\cos x, \cos \varepsilon, \left(-\sin x\right) \cdot \sin \varepsilon\right)} - \cos x \]
  3. Recombined 3 regimes into one program.

  4. Final simplification99.3%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.0029:\\ \;\;\;\;\mathsf{fma}\left(\sin \varepsilon, -\sin x, \cos \varepsilon \cdot \cos x\right) - \cos x\\ \mathbf{elif}\;\varepsilon \leq 0.002:\\ \;\;\;\;\mathsf{fma}\left(0.041666666666666664, \cos x \cdot {\varepsilon}^{4}, -0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) + \sin x \cdot \left(0.16666666666666666 \cdot {\varepsilon}^{3} - \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\cos x, \cos \varepsilon, \sin \varepsilon \cdot \left(-\sin x\right)\right) - \cos x\\ \end{array} \]

Alternative 2?

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.8 \cdot 10^{-5}:\\ \;\;\;\;\left(\cos \varepsilon \cdot \cos x - \sin \varepsilon \cdot \sin x\right) - \cos x\\ \mathbf{elif}\;\varepsilon \leq 4.3 \cdot 10^{-5}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\cos x, \cos \varepsilon, \sin \varepsilon \cdot \left(-\sin x\right)\right) - \cos x\\ \end{array} \]
Derivation
  1. Split input into 3 regimes

  2. if eps < -4.8000000000000001e-5

    1. Initial program 53.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. cos-sum98.7%

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

    3. Applied egg-rr98.7%

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

    if -4.8000000000000001e-5 < eps < 4.3000000000000002e-5

    1. Initial program 19.7%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 99.9%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg99.9%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg99.9%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow299.9%

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

      4. associate-*l*99.9%

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

    4. Simplified99.9%

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

    if 4.3000000000000002e-5 < eps

    1. Initial program 57.2%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. cos-sum98.2%

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

      2. cancel-sign-sub-inv98.2%

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

      3. fma-def98.2%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\cos x, \cos \varepsilon, \left(-\sin x\right) \cdot \sin \varepsilon\right)} - \cos x \]

    3. Applied egg-rr98.2%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\cos x, \cos \varepsilon, \left(-\sin x\right) \cdot \sin \varepsilon\right)} - \cos x \]
  3. Recombined 3 regimes into one program.

  4. Final simplification99.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.8 \cdot 10^{-5}:\\ \;\;\;\;\left(\cos \varepsilon \cdot \cos x - \sin \varepsilon \cdot \sin x\right) - \cos x\\ \mathbf{elif}\;\varepsilon \leq 4.3 \cdot 10^{-5}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\cos x, \cos \varepsilon, \sin \varepsilon \cdot \left(-\sin x\right)\right) - \cos x\\ \end{array} \]

Alternative 3?

\[\begin{array}{l} t_0 := -\sin x\\ \mathbf{if}\;\varepsilon \leq -4.8 \cdot 10^{-5}:\\ \;\;\;\;\mathsf{fma}\left(\sin \varepsilon, t_0, \cos \varepsilon \cdot \cos x\right) - \cos x\\ \mathbf{elif}\;\varepsilon \leq 3.1 \cdot 10^{-5}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\cos x, \cos \varepsilon, \sin \varepsilon \cdot t_0\right) - \cos x\\ \end{array} \]
Derivation
  1. Split input into 3 regimes

  2. if eps < -4.8000000000000001e-5

    1. Initial program 53.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. cos-sum98.7%

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

      2. sub-neg98.7%

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

    3. Applied egg-rr98.7%

      \[\leadsto \color{blue}{\left(\cos x \cdot \cos \varepsilon + \left(-\sin x \cdot \sin \varepsilon\right)\right)} - \cos x \]
    4. Step-by-step derivation

      1. +-commutative98.7%

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

      2. distribute-lft-neg-in98.7%

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

      3. *-commutative98.7%

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

      4. fma-def98.7%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\sin \varepsilon, -\sin x, \cos x \cdot \cos \varepsilon\right)} - \cos x \]

      5. *-commutative98.7%

        \[\leadsto \mathsf{fma}\left(\sin \varepsilon, -\sin x, \color{blue}{\cos \varepsilon \cdot \cos x}\right) - \cos x \]

    5. Simplified98.7%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\sin \varepsilon, -\sin x, \cos \varepsilon \cdot \cos x\right)} - \cos x \]

    if -4.8000000000000001e-5 < eps < 3.10000000000000014e-5

    1. Initial program 19.7%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 99.9%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg99.9%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg99.9%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow299.9%

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

      4. associate-*l*99.9%

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

    4. Simplified99.9%

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

    if 3.10000000000000014e-5 < eps

    1. Initial program 57.2%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. cos-sum98.2%

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

      2. cancel-sign-sub-inv98.2%

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

      3. fma-def98.2%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\cos x, \cos \varepsilon, \left(-\sin x\right) \cdot \sin \varepsilon\right)} - \cos x \]

    3. Applied egg-rr98.2%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\cos x, \cos \varepsilon, \left(-\sin x\right) \cdot \sin \varepsilon\right)} - \cos x \]
  3. Recombined 3 regimes into one program.

  4. Final simplification99.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.8 \cdot 10^{-5}:\\ \;\;\;\;\mathsf{fma}\left(\sin \varepsilon, -\sin x, \cos \varepsilon \cdot \cos x\right) - \cos x\\ \mathbf{elif}\;\varepsilon \leq 3.1 \cdot 10^{-5}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\cos x, \cos \varepsilon, \sin \varepsilon \cdot \left(-\sin x\right)\right) - \cos x\\ \end{array} \]

Alternative 4?

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -2.5 \cdot 10^{-5} \lor \neg \left(\varepsilon \leq 5 \cdot 10^{-5}\right):\\ \;\;\;\;\cos \varepsilon \cdot \cos x - \left(\cos x + \sin \varepsilon \cdot \sin x\right)\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \end{array} \]
Derivation
  1. Split input into 2 regimes

  2. if eps < -2.50000000000000012e-5 or 5.00000000000000024e-5 < eps

    1. Initial program 55.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. add-log-exp55.4%

        \[\leadsto \color{blue}{\log \left(e^{\cos \left(x + \varepsilon\right) - \cos x}\right)} \]

      2. add-cube-cbrt54.3%

        \[\leadsto \log \color{blue}{\left(\left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}} \cdot \sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right) \cdot \sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right)} \]

      3. log-prod54.3%

        \[\leadsto \color{blue}{\log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}} \cdot \sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right) + \log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right)} \]

    3. Applied egg-rr54.3%

      \[\leadsto \color{blue}{\log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}} \cdot \sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right) + \log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right)} \]
    4. Step-by-step derivation

      1. log-prod54.3%

        \[\leadsto \color{blue}{\left(\log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right) + \log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right)\right)} + \log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right) \]

      2. count-254.3%

        \[\leadsto \color{blue}{2 \cdot \log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right)} + \log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right) \]

      3. distribute-lft1-in54.3%

        \[\leadsto \color{blue}{\left(2 + 1\right) \cdot \log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right)} \]

      4. metadata-eval54.3%

        \[\leadsto \color{blue}{3} \cdot \log \left(\sqrt[3]{e^{\cos \left(x + \varepsilon\right) - \cos x}}\right) \]

      5. sub-neg54.3%

        \[\leadsto 3 \cdot \log \left(\sqrt[3]{e^{\color{blue}{\cos \left(x + \varepsilon\right) + \left(-\cos x\right)}}}\right) \]

      6. +-commutative54.3%

        \[\leadsto 3 \cdot \log \left(\sqrt[3]{e^{\cos \color{blue}{\left(\varepsilon + x\right)} + \left(-\cos x\right)}}\right) \]

      7. sub-neg54.3%

        \[\leadsto 3 \cdot \log \left(\sqrt[3]{e^{\color{blue}{\cos \left(\varepsilon + x\right) - \cos x}}}\right) \]

    5. Simplified54.3%

      \[\leadsto \color{blue}{3 \cdot \log \left(\sqrt[3]{e^{\cos \left(\varepsilon + x\right) - \cos x}}\right)} \]
    6. Step-by-step derivation

      1. add-log-exp54.3%

        \[\leadsto \color{blue}{\log \left(e^{3 \cdot \log \left(\sqrt[3]{e^{\cos \left(\varepsilon + x\right) - \cos x}}\right)}\right)} \]

      2. *-commutative54.3%

        \[\leadsto \log \left(e^{\color{blue}{\log \left(\sqrt[3]{e^{\cos \left(\varepsilon + x\right) - \cos x}}\right) \cdot 3}}\right) \]

      3. exp-to-pow54.2%

        \[\leadsto \log \color{blue}{\left({\left(\sqrt[3]{e^{\cos \left(\varepsilon + x\right) - \cos x}}\right)}^{3}\right)} \]

      4. pow354.3%

        \[\leadsto \log \color{blue}{\left(\left(\sqrt[3]{e^{\cos \left(\varepsilon + x\right) - \cos x}} \cdot \sqrt[3]{e^{\cos \left(\varepsilon + x\right) - \cos x}}\right) \cdot \sqrt[3]{e^{\cos \left(\varepsilon + x\right) - \cos x}}\right)} \]

      5. add-cube-cbrt55.4%

        \[\leadsto \log \color{blue}{\left(e^{\cos \left(\varepsilon + x\right) - \cos x}\right)} \]

      6. add-log-exp55.5%

        \[\leadsto \color{blue}{\cos \left(\varepsilon + x\right) - \cos x} \]

      7. cos-sum98.4%

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

      8. associate--l-98.4%

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

    7. Applied egg-rr98.4%

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

    if -2.50000000000000012e-5 < eps < 5.00000000000000024e-5

    1. Initial program 19.7%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 99.9%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg99.9%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg99.9%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow299.9%

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

      4. associate-*l*99.9%

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

    4. Simplified99.9%

      \[\leadsto \color{blue}{-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification99.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -2.5 \cdot 10^{-5} \lor \neg \left(\varepsilon \leq 5 \cdot 10^{-5}\right):\\ \;\;\;\;\cos \varepsilon \cdot \cos x - \left(\cos x + \sin \varepsilon \cdot \sin x\right)\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \end{array} \]

Alternative 5?

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -9.8 \cdot 10^{-5} \lor \neg \left(\varepsilon \leq 4.2 \cdot 10^{-5}\right):\\ \;\;\;\;\left(\cos \varepsilon \cdot \cos x - \sin \varepsilon \cdot \sin x\right) - \cos x\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \end{array} \]
Derivation
  1. Split input into 2 regimes

  2. if eps < -9.8e-5 or 4.19999999999999977e-5 < eps

    1. Initial program 55.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. cos-sum98.4%

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

    3. Applied egg-rr98.4%

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

    if -9.8e-5 < eps < 4.19999999999999977e-5

    1. Initial program 19.7%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 99.9%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg99.9%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg99.9%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow299.9%

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

      4. associate-*l*99.9%

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

    4. Simplified99.9%

      \[\leadsto \color{blue}{-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification99.1%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -9.8 \cdot 10^{-5} \lor \neg \left(\varepsilon \leq 4.2 \cdot 10^{-5}\right):\\ \;\;\;\;\left(\cos \varepsilon \cdot \cos x - \sin \varepsilon \cdot \sin x\right) - \cos x\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \end{array} \]

Alternative 6?

\[\begin{array}{l} \mathbf{if}\;\cos \left(\varepsilon + x\right) - \cos x \leq -5 \cdot 10^{-8}:\\ \;\;\;\;-2 \cdot {\sin \left(\varepsilon \cdot 0.5\right)}^{2}\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \end{array} \]
Derivation
  1. Split input into 2 regimes

  2. if (-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x)) < -4.9999999999999998e-8

    1. Initial program 83.0%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. diff-cos84.0%

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

      2. div-inv84.0%

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

      3. metadata-eval84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot \color{blue}{0.5}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \]

      4. div-inv84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \color{blue}{\left(\left(\left(x + \varepsilon\right) + x\right) \cdot \frac{1}{2}\right)}\right) \]

      5. +-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\color{blue}{\left(x + \left(x + \varepsilon\right)\right)} \cdot \frac{1}{2}\right)\right) \]

      6. metadata-eval84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot \color{blue}{0.5}\right)\right) \]

    3. Applied egg-rr84.0%

      \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right)} \]
    4. Step-by-step derivation

      1. *-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \color{blue}{\left(0.5 \cdot \left(\left(x + \varepsilon\right) - x\right)\right)} \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

      2. +-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\color{blue}{\left(\varepsilon + x\right)} - x\right)\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

      3. associate--l+83.8%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \color{blue}{\left(\varepsilon + \left(x - x\right)\right)}\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

      4. *-commutative83.8%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \color{blue}{\left(0.5 \cdot \left(x + \left(x + \varepsilon\right)\right)\right)}\right) \]

      5. associate-+r+84.0%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \color{blue}{\left(\left(x + x\right) + \varepsilon\right)}\right)\right) \]

      6. +-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \color{blue}{\left(\varepsilon + \left(x + x\right)\right)}\right)\right) \]

    5. Simplified84.0%

      \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \left(\varepsilon + \left(x + x\right)\right)\right)\right)} \]

    6. Taylor expanded in x around 0 83.5%

      \[\leadsto -2 \cdot \color{blue}{{\sin \left(0.5 \cdot \varepsilon\right)}^{2}} \]

    if -4.9999999999999998e-8 < (-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))

    1. Initial program 15.6%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 74.2%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg74.2%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg74.2%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow274.2%

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

      4. associate-*l*74.2%

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

    4. Simplified74.2%

      \[\leadsto \color{blue}{-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification77.2%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(\varepsilon + x\right) - \cos x \leq -5 \cdot 10^{-8}:\\ \;\;\;\;-2 \cdot {\sin \left(\varepsilon \cdot 0.5\right)}^{2}\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)\right) - \varepsilon \cdot \sin x\\ \end{array} \]

Alternative 7?

\[\begin{array}{l} \mathbf{if}\;\cos \left(\varepsilon + x\right) - \cos x \leq -5 \cdot 10^{-8}:\\ \;\;\;\;-2 \cdot {\sin \left(\varepsilon \cdot 0.5\right)}^{2}\\ \mathbf{else}:\\ \;\;\;\;\varepsilon \cdot \left(\cos x \cdot \left(\varepsilon \cdot -0.5\right) - \sin x\right)\\ \end{array} \]
Derivation
  1. Split input into 2 regimes

  2. if (-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x)) < -4.9999999999999998e-8

    1. Initial program 83.0%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. diff-cos84.0%

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

      2. div-inv84.0%

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

      3. metadata-eval84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot \color{blue}{0.5}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \]

      4. div-inv84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \color{blue}{\left(\left(\left(x + \varepsilon\right) + x\right) \cdot \frac{1}{2}\right)}\right) \]

      5. +-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\color{blue}{\left(x + \left(x + \varepsilon\right)\right)} \cdot \frac{1}{2}\right)\right) \]

      6. metadata-eval84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot \color{blue}{0.5}\right)\right) \]

    3. Applied egg-rr84.0%

      \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right)} \]
    4. Step-by-step derivation

      1. *-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \color{blue}{\left(0.5 \cdot \left(\left(x + \varepsilon\right) - x\right)\right)} \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

      2. +-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\color{blue}{\left(\varepsilon + x\right)} - x\right)\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

      3. associate--l+83.8%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \color{blue}{\left(\varepsilon + \left(x - x\right)\right)}\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

      4. *-commutative83.8%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \color{blue}{\left(0.5 \cdot \left(x + \left(x + \varepsilon\right)\right)\right)}\right) \]

      5. associate-+r+84.0%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \color{blue}{\left(\left(x + x\right) + \varepsilon\right)}\right)\right) \]

      6. +-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \color{blue}{\left(\varepsilon + \left(x + x\right)\right)}\right)\right) \]

    5. Simplified84.0%

      \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \left(\varepsilon + \left(x + x\right)\right)\right)\right)} \]

    6. Taylor expanded in x around 0 83.5%

      \[\leadsto -2 \cdot \color{blue}{{\sin \left(0.5 \cdot \varepsilon\right)}^{2}} \]

    if -4.9999999999999998e-8 < (-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))

    1. Initial program 15.6%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 74.2%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg74.2%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg74.2%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow274.2%

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

      4. associate-*l*74.2%

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

    4. Simplified74.2%

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

    5. Taylor expanded in eps around 0 74.2%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    6. Step-by-step derivation

      1. fma-def74.2%

        \[\leadsto \color{blue}{\mathsf{fma}\left(-0.5, {\varepsilon}^{2} \cdot \cos x, -1 \cdot \left(\varepsilon \cdot \sin x\right)\right)} \]

      2. unpow274.2%

        \[\leadsto \mathsf{fma}\left(-0.5, \color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot \cos x, -1 \cdot \left(\varepsilon \cdot \sin x\right)\right) \]

      3. associate-*r*74.2%

        \[\leadsto \mathsf{fma}\left(-0.5, \color{blue}{\varepsilon \cdot \left(\varepsilon \cdot \cos x\right)}, -1 \cdot \left(\varepsilon \cdot \sin x\right)\right) \]

      4. neg-mul-174.2%

        \[\leadsto \mathsf{fma}\left(-0.5, \varepsilon \cdot \left(\varepsilon \cdot \cos x\right), \color{blue}{-\varepsilon \cdot \sin x}\right) \]

      5. fma-neg74.2%

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

      6. *-commutative74.2%

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

      7. associate-*l*74.2%

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

      8. distribute-lft-out--74.1%

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

      9. *-commutative74.1%

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

      10. associate-*l*74.1%

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

    7. Simplified74.1%

      \[\leadsto \color{blue}{\varepsilon \cdot \left(\cos x \cdot \left(\varepsilon \cdot -0.5\right) - \sin x\right)} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification77.2%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(\varepsilon + x\right) - \cos x \leq -5 \cdot 10^{-8}:\\ \;\;\;\;-2 \cdot {\sin \left(\varepsilon \cdot 0.5\right)}^{2}\\ \mathbf{else}:\\ \;\;\;\;\varepsilon \cdot \left(\cos x \cdot \left(\varepsilon \cdot -0.5\right) - \sin x\right)\\ \end{array} \]

Alternative 8?

\[\begin{array}{l} \mathbf{if}\;\cos \left(\varepsilon + x\right) - \cos x \leq -5 \cdot 10^{-8}:\\ \;\;\;\;-2 \cdot {\sin \left(\varepsilon \cdot 0.5\right)}^{2}\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) - \varepsilon \cdot \sin x\\ \end{array} \]
Derivation
  1. Split input into 2 regimes

  2. if (-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x)) < -4.9999999999999998e-8

    1. Initial program 83.0%

      \[\cos \left(x + \varepsilon\right) - \cos x \]
    2. Step-by-step derivation

      1. diff-cos84.0%

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

      2. div-inv84.0%

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

      3. metadata-eval84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot \color{blue}{0.5}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \]

      4. div-inv84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \color{blue}{\left(\left(\left(x + \varepsilon\right) + x\right) \cdot \frac{1}{2}\right)}\right) \]

      5. +-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\color{blue}{\left(x + \left(x + \varepsilon\right)\right)} \cdot \frac{1}{2}\right)\right) \]

      6. metadata-eval84.0%

        \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot \color{blue}{0.5}\right)\right) \]

    3. Applied egg-rr84.0%

      \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right)} \]
    4. Step-by-step derivation

      1. *-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \color{blue}{\left(0.5 \cdot \left(\left(x + \varepsilon\right) - x\right)\right)} \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

      2. +-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\color{blue}{\left(\varepsilon + x\right)} - x\right)\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

      3. associate--l+83.8%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \color{blue}{\left(\varepsilon + \left(x - x\right)\right)}\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

      4. *-commutative83.8%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \color{blue}{\left(0.5 \cdot \left(x + \left(x + \varepsilon\right)\right)\right)}\right) \]

      5. associate-+r+84.0%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \color{blue}{\left(\left(x + x\right) + \varepsilon\right)}\right)\right) \]

      6. +-commutative84.0%

        \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \color{blue}{\left(\varepsilon + \left(x + x\right)\right)}\right)\right) \]

    5. Simplified84.0%

      \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \left(\varepsilon + \left(x + x\right)\right)\right)\right)} \]

    6. Taylor expanded in x around 0 83.5%

      \[\leadsto -2 \cdot \color{blue}{{\sin \left(0.5 \cdot \varepsilon\right)}^{2}} \]

    if -4.9999999999999998e-8 < (-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))

    1. Initial program 15.6%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 74.2%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg74.2%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg74.2%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow274.2%

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

      4. associate-*l*74.2%

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

    4. Simplified74.2%

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

    5. Taylor expanded in x around 0 73.3%

      \[\leadsto -0.5 \cdot \left(\varepsilon \cdot \color{blue}{\varepsilon}\right) - \varepsilon \cdot \sin x \]
  3. Recombined 2 regimes into one program.

  4. Final simplification76.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(\varepsilon + x\right) - \cos x \leq -5 \cdot 10^{-8}:\\ \;\;\;\;-2 \cdot {\sin \left(\varepsilon \cdot 0.5\right)}^{2}\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) - \varepsilon \cdot \sin x\\ \end{array} \]

Alternative 9?

\[\begin{array}{l} t_0 := \cos \left(\varepsilon + x\right) - \cos x\\ \mathbf{if}\;t_0 \leq -5 \cdot 10^{-8}:\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) - \varepsilon \cdot \sin x\\ \end{array} \]
Derivation
  1. Split input into 2 regimes

  2. if (-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x)) < -4.9999999999999998e-8

    1. Initial program 83.0%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    if -4.9999999999999998e-8 < (-.f64 (cos.f64 (+.f64 x eps)) (cos.f64 x))

    1. Initial program 15.6%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 74.2%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg74.2%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg74.2%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow274.2%

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

      4. associate-*l*74.2%

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

    4. Simplified74.2%

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

    5. Taylor expanded in x around 0 73.3%

      \[\leadsto -0.5 \cdot \left(\varepsilon \cdot \color{blue}{\varepsilon}\right) - \varepsilon \cdot \sin x \]
  3. Recombined 2 regimes into one program.

  4. Final simplification76.6%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\cos \left(\varepsilon + x\right) - \cos x \leq -5 \cdot 10^{-8}:\\ \;\;\;\;\cos \left(\varepsilon + x\right) - \cos x\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) - \varepsilon \cdot \sin x\\ \end{array} \]

Alternative 10?

\[-2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon - x \cdot -2\right)\right) \cdot \sin \left(\varepsilon \cdot 0.5\right)\right) \]
Derivation

  1. Initial program 38.0%

    \[\cos \left(x + \varepsilon\right) - \cos x \]
  2. Step-by-step derivation

    1. diff-cos47.7%

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

    2. div-inv47.7%

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

    3. metadata-eval47.7%

      \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot \color{blue}{0.5}\right) \cdot \sin \left(\frac{\left(x + \varepsilon\right) + x}{2}\right)\right) \]

    4. div-inv47.7%

      \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \color{blue}{\left(\left(\left(x + \varepsilon\right) + x\right) \cdot \frac{1}{2}\right)}\right) \]

    5. +-commutative47.7%

      \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\color{blue}{\left(x + \left(x + \varepsilon\right)\right)} \cdot \frac{1}{2}\right)\right) \]

    6. metadata-eval47.7%

      \[\leadsto -2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot \color{blue}{0.5}\right)\right) \]

  3. Applied egg-rr47.7%

    \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(\left(\left(x + \varepsilon\right) - x\right) \cdot 0.5\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right)} \]
  4. Step-by-step derivation

    1. *-commutative47.7%

      \[\leadsto -2 \cdot \left(\sin \color{blue}{\left(0.5 \cdot \left(\left(x + \varepsilon\right) - x\right)\right)} \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

    2. +-commutative47.7%

      \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\color{blue}{\left(\varepsilon + x\right)} - x\right)\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

    3. associate--l+78.0%

      \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \color{blue}{\left(\varepsilon + \left(x - x\right)\right)}\right) \cdot \sin \left(\left(x + \left(x + \varepsilon\right)\right) \cdot 0.5\right)\right) \]

    4. *-commutative78.0%

      \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \color{blue}{\left(0.5 \cdot \left(x + \left(x + \varepsilon\right)\right)\right)}\right) \]

    5. associate-+r+78.1%

      \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \color{blue}{\left(\left(x + x\right) + \varepsilon\right)}\right)\right) \]

    6. +-commutative78.1%

      \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \color{blue}{\left(\varepsilon + \left(x + x\right)\right)}\right)\right) \]

  5. Simplified78.1%

    \[\leadsto \color{blue}{-2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon + \left(x - x\right)\right)\right) \cdot \sin \left(0.5 \cdot \left(\varepsilon + \left(x + x\right)\right)\right)\right)} \]

  6. Taylor expanded in x around -inf 78.1%

    \[\leadsto -2 \cdot \color{blue}{\left(\sin \left(0.5 \cdot \left(\varepsilon - -2 \cdot x\right)\right) \cdot \sin \left(0.5 \cdot \varepsilon\right)\right)} \]

  7. Final simplification78.1%

    \[\leadsto -2 \cdot \left(\sin \left(0.5 \cdot \left(\varepsilon - x \cdot -2\right)\right) \cdot \sin \left(\varepsilon \cdot 0.5\right)\right) \]

Alternative 11?

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.0014:\\ \;\;\;\;\cos \varepsilon - \cos x\\ \mathbf{elif}\;\varepsilon \leq 0.00325:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) - \varepsilon \cdot \sin x\\ \mathbf{else}:\\ \;\;\;\;\cos \varepsilon + -1\\ \end{array} \]
Derivation
  1. Split input into 3 regimes

  2. if eps < -0.00139999999999999999

    1. Initial program 53.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 55.5%

      \[\leadsto \color{blue}{\cos \varepsilon} - \cos x \]

    if -0.00139999999999999999 < eps < 0.00324999999999999985

    1. Initial program 20.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 99.2%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg99.2%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg99.2%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow299.2%

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

      4. associate-*l*99.2%

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

    4. Simplified99.2%

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

    5. Taylor expanded in x around 0 98.5%

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

    if 0.00324999999999999985 < eps

    1. Initial program 56.8%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 59.0%

      \[\leadsto \color{blue}{\cos \varepsilon - 1} \]
  3. Recombined 3 regimes into one program.

  4. Final simplification77.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.0014:\\ \;\;\;\;\cos \varepsilon - \cos x\\ \mathbf{elif}\;\varepsilon \leq 0.00325:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) - \varepsilon \cdot \sin x\\ \mathbf{else}:\\ \;\;\;\;\cos \varepsilon + -1\\ \end{array} \]

Alternative 12?

\[\begin{array}{l} t_0 := \cos \varepsilon + -1\\ \mathbf{if}\;\varepsilon \leq -2.5 \cdot 10^{-6}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;\varepsilon \leq 4.4 \cdot 10^{-95}:\\ \;\;\;\;\varepsilon \cdot \left(-\sin x\right)\\ \mathbf{elif}\;\varepsilon \leq 0.00122:\\ \;\;\;\;\mathsf{fma}\left(-\varepsilon, x, \varepsilon \cdot \left(\varepsilon \cdot -0.5\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Derivation
  1. Split input into 3 regimes

  2. if eps < -2.5000000000000002e-6 or 0.00121999999999999995 < eps

    1. Initial program 55.2%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 57.2%

      \[\leadsto \color{blue}{\cos \varepsilon - 1} \]

    if -2.5000000000000002e-6 < eps < 4.3999999999999998e-95

    1. Initial program 23.8%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 88.2%

      \[\leadsto \color{blue}{-1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. associate-*r*88.2%

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

      2. mul-1-neg88.2%

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

    4. Simplified88.2%

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

    if 4.3999999999999998e-95 < eps < 0.00121999999999999995

    1. Initial program 8.7%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 96.8%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg96.8%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg96.8%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow296.8%

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

      4. associate-*l*96.8%

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

    4. Simplified96.8%

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

    5. Taylor expanded in x around 0 69.0%

      \[\leadsto \color{blue}{-1 \cdot \left(\varepsilon \cdot x\right) + -0.5 \cdot {\varepsilon}^{2}} \]
    6. Step-by-step derivation

      1. associate-*r*69.0%

        \[\leadsto \color{blue}{\left(-1 \cdot \varepsilon\right) \cdot x} + -0.5 \cdot {\varepsilon}^{2} \]

      2. fma-def69.0%

        \[\leadsto \color{blue}{\mathsf{fma}\left(-1 \cdot \varepsilon, x, -0.5 \cdot {\varepsilon}^{2}\right)} \]

      3. neg-mul-169.0%

        \[\leadsto \mathsf{fma}\left(\color{blue}{-\varepsilon}, x, -0.5 \cdot {\varepsilon}^{2}\right) \]

      4. *-commutative69.0%

        \[\leadsto \mathsf{fma}\left(-\varepsilon, x, \color{blue}{{\varepsilon}^{2} \cdot -0.5}\right) \]

      5. unpow269.0%

        \[\leadsto \mathsf{fma}\left(-\varepsilon, x, \color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot -0.5\right) \]

      6. associate-*l*69.0%

        \[\leadsto \mathsf{fma}\left(-\varepsilon, x, \color{blue}{\varepsilon \cdot \left(\varepsilon \cdot -0.5\right)}\right) \]

    7. Simplified69.0%

      \[\leadsto \color{blue}{\mathsf{fma}\left(-\varepsilon, x, \varepsilon \cdot \left(\varepsilon \cdot -0.5\right)\right)} \]
  3. Recombined 3 regimes into one program.

  4. Final simplification70.4%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -2.5 \cdot 10^{-6}:\\ \;\;\;\;\cos \varepsilon + -1\\ \mathbf{elif}\;\varepsilon \leq 4.4 \cdot 10^{-95}:\\ \;\;\;\;\varepsilon \cdot \left(-\sin x\right)\\ \mathbf{elif}\;\varepsilon \leq 0.00122:\\ \;\;\;\;\mathsf{fma}\left(-\varepsilon, x, \varepsilon \cdot \left(\varepsilon \cdot -0.5\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\cos \varepsilon + -1\\ \end{array} \]

Alternative 13?

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.00155 \lor \neg \left(\varepsilon \leq 0.0047\right):\\ \;\;\;\;\cos \varepsilon + -1\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) - \varepsilon \cdot \sin x\\ \end{array} \]
Derivation
  1. Split input into 2 regimes

  2. if eps < -0.00154999999999999995 or 0.00470000000000000018 < eps

    1. Initial program 55.2%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 57.2%

      \[\leadsto \color{blue}{\cos \varepsilon - 1} \]

    if -0.00154999999999999995 < eps < 0.00470000000000000018

    1. Initial program 20.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 99.2%

      \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + -1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. mul-1-neg99.2%

        \[\leadsto -0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) + \color{blue}{\left(-\varepsilon \cdot \sin x\right)} \]

      2. unsub-neg99.2%

        \[\leadsto \color{blue}{-0.5 \cdot \left({\varepsilon}^{2} \cdot \cos x\right) - \varepsilon \cdot \sin x} \]

      3. unpow299.2%

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

      4. associate-*l*99.2%

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

    4. Simplified99.2%

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

    5. Taylor expanded in x around 0 98.5%

      \[\leadsto -0.5 \cdot \left(\varepsilon \cdot \color{blue}{\varepsilon}\right) - \varepsilon \cdot \sin x \]
  3. Recombined 2 regimes into one program.

  4. Final simplification77.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.00155 \lor \neg \left(\varepsilon \leq 0.0047\right):\\ \;\;\;\;\cos \varepsilon + -1\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) - \varepsilon \cdot \sin x\\ \end{array} \]

Alternative 14?

\[\begin{array}{l} t_0 := \cos \varepsilon + -1\\ t_1 := -0.5 \cdot \left(\varepsilon \cdot \varepsilon\right)\\ \mathbf{if}\;\varepsilon \leq -0.00014:\\ \;\;\;\;t_0\\ \mathbf{elif}\;\varepsilon \leq -5.6 \cdot 10^{-139}:\\ \;\;\;\;t_1\\ \mathbf{elif}\;\varepsilon \leq 3.2 \cdot 10^{-138}:\\ \;\;\;\;\sin \varepsilon \cdot \left(-x\right)\\ \mathbf{elif}\;\varepsilon \leq 0.00018:\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Derivation
  1. Split input into 3 regimes

  2. if eps < -1.3999999999999999e-4 or 1.80000000000000011e-4 < eps

    1. Initial program 55.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 57.1%

      \[\leadsto \color{blue}{\cos \varepsilon - 1} \]

    if -1.3999999999999999e-4 < eps < -5.5999999999999997e-139 or 3.2000000000000001e-138 < eps < 1.80000000000000011e-4

    1. Initial program 4.1%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 4.1%

      \[\leadsto \color{blue}{\cos \varepsilon - 1} \]

    3. Taylor expanded in eps around 0 44.3%

      \[\leadsto \color{blue}{-0.5 \cdot {\varepsilon}^{2}} \]
    4. Step-by-step derivation

      1. *-commutative44.3%

        \[\leadsto \color{blue}{{\varepsilon}^{2} \cdot -0.5} \]

      2. unpow244.3%

        \[\leadsto \color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot -0.5 \]

    5. Simplified44.3%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot \varepsilon\right) \cdot -0.5} \]

    if -5.5999999999999997e-139 < eps < 3.2000000000000001e-138

    1. Initial program 32.3%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 30.5%

      \[\leadsto \color{blue}{\left(\cos \varepsilon + -1 \cdot \left(x \cdot \sin \varepsilon\right)\right)} - \cos x \]
    3. Step-by-step derivation

      1. mul-1-neg30.5%

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

      2. unsub-neg30.5%

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

    4. Simplified30.5%

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

    5. Taylor expanded in x around inf 50.6%

      \[\leadsto \color{blue}{-1 \cdot \left(x \cdot \sin \varepsilon\right)} \]
    6. Step-by-step derivation

      1. neg-mul-150.6%

        \[\leadsto \color{blue}{-x \cdot \sin \varepsilon} \]

      2. distribute-rgt-neg-in50.6%

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

    7. Simplified50.6%

      \[\leadsto \color{blue}{x \cdot \left(-\sin \varepsilon\right)} \]
  3. Recombined 3 regimes into one program.

  4. Final simplification52.5%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.00014:\\ \;\;\;\;\cos \varepsilon + -1\\ \mathbf{elif}\;\varepsilon \leq -5.6 \cdot 10^{-139}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right)\\ \mathbf{elif}\;\varepsilon \leq 3.2 \cdot 10^{-138}:\\ \;\;\;\;\sin \varepsilon \cdot \left(-x\right)\\ \mathbf{elif}\;\varepsilon \leq 0.00018:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\cos \varepsilon + -1\\ \end{array} \]

Alternative 15?

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -1.35 \cdot 10^{-7} \lor \neg \left(\varepsilon \leq 6.5 \cdot 10^{-7}\right):\\ \;\;\;\;\cos \varepsilon + -1\\ \mathbf{else}:\\ \;\;\;\;\varepsilon \cdot \left(-\sin x\right)\\ \end{array} \]
Derivation
  1. Split input into 2 regimes

  2. if eps < -1.35000000000000004e-7 or 6.50000000000000024e-7 < eps

    1. Initial program 55.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 57.1%

      \[\leadsto \color{blue}{\cos \varepsilon - 1} \]

    if -1.35000000000000004e-7 < eps < 6.50000000000000024e-7

    1. Initial program 19.7%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in eps around 0 80.3%

      \[\leadsto \color{blue}{-1 \cdot \left(\varepsilon \cdot \sin x\right)} \]
    3. Step-by-step derivation

      1. associate-*r*80.3%

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

      2. mul-1-neg80.3%

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

    4. Simplified80.3%

      \[\leadsto \color{blue}{\left(-\varepsilon\right) \cdot \sin x} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification68.4%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -1.35 \cdot 10^{-7} \lor \neg \left(\varepsilon \leq 6.5 \cdot 10^{-7}\right):\\ \;\;\;\;\cos \varepsilon + -1\\ \mathbf{else}:\\ \;\;\;\;\varepsilon \cdot \left(-\sin x\right)\\ \end{array} \]

Alternative 16?

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.00014 \lor \neg \left(\varepsilon \leq 0.00018\right):\\ \;\;\;\;\cos \varepsilon + -1\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right)\\ \end{array} \]
Derivation
  1. Split input into 2 regimes

  2. if eps < -1.3999999999999999e-4 or 1.80000000000000011e-4 < eps

    1. Initial program 55.5%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 57.1%

      \[\leadsto \color{blue}{\cos \varepsilon - 1} \]

    if -1.3999999999999999e-4 < eps < 1.80000000000000011e-4

    1. Initial program 19.7%

      \[\cos \left(x + \varepsilon\right) - \cos x \]

    2. Taylor expanded in x around 0 19.7%

      \[\leadsto \color{blue}{\cos \varepsilon - 1} \]

    3. Taylor expanded in eps around 0 38.4%

      \[\leadsto \color{blue}{-0.5 \cdot {\varepsilon}^{2}} \]
    4. Step-by-step derivation

      1. *-commutative38.4%

        \[\leadsto \color{blue}{{\varepsilon}^{2} \cdot -0.5} \]

      2. unpow238.4%

        \[\leadsto \color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot -0.5 \]

    5. Simplified38.4%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot \varepsilon\right) \cdot -0.5} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification47.9%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -0.00014 \lor \neg \left(\varepsilon \leq 0.00018\right):\\ \;\;\;\;\cos \varepsilon + -1\\ \mathbf{else}:\\ \;\;\;\;-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right)\\ \end{array} \]

Alternative 17?

\[-0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) \]
Derivation

  1. Initial program 38.0%

    \[\cos \left(x + \varepsilon\right) - \cos x \]

  2. Taylor expanded in x around 0 38.8%

    \[\leadsto \color{blue}{\cos \varepsilon - 1} \]

  3. Taylor expanded in eps around 0 21.0%

    \[\leadsto \color{blue}{-0.5 \cdot {\varepsilon}^{2}} \]
  4. Step-by-step derivation

    1. *-commutative21.0%

      \[\leadsto \color{blue}{{\varepsilon}^{2} \cdot -0.5} \]

    2. unpow221.0%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot -0.5 \]

  5. Simplified21.0%

    \[\leadsto \color{blue}{\left(\varepsilon \cdot \varepsilon\right) \cdot -0.5} \]

  6. Final simplification21.0%

    \[\leadsto -0.5 \cdot \left(\varepsilon \cdot \varepsilon\right) \]

Reproduce

?
herbie shell --seed 2023166 
(FPCore (x eps)
  :name "2cos (problem 3.3.5)"
  :precision binary64
  (- (cos (+ x eps)) (cos x)))