Error

Try it out

Target

Derivation

1. Initial program 8.4

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

3. Applied flip--7.7

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

5. Applied add-sqr-sqrt6.6

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

7. Applied flip3--6.0

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

9. Applied flip--5.4

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

10. Final simplification5.4

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

Reproduce

herbie shell --seed 2018360 
(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: 8.7s)Debug log