\[\frac{x0}{1 - x1} - x0\]

↓

\[\begin{array}{l} \mathbf{if}\;x1 \le 0.00021208908081054686:\\ \;\;\;\;{\left({e}^{\left(\sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)} \cdot \sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right)}\right)}^{\left(\sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right)}\\ \mathbf{else}:\\ \;\;\;\;(\left(\frac{\sqrt{x0}}{\sqrt{x1} + 1}\right) \cdot \left(\frac{\sqrt{x0}}{1 - \sqrt{x1}}\right) + \left(-x0\right))_*\\ \end{array}\]

double f(double x0, double x1) {
        double r41375608 = x0;
        double r41375609 = 1.0;
        double r41375610 = x1;
        double r41375611 = r41375609 - r41375610;
        double r41375612 = r41375608 / r41375611;
        double r41375613 = r41375612 - r41375608;
        return r41375613;
}

↓

double f(double x0, double x1) {
        double r41375614 = x1;
        double r41375615 = 0.00021208908081054686;
        bool r41375616 = r41375614 <= r41375615;
        double r41375617 = exp(1.0);
        double r41375618 = x0;
        double r41375619 = cbrt(r41375618);
        double r41375620 = r41375619 * r41375619;
        double r41375621 = 1.0;
        double r41375622 = r41375621 - r41375614;
        double r41375623 = r41375619 / r41375622;
        double r41375624 = -r41375618;
        double r41375625 = fma(r41375620, r41375623, r41375624);
        double r41375626 = log(r41375625);
        double r41375627 = cbrt(r41375626);
        double r41375628 = r41375627 * r41375627;
        double r41375629 = pow(r41375617, r41375628);
        double r41375630 = pow(r41375629, r41375627);
        double r41375631 = sqrt(r41375618);
        double r41375632 = sqrt(r41375614);
        double r41375633 = r41375632 + r41375621;
        double r41375634 = r41375631 / r41375633;
        double r41375635 = r41375621 - r41375632;
        double r41375636 = r41375631 / r41375635;
        double r41375637 = fma(r41375634, r41375636, r41375624);
        double r41375638 = r41375616 ? r41375630 : r41375637;
        return r41375638;
}

\frac{x0}{1 - x1} - x0

↓

\begin{array}{l}
\mathbf{if}\;x1 \le 0.00021208908081054686:\\
\;\;\;\;{\left({e}^{\left(\sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)} \cdot \sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right)}\right)}^{\left(\sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right)}\\

\mathbf{else}:\\
\;\;\;\;(\left(\frac{\sqrt{x0}}{\sqrt{x1} + 1}\right) \cdot \left(\frac{\sqrt{x0}}{1 - \sqrt{x1}}\right) + \left(-x0\right))_*\\

\end{array}

Original	7.8
Target	0.2
Herbie	6.0

Derivation

Split input into 2 regimes
if x1 < 0.00021208908081054686
1. Initial program 11.2
  \[\frac{x0}{1 - x1} - x0\]
2. Using strategy rm
3. Applied *-un-lft-identity11.2
  \[\leadsto \frac{x0}{1 - \color{blue}{1 \cdot x1}} - x0\]
4. Applied *-un-lft-identity11.2
  \[\leadsto \frac{x0}{\color{blue}{1 \cdot 1} - 1 \cdot x1} - x0\]
5. Applied distribute-lft-out--11.2
  \[\leadsto \frac{x0}{\color{blue}{1 \cdot \left(1 - x1\right)}} - x0\]
6. Applied add-cube-cbrt11.2
  \[\leadsto \frac{\color{blue}{\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \sqrt[3]{x0}}}{1 \cdot \left(1 - x1\right)} - x0\]
7. Applied times-frac10.9
  \[\leadsto \color{blue}{\frac{\sqrt[3]{x0} \cdot \sqrt[3]{x0}}{1} \cdot \frac{\sqrt[3]{x0}}{1 - x1}} - x0\]
8. Applied fma-neg8.9
  \[\leadsto \color{blue}{(\left(\frac{\sqrt[3]{x0} \cdot \sqrt[3]{x0}}{1}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*}\]
9. Simplified8.9
  \[\leadsto (\color{blue}{\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right)} \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\]
10. Using strategy rm
11. Applied add-exp-log8.9
  \[\leadsto \color{blue}{e^{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}}\]
12. Using strategy rm
13. Applied pow18.9
  \[\leadsto e^{\log \color{blue}{\left({\left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}^{1}\right)}}\]
14. Applied log-pow8.9
  \[\leadsto e^{\color{blue}{1 \cdot \log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}}\]
15. Applied exp-prod8.9
  \[\leadsto \color{blue}{{\left(e^{1}\right)}^{\left(\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)\right)}}\]
16. Simplified8.9
  \[\leadsto {\color{blue}{e}}^{\left(\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)\right)}\]
17. Using strategy rm
18. Applied add-cube-cbrt8.9
  \[\leadsto {e}^{\color{blue}{\left(\left(\sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)} \cdot \sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right) \cdot \sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right)}}\]
19. Applied pow-unpow8.9
  \[\leadsto \color{blue}{{\left({e}^{\left(\sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)} \cdot \sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right)}\right)}^{\left(\sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right)}}\]
if 0.00021208908081054686 < x1
1. Initial program 4.5
  \[\frac{x0}{1 - x1} - x0\]
2. Using strategy rm
3. Applied add-sqr-sqrt4.5
  \[\leadsto \frac{x0}{1 - \color{blue}{\sqrt{x1} \cdot \sqrt{x1}}} - x0\]
4. Applied *-un-lft-identity4.5
  \[\leadsto \frac{x0}{\color{blue}{1 \cdot 1} - \sqrt{x1} \cdot \sqrt{x1}} - x0\]
5. Applied difference-of-squares4.5
  \[\leadsto \frac{x0}{\color{blue}{\left(1 + \sqrt{x1}\right) \cdot \left(1 - \sqrt{x1}\right)}} - x0\]
6. Applied add-sqr-sqrt4.5
  \[\leadsto \frac{\color{blue}{\sqrt{x0} \cdot \sqrt{x0}}}{\left(1 + \sqrt{x1}\right) \cdot \left(1 - \sqrt{x1}\right)} - x0\]
7. Applied times-frac5.1
  \[\leadsto \color{blue}{\frac{\sqrt{x0}}{1 + \sqrt{x1}} \cdot \frac{\sqrt{x0}}{1 - \sqrt{x1}}} - x0\]
8. Applied fma-neg3.1
  \[\leadsto \color{blue}{(\left(\frac{\sqrt{x0}}{1 + \sqrt{x1}}\right) \cdot \left(\frac{\sqrt{x0}}{1 - \sqrt{x1}}\right) + \left(-x0\right))_*}\]
Recombined 2 regimes into one program.
Final simplification6.0
\[\leadsto \begin{array}{l} \mathbf{if}\;x1 \le 0.00021208908081054686:\\ \;\;\;\;{\left({e}^{\left(\sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)} \cdot \sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right)}\right)}^{\left(\sqrt[3]{\log \left((\left(\sqrt[3]{x0} \cdot \sqrt[3]{x0}\right) \cdot \left(\frac{\sqrt[3]{x0}}{1 - x1}\right) + \left(-x0\right))_*\right)}\right)}\\ \mathbf{else}:\\ \;\;\;\;(\left(\frac{\sqrt{x0}}{\sqrt{x1} + 1}\right) \cdot \left(\frac{\sqrt{x0}}{1 - \sqrt{x1}}\right) + \left(-x0\right))_*\\ \end{array}\]

could not determine a ground truth for program pre (more)

Error

Target

Derivation

`if x1 < 0.00021208908081054686`

`if 0.00021208908081054686 < x1`

Reproduce