Average Error: 7.9 → 5.4
Time: 1.1m
Precision: 64
\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]
\[\frac{x0}{1 - x1} - x0\]
↓
\[\frac{\frac{{\left(\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}}\right)}^{3} - {\left(\left(x0 \cdot x0\right) \cdot x0\right)}^{3}}{\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} \cdot \frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} + \left(\left(\left(x0 \cdot x0\right) \cdot x0\right) \cdot \frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} + \left(\left(x0 \cdot x0\right) \cdot x0\right) \cdot \left(\left(x0 \cdot x0\right) \cdot x0\right)\right)}}{\left(x0 \cdot \sqrt[3]{\left(\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}\right) \cdot \frac{x0}{1 - x1}} + x0 \cdot x0\right) + \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}\]
\frac{x0}{1 - x1} - x0
↓
\frac{\frac{{\left(\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}}\right)}^{3} - {\left(\left(x0 \cdot x0\right) \cdot x0\right)}^{3}}{\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} \cdot \frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} + \left(\left(\left(x0 \cdot x0\right) \cdot x0\right) \cdot \frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} + \left(\left(x0 \cdot x0\right) \cdot x0\right) \cdot \left(\left(x0 \cdot x0\right) \cdot x0\right)\right)}}{\left(x0 \cdot \sqrt[3]{\left(\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}\right) \cdot \frac{x0}{1 - x1}} + x0 \cdot x0\right) + \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}
double f(double x0, double x1) {
        double r12345378 = x0;
        double r12345379 = 1.0;
        double r12345380 = x1;
        double r12345381 = r12345379 - r12345380;
        double r12345382 = r12345378 / r12345381;
        double r12345383 = r12345382 - r12345378;
        return r12345383;
}
↓
double f(double x0, double x1) {
        double r12345384 = x0;
        double r12345385 = 1.0;
        double r12345386 = x1;
        double r12345387 = r12345385 - r12345386;
        double r12345388 = sqrt(r12345387);
        double r12345389 = r12345384 / r12345388;
        double r12345390 = r12345384 / r12345387;
        double r12345391 = r12345389 * r12345390;
        double r12345392 = r12345387 / r12345384;
        double r12345393 = r12345388 * r12345392;
        double r12345394 = r12345391 / r12345393;
        double r12345395 = 3.0;
        double r12345396 = pow(r12345394, r12345395);
        double r12345397 = r12345384 * r12345384;
        double r12345398 = r12345397 * r12345384;
        double r12345399 = pow(r12345398, r12345395);
        double r12345400 = r12345396 - r12345399;
        double r12345401 = r12345394 * r12345394;
        double r12345402 = r12345398 * r12345394;
        double r12345403 = r12345398 * r12345398;
        double r12345404 = r12345402 + r12345403;
        double r12345405 = r12345401 + r12345404;
        double r12345406 = r12345400 / r12345405;
        double r12345407 = r12345390 * r12345390;
        double r12345408 = r12345407 * r12345390;
        double r12345409 = cbrt(r12345408);
        double r12345410 = r12345384 * r12345409;
        double r12345411 = r12345410 + r12345397;
        double r12345412 = r12345411 + r12345407;
        double r12345413 = r12345406 / r12345412;
        return r12345413;
}

Error

Bits error versus x0

Bits error versus x1

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original7.9
Target0.3
Herbie5.4
\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

  1. Initial program 7.9

    \[\frac{x0}{1 - x1} - x0\]
  2. Using strategy rm

  3. Applied flip3--7.7

    \[\leadsto \color{blue}{\frac{{\left(\frac{x0}{1 - x1}\right)}^{3} - {x0}^{3}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}}\]

  4. Simplified7.3

    \[\leadsto \frac{\color{blue}{\frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}\right) - x0 \cdot \left(x0 \cdot x0\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]
  5. Using strategy rm

  6. Applied clear-num7.1

    \[\leadsto \frac{\frac{x0}{1 - x1} \cdot \left(\frac{x0}{1 - x1} \cdot \color{blue}{\frac{1}{\frac{1 - x1}{x0}}}\right) - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]

  7. Applied un-div-inv7.1

    \[\leadsto \frac{\frac{x0}{1 - x1} \cdot \color{blue}{\frac{\frac{x0}{1 - x1}}{\frac{1 - x1}{x0}}} - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]

  8. Applied add-sqr-sqrt6.9

    \[\leadsto \frac{\frac{x0}{\color{blue}{\sqrt{1 - x1} \cdot \sqrt{1 - x1}}} \cdot \frac{\frac{x0}{1 - x1}}{\frac{1 - x1}{x0}} - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]

  9. Applied associate-/r*6.9

    \[\leadsto \frac{\color{blue}{\frac{\frac{x0}{\sqrt{1 - x1}}}{\sqrt{1 - x1}}} \cdot \frac{\frac{x0}{1 - x1}}{\frac{1 - x1}{x0}} - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]

  10. Applied frac-times6.0

    \[\leadsto \frac{\color{blue}{\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}}} - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{1 - x1} \cdot x0\right)}\]
  11. Using strategy rm

  12. Applied add-cbrt-cube6.0

    \[\leadsto \frac{\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{x0}{\color{blue}{\sqrt[3]{\left(\left(1 - x1\right) \cdot \left(1 - x1\right)\right) \cdot \left(1 - x1\right)}}} \cdot x0\right)}\]

  13. Applied add-cbrt-cube6.0

    \[\leadsto \frac{\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \frac{\color{blue}{\sqrt[3]{\left(x0 \cdot x0\right) \cdot x0}}}{\sqrt[3]{\left(\left(1 - x1\right) \cdot \left(1 - x1\right)\right) \cdot \left(1 - x1\right)}} \cdot x0\right)}\]

  14. Applied cbrt-undiv6.0

    \[\leadsto \frac{\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \color{blue}{\sqrt[3]{\frac{\left(x0 \cdot x0\right) \cdot x0}{\left(\left(1 - x1\right) \cdot \left(1 - x1\right)\right) \cdot \left(1 - x1\right)}}} \cdot x0\right)}\]

  15. Simplified6.0

    \[\leadsto \frac{\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} - x0 \cdot \left(x0 \cdot x0\right)}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \sqrt[3]{\color{blue}{\left(\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}\right) \cdot \frac{x0}{1 - x1}}} \cdot x0\right)}\]
  16. Using strategy rm

  17. Applied flip3--5.4

    \[\leadsto \frac{\color{blue}{\frac{{\left(\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}}\right)}^{3} - {\left(x0 \cdot \left(x0 \cdot x0\right)\right)}^{3}}{\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} \cdot \frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} + \left(\left(x0 \cdot \left(x0 \cdot x0\right)\right) \cdot \left(x0 \cdot \left(x0 \cdot x0\right)\right) + \frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} \cdot \left(x0 \cdot \left(x0 \cdot x0\right)\right)\right)}}}{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} + \left(x0 \cdot x0 + \sqrt[3]{\left(\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}\right) \cdot \frac{x0}{1 - x1}} \cdot x0\right)}\]

  18. Final simplification5.4

    \[\leadsto \frac{\frac{{\left(\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}}\right)}^{3} - {\left(\left(x0 \cdot x0\right) \cdot x0\right)}^{3}}{\frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} \cdot \frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} + \left(\left(\left(x0 \cdot x0\right) \cdot x0\right) \cdot \frac{\frac{x0}{\sqrt{1 - x1}} \cdot \frac{x0}{1 - x1}}{\sqrt{1 - x1} \cdot \frac{1 - x1}{x0}} + \left(\left(x0 \cdot x0\right) \cdot x0\right) \cdot \left(\left(x0 \cdot x0\right) \cdot x0\right)\right)}}{\left(x0 \cdot \sqrt[3]{\left(\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}\right) \cdot \frac{x0}{1 - x1}} + x0 \cdot x0\right) + \frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1}}\]

Reproduce

herbie shell --seed 2019158 
(FPCore (x0 x1)
  :name "(- (/ x0 (- 1 x1)) x0)"
  :pre (or (and (== x0 1.855) (== x1 0.000209)) (and (== x0 2.985) (== x1 0.0186)))

  :herbie-target
  (/ (* x0 x1) (- 1 x1))

  (- (/ x0 (- 1 x1)) x0))