Average Error: 37.2 → 0.4
Time: 8.9s
Precision: 64
\[\sin \left(x + \varepsilon\right) - \sin x\]
↓
\[\begin{array}{l} \mathbf{if}\;\varepsilon \le -0.03050652900604648373739102851232019020244:\\ \;\;\;\;\frac{\left(\sin x \cdot \left(\cos \varepsilon - 1\right) + \cos x \cdot \sin \varepsilon\right) \cdot \left(\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x\right)}{\sin x \cdot \left(\cos \varepsilon + 1\right) + \cos x \cdot \sin \varepsilon}\\ \mathbf{elif}\;\varepsilon \le 0.03268722773714166640601774815877433866262:\\ \;\;\;\;1 \cdot \left(\sin x \cdot \left(\frac{1}{24} \cdot {\varepsilon}^{4} - \left(\frac{1}{2} \cdot {\varepsilon}^{2} + \frac{1}{720} \cdot {\varepsilon}^{6}\right)\right) + \cos x \cdot \sin \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}^{3} - {\left(\sin x\right)}^{3}}{\left(\sin \varepsilon \cdot \cos x + \sin x \cdot \cos \varepsilon\right) \cdot \left(\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x\right) + \sin x \cdot \sin x}\\ \end{array}\]
\sin \left(x + \varepsilon\right) - \sin x
↓
\begin{array}{l}
\mathbf{if}\;\varepsilon \le -0.03050652900604648373739102851232019020244:\\
\;\;\;\;\frac{\left(\sin x \cdot \left(\cos \varepsilon - 1\right) + \cos x \cdot \sin \varepsilon\right) \cdot \left(\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x\right)}{\sin x \cdot \left(\cos \varepsilon + 1\right) + \cos x \cdot \sin \varepsilon}\\

\mathbf{elif}\;\varepsilon \le 0.03268722773714166640601774815877433866262:\\
\;\;\;\;1 \cdot \left(\sin x \cdot \left(\frac{1}{24} \cdot {\varepsilon}^{4} - \left(\frac{1}{2} \cdot {\varepsilon}^{2} + \frac{1}{720} \cdot {\varepsilon}^{6}\right)\right) + \cos x \cdot \sin \varepsilon\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}^{3} - {\left(\sin x\right)}^{3}}{\left(\sin \varepsilon \cdot \cos x + \sin x \cdot \cos \varepsilon\right) \cdot \left(\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x\right) + \sin x \cdot \sin x}\\

\end{array}
double f(double x, double eps) {
        double r158192 = x;
        double r158193 = eps;
        double r158194 = r158192 + r158193;
        double r158195 = sin(r158194);
        double r158196 = sin(r158192);
        double r158197 = r158195 - r158196;
        return r158197;
}
↓
double f(double x, double eps) {
        double r158198 = eps;
        double r158199 = -0.030506529006046484;
        bool r158200 = r158198 <= r158199;
        double r158201 = x;
        double r158202 = sin(r158201);
        double r158203 = cos(r158198);
        double r158204 = 1.0;
        double r158205 = r158203 - r158204;
        double r158206 = r158202 * r158205;
        double r158207 = cos(r158201);
        double r158208 = sin(r158198);
        double r158209 = r158207 * r158208;
        double r158210 = r158206 + r158209;
        double r158211 = r158202 * r158203;
        double r158212 = r158211 + r158209;
        double r158213 = r158212 + r158202;
        double r158214 = r158210 * r158213;
        double r158215 = r158203 + r158204;
        double r158216 = r158202 * r158215;
        double r158217 = r158216 + r158209;
        double r158218 = r158214 / r158217;
        double r158219 = 0.032687227737141666;
        bool r158220 = r158198 <= r158219;
        double r158221 = 0.041666666666666664;
        double r158222 = 4.0;
        double r158223 = pow(r158198, r158222);
        double r158224 = r158221 * r158223;
        double r158225 = 0.5;
        double r158226 = 2.0;
        double r158227 = pow(r158198, r158226);
        double r158228 = r158225 * r158227;
        double r158229 = 0.001388888888888889;
        double r158230 = 6.0;
        double r158231 = pow(r158198, r158230);
        double r158232 = r158229 * r158231;
        double r158233 = r158228 + r158232;
        double r158234 = r158224 - r158233;
        double r158235 = r158202 * r158234;
        double r158236 = r158235 + r158209;
        double r158237 = r158204 * r158236;
        double r158238 = 3.0;
        double r158239 = pow(r158212, r158238);
        double r158240 = pow(r158202, r158238);
        double r158241 = r158239 - r158240;
        double r158242 = r158208 * r158207;
        double r158243 = r158242 + r158211;
        double r158244 = r158243 * r158213;
        double r158245 = r158202 * r158202;
        double r158246 = r158244 + r158245;
        double r158247 = r158241 / r158246;
        double r158248 = r158220 ? r158237 : r158247;
        double r158249 = r158200 ? r158218 : r158248;
        return r158249;
}

Error

Bits error versus x

Bits error versus eps

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original37.2
Target15.0
Herbie0.4
\[2 \cdot \left(\cos \left(x + \frac{\varepsilon}{2}\right) \cdot \sin \left(\frac{\varepsilon}{2}\right)\right)\]

Derivation

  1. Split input into 3 regimes

  2. if eps < -0.030506529006046484

    1. Initial program 29.6

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

    3. Applied sin-sum0.4

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

    5. Applied flip--0.6

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

    6. Simplified0.5

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

    7. Simplified0.7

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

    if -0.030506529006046484 < eps < 0.032687227737141666

    1. Initial program 44.7

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

    3. Applied sin-sum44.0

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

    5. Applied *-un-lft-identity44.0

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

    6. Applied *-un-lft-identity44.0

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

    7. Applied distribute-lft-out--44.0

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

    8. Simplified0.3

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

    9. Taylor expanded around 0 0.1

      \[\leadsto 1 \cdot \left(\sin x \cdot \color{blue}{\left(\frac{1}{24} \cdot {\varepsilon}^{4} - \left(\frac{1}{2} \cdot {\varepsilon}^{2} + \frac{1}{720} \cdot {\varepsilon}^{6}\right)\right)} + \cos x \cdot \sin \varepsilon\right)\]

    if 0.032687227737141666 < eps

    1. Initial program 30.0

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

    3. Applied sin-sum0.4

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

    5. Applied flip3--0.6

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

    6. Simplified0.6

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

  4. Final simplification0.4

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \le -0.03050652900604648373739102851232019020244:\\ \;\;\;\;\frac{\left(\sin x \cdot \left(\cos \varepsilon - 1\right) + \cos x \cdot \sin \varepsilon\right) \cdot \left(\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x\right)}{\sin x \cdot \left(\cos \varepsilon + 1\right) + \cos x \cdot \sin \varepsilon}\\ \mathbf{elif}\;\varepsilon \le 0.03268722773714166640601774815877433866262:\\ \;\;\;\;1 \cdot \left(\sin x \cdot \left(\frac{1}{24} \cdot {\varepsilon}^{4} - \left(\frac{1}{2} \cdot {\varepsilon}^{2} + \frac{1}{720} \cdot {\varepsilon}^{6}\right)\right) + \cos x \cdot \sin \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right)}^{3} - {\left(\sin x\right)}^{3}}{\left(\sin \varepsilon \cdot \cos x + \sin x \cdot \cos \varepsilon\right) \cdot \left(\left(\sin x \cdot \cos \varepsilon + \cos x \cdot \sin \varepsilon\right) + \sin x\right) + \sin x \cdot \sin x}\\ \end{array}\]

Reproduce

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

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

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