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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -0.01854364127689415303601450091264268849045:\\ \;\;\;\;{e}^{\left(\log \left(1 - \cos x\right)\right)} \cdot \frac{1}{\sin x}\\ \mathbf{elif}\;x \le 0.02331429387269752864786376278516399906948:\\ \;\;\;\;\frac{1}{24} \cdot {x}^{3} + \left(\frac{1}{240} \cdot {x}^{5} + \frac{1}{2} \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{1}^{\left(\log \left(1 - \cos x\right)\right)}}{\frac{\sin x}{1 - \cos x}}\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;x \le -0.01854364127689415303601450091264268849045:\\
\;\;\;\;{e}^{\left(\log \left(1 - \cos x\right)\right)} \cdot \frac{1}{\sin x}\\

\mathbf{elif}\;x \le 0.02331429387269752864786376278516399906948:\\
\;\;\;\;\frac{1}{24} \cdot {x}^{3} + \left(\frac{1}{240} \cdot {x}^{5} + \frac{1}{2} \cdot x\right)\\

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

\end{array}

double f(double x) {
        double r58123 = 1.0;
        double r58124 = x;
        double r58125 = cos(r58124);
        double r58126 = r58123 - r58125;
        double r58127 = sin(r58124);
        double r58128 = r58126 / r58127;
        return r58128;
}

↓

double f(double x) {
        double r58129 = x;
        double r58130 = -0.018543641276894153;
        bool r58131 = r58129 <= r58130;
        double r58132 = exp(1.0);
        double r58133 = 1.0;
        double r58134 = cos(r58129);
        double r58135 = r58133 - r58134;
        double r58136 = log(r58135);
        double r58137 = pow(r58132, r58136);
        double r58138 = 1.0;
        double r58139 = sin(r58129);
        double r58140 = r58138 / r58139;
        double r58141 = r58137 * r58140;
        double r58142 = 0.02331429387269753;
        bool r58143 = r58129 <= r58142;
        double r58144 = 0.041666666666666664;
        double r58145 = 3.0;
        double r58146 = pow(r58129, r58145);
        double r58147 = r58144 * r58146;
        double r58148 = 0.004166666666666667;
        double r58149 = 5.0;
        double r58150 = pow(r58129, r58149);
        double r58151 = r58148 * r58150;
        double r58152 = 0.5;
        double r58153 = r58152 * r58129;
        double r58154 = r58151 + r58153;
        double r58155 = r58147 + r58154;
        double r58156 = pow(r58138, r58136);
        double r58157 = r58139 / r58135;
        double r58158 = r58156 / r58157;
        double r58159 = r58143 ? r58155 : r58158;
        double r58160 = r58131 ? r58141 : r58159;
        return r58160;
}

Original	30.7
Target	0.0
Herbie	0.5

Derivation

Split input into 3 regimes
if x < -0.018543641276894153
1. Initial program 0.9
  \[\frac{1 - \cos x}{\sin x}\]
2. Using strategy rm
3. Applied add-exp-log0.9
  \[\leadsto \frac{\color{blue}{e^{\log \left(1 - \cos x\right)}}}{\sin x}\]
4. Using strategy rm
5. Applied pow10.9
  \[\leadsto \frac{e^{\log \color{blue}{\left({\left(1 - \cos x\right)}^{1}\right)}}}{\sin x}\]
6. Applied log-pow0.9
  \[\leadsto \frac{e^{\color{blue}{1 \cdot \log \left(1 - \cos x\right)}}}{\sin x}\]
7. Applied exp-prod1.0
  \[\leadsto \frac{\color{blue}{{\left(e^{1}\right)}^{\left(\log \left(1 - \cos x\right)\right)}}}{\sin x}\]
8. Simplified1.0
  \[\leadsto \frac{{\color{blue}{e}}^{\left(\log \left(1 - \cos x\right)\right)}}{\sin x}\]
9. Using strategy rm
10. Applied div-inv1.0
  \[\leadsto \color{blue}{{e}^{\left(\log \left(1 - \cos x\right)\right)} \cdot \frac{1}{\sin x}}\]
if -0.018543641276894153 < x < 0.02331429387269753
1. Initial program 59.9
  \[\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)}\]
if 0.02331429387269753 < x
1. Initial program 0.9
  \[\frac{1 - \cos x}{\sin x}\]
2. Using strategy rm
3. Applied add-exp-log0.9
  \[\leadsto \frac{\color{blue}{e^{\log \left(1 - \cos x\right)}}}{\sin x}\]
4. Using strategy rm
5. Applied pow10.9
  \[\leadsto \frac{e^{\log \color{blue}{\left({\left(1 - \cos x\right)}^{1}\right)}}}{\sin x}\]
6. Applied log-pow0.9
  \[\leadsto \frac{e^{\color{blue}{1 \cdot \log \left(1 - \cos x\right)}}}{\sin x}\]
7. Applied exp-prod1.0
  \[\leadsto \frac{\color{blue}{{\left(e^{1}\right)}^{\left(\log \left(1 - \cos x\right)\right)}}}{\sin x}\]
8. Simplified1.0
  \[\leadsto \frac{{\color{blue}{e}}^{\left(\log \left(1 - \cos x\right)\right)}}{\sin x}\]
9. Using strategy rm
10. Applied *-un-lft-identity1.0
  \[\leadsto \frac{{\color{blue}{\left(1 \cdot e\right)}}^{\left(\log \left(1 - \cos x\right)\right)}}{\sin x}\]
11. Applied unpow-prod-down1.0
  \[\leadsto \frac{\color{blue}{{1}^{\left(\log \left(1 - \cos x\right)\right)} \cdot {e}^{\left(\log \left(1 - \cos x\right)\right)}}}{\sin x}\]
12. Applied associate-/l*1.0
  \[\leadsto \color{blue}{\frac{{1}^{\left(\log \left(1 - \cos x\right)\right)}}{\frac{\sin x}{{e}^{\left(\log \left(1 - \cos x\right)\right)}}}}\]
13. Simplified1.0
  \[\leadsto \frac{{1}^{\left(\log \left(1 - \cos x\right)\right)}}{\color{blue}{\frac{\sin x}{1 - \cos x}}}\]
Recombined 3 regimes into one program.
Final simplification0.5
\[\leadsto \begin{array}{l} \mathbf{if}\;x \le -0.01854364127689415303601450091264268849045:\\ \;\;\;\;{e}^{\left(\log \left(1 - \cos x\right)\right)} \cdot \frac{1}{\sin x}\\ \mathbf{elif}\;x \le 0.02331429387269752864786376278516399906948:\\ \;\;\;\;\frac{1}{24} \cdot {x}^{3} + \left(\frac{1}{240} \cdot {x}^{5} + \frac{1}{2} \cdot x\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{{1}^{\left(\log \left(1 - \cos x\right)\right)}}{\frac{\sin x}{1 - \cos x}}\\ \end{array}\]

Error

Try it out

Target

Derivation

`if x < -0.018543641276894153`

`if -0.018543641276894153 < x < 0.02331429387269753`

`if 0.02331429387269753 < x`

Reproduce

In
Out