\[\frac{1 - \cos x}{\sin x}\]

↓

\[\begin{array}{l} \mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -9.955579397094595477807343897325154102873 \cdot 10^{-4}:\\ \;\;\;\;\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \left(\cos x + 1\right) + 1 \cdot 1\right) \cdot \sin x}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le 6.585706534220822007288757837795145633208 \cdot 10^{-6}:\\ \;\;\;\;\left(\frac{1}{24} \cdot {x}^{3} + \frac{1}{240} \cdot {x}^{5}\right) + \frac{1}{2} \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sin x} \cdot \left(1 - \cos x\right)\\ \end{array}\]

\frac{1 - \cos x}{\sin x}

↓

\begin{array}{l}
\mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -9.955579397094595477807343897325154102873 \cdot 10^{-4}:\\
\;\;\;\;\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \left(\cos x + 1\right) + 1 \cdot 1\right) \cdot \sin x}\\

\mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le 6.585706534220822007288757837795145633208 \cdot 10^{-6}:\\
\;\;\;\;\left(\frac{1}{24} \cdot {x}^{3} + \frac{1}{240} \cdot {x}^{5}\right) + \frac{1}{2} \cdot x\\

\mathbf{else}:\\
\;\;\;\;\frac{1}{\sin x} \cdot \left(1 - \cos x\right)\\

\end{array}

double f(double x) {
        double r161567 = 1.0;
        double r161568 = x;
        double r161569 = cos(r161568);
        double r161570 = r161567 - r161569;
        double r161571 = sin(r161568);
        double r161572 = r161570 / r161571;
        return r161572;
}

↓

double f(double x) {
        double r161573 = 1.0;
        double r161574 = x;
        double r161575 = cos(r161574);
        double r161576 = r161573 - r161575;
        double r161577 = sin(r161574);
        double r161578 = r161576 / r161577;
        double r161579 = -0.0009955579397094595;
        bool r161580 = r161578 <= r161579;
        double r161581 = 3.0;
        double r161582 = pow(r161573, r161581);
        double r161583 = pow(r161575, r161581);
        double r161584 = r161582 - r161583;
        double r161585 = r161575 + r161573;
        double r161586 = r161575 * r161585;
        double r161587 = r161573 * r161573;
        double r161588 = r161586 + r161587;
        double r161589 = r161588 * r161577;
        double r161590 = r161584 / r161589;
        double r161591 = 6.585706534220822e-06;
        bool r161592 = r161578 <= r161591;
        double r161593 = 0.041666666666666664;
        double r161594 = pow(r161574, r161581);
        double r161595 = r161593 * r161594;
        double r161596 = 0.004166666666666667;
        double r161597 = 5.0;
        double r161598 = pow(r161574, r161597);
        double r161599 = r161596 * r161598;
        double r161600 = r161595 + r161599;
        double r161601 = 0.5;
        double r161602 = r161601 * r161574;
        double r161603 = r161600 + r161602;
        double r161604 = 1.0;
        double r161605 = r161604 / r161577;
        double r161606 = r161605 * r161576;
        double r161607 = r161592 ? r161603 : r161606;
        double r161608 = r161580 ? r161590 : r161607;
        return r161608;
}

Original	30.3
Target	0.0
Herbie	0.6

Derivation

Split input into 3 regimes
if (/ (- 1.0 (cos x)) (sin x)) < -0.0009955579397094595
1. Initial program 0.9
  \[\frac{1 - \cos x}{\sin x}\]
2. Using strategy rm
3. Applied flip3--1.0
  \[\leadsto \frac{\color{blue}{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)}}}{\sin x}\]
4. Applied associate-/l/1.0
  \[\leadsto \color{blue}{\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\sin x \cdot \left(1 \cdot 1 + \left(\cos x \cdot \cos x + 1 \cdot \cos x\right)\right)}}\]
5. Simplified1.0
  \[\leadsto \frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\color{blue}{\left(\cos x \cdot \left(\cos x + 1\right) + 1 \cdot 1\right) \cdot \sin x}}\]
if -0.0009955579397094595 < (/ (- 1.0 (cos x)) (sin x)) < 6.585706534220822e-06
1. Initial program 60.3
  \[\frac{1 - \cos x}{\sin x}\]
2. Taylor expanded around 0 0.0
  \[\leadsto \color{blue}{\frac{1}{24} \cdot {x}^{3} + \left(\frac{1}{240} \cdot {x}^{5} + \frac{1}{2} \cdot x\right)}\]
3. Using strategy rm
4. Applied associate-+r+0.0
  \[\leadsto \color{blue}{\left(\frac{1}{24} \cdot {x}^{3} + \frac{1}{240} \cdot {x}^{5}\right) + \frac{1}{2} \cdot x}\]
if 6.585706534220822e-06 < (/ (- 1.0 (cos x)) (sin x))
1. Initial program 1.2
  \[\frac{1 - \cos x}{\sin x}\]
2. Using strategy rm
3. Applied clear-num1.2
  \[\leadsto \color{blue}{\frac{1}{\frac{\sin x}{1 - \cos x}}}\]
4. Using strategy rm
5. Applied div-inv1.3
  \[\leadsto \frac{1}{\color{blue}{\sin x \cdot \frac{1}{1 - \cos x}}}\]
6. Applied add-cube-cbrt1.3
  \[\leadsto \frac{\color{blue}{\left(\sqrt[3]{1} \cdot \sqrt[3]{1}\right) \cdot \sqrt[3]{1}}}{\sin x \cdot \frac{1}{1 - \cos x}}\]
7. Applied times-frac1.3
  \[\leadsto \color{blue}{\frac{\sqrt[3]{1} \cdot \sqrt[3]{1}}{\sin x} \cdot \frac{\sqrt[3]{1}}{\frac{1}{1 - \cos x}}}\]
8. Simplified1.3
  \[\leadsto \color{blue}{\frac{1}{\sin x}} \cdot \frac{\sqrt[3]{1}}{\frac{1}{1 - \cos x}}\]
9. Simplified1.2
  \[\leadsto \frac{1}{\sin x} \cdot \color{blue}{\left(1 - \cos x\right)}\]
Recombined 3 regimes into one program.
Final simplification0.6
\[\leadsto \begin{array}{l} \mathbf{if}\;\frac{1 - \cos x}{\sin x} \le -9.955579397094595477807343897325154102873 \cdot 10^{-4}:\\ \;\;\;\;\frac{{1}^{3} - {\left(\cos x\right)}^{3}}{\left(\cos x \cdot \left(\cos x + 1\right) + 1 \cdot 1\right) \cdot \sin x}\\ \mathbf{elif}\;\frac{1 - \cos x}{\sin x} \le 6.585706534220822007288757837795145633208 \cdot 10^{-6}:\\ \;\;\;\;\left(\frac{1}{24} \cdot {x}^{3} + \frac{1}{240} \cdot {x}^{5}\right) + \frac{1}{2} \cdot x\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sin x} \cdot \left(1 - \cos x\right)\\ \end{array}\]

Error

Try it out

Target

Derivation

`if (/ (- 1.0 (cos x)) (sin x)) < -0.0009955579397094595`

`if -0.0009955579397094595 < (/ (- 1.0 (cos x)) (sin x)) < 6.585706534220822e-06`

`if 6.585706534220822e-06 < (/ (- 1.0 (cos x)) (sin x))`

Reproduce

In
Out