Error

Try it out

Target

Derivation

1. Initial program 8.4

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

3. Applied clear-num7.5

   \[\leadsto \color{blue}{\frac{1}{\frac{1 - x1}{x0}}} - x0\]
4. Using strategy rm

5. Applied flip3--7.6

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

7. Applied *-un-lft-identity7.6

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

8. Applied add-cube-cbrt7.5

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

9. Applied times-frac7.5

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

10. Simplified5.1

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

11. Final simplification5.1

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

Reproduce

herbie shell --seed 2019002 
(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))

Details

Time bar (total: 36.2s)Debug log