Average Error: 36.1 → 0.4
Time: 24.3s
Precision: 64
\[\sin \left(x + \varepsilon\right) - \sin x\]
↓
\[\frac{-\sin x \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{1 + \cos \varepsilon} + \cos x \cdot \sin \varepsilon\]
\sin \left(x + \varepsilon\right) - \sin x
↓
\frac{-\sin x \cdot \left(\sin \varepsilon \cdot \sin \varepsilon\right)}{1 + \cos \varepsilon} + \cos x \cdot \sin \varepsilon
double f(double x, double eps) {
        double r6405549 = x;
        double r6405550 = eps;
        double r6405551 = r6405549 + r6405550;
        double r6405552 = sin(r6405551);
        double r6405553 = sin(r6405549);
        double r6405554 = r6405552 - r6405553;
        return r6405554;
}
↓
double f(double x, double eps) {
        double r6405555 = x;
        double r6405556 = sin(r6405555);
        double r6405557 = eps;
        double r6405558 = sin(r6405557);
        double r6405559 = r6405558 * r6405558;
        double r6405560 = r6405556 * r6405559;
        double r6405561 = -r6405560;
        double r6405562 = 1.0;
        double r6405563 = cos(r6405557);
        double r6405564 = r6405562 + r6405563;
        double r6405565 = r6405561 / r6405564;
        double r6405566 = cos(r6405555);
        double r6405567 = r6405566 * r6405558;
        double r6405568 = r6405565 + r6405567;
        return r6405568;
}

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original36.1
Target14.2
Herbie0.4
\[2 \cdot \left(\cos \left(x + \frac{\varepsilon}{2}\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right)\]

Derivation

  1. Initial program 36.1

    \[\sin \left(x + \varepsilon\right) - \sin x\]
  2. Using strategy rm

  3. Applied +-commutative36.1

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

  4. Applied sin-sum21.7

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

  5. Applied associate--l+0.4

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

  7. Applied add-log-exp14.5

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

  8. Applied add-log-exp0.5

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

  9. Applied diff-log0.5

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

  10. Simplified0.4

    \[\leadsto \sin \varepsilon \cdot \cos x + \log \color{blue}{\left(e^{\cos \varepsilon \cdot \sin x - \sin x}\right)}\]
  11. Using strategy rm

  12. Applied *-un-lft-identity0.4

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

  13. Applied distribute-rgt-out--0.4

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

  14. Applied exp-prod0.5

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

  15. Applied log-pow0.4

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

  16. Simplified0.4

    \[\leadsto \sin \varepsilon \cdot \cos x + \left(\cos \varepsilon - 1\right) \cdot \color{blue}{\sin x}\]
  17. Using strategy rm

  18. Applied flip--0.5

    \[\leadsto \sin \varepsilon \cdot \cos x + \color{blue}{\frac{\cos \varepsilon \cdot \cos \varepsilon - 1 \cdot 1}{\cos \varepsilon + 1}} \cdot \sin x\]

  19. Applied associate-*l/0.5

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

  20. Simplified0.4

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

  21. Final simplification0.4

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

Reproduce

herbie shell --seed 2019158 
(FPCore (x eps)
  :name "2sin (example 3.3)"

  :herbie-target
  (* 2 (* (cos (+ x (/ eps 2))) (sin (/ eps 2))))

  (- (sin (+ x eps)) (sin x)))