Average Error: 8.4 → 5.4
Time: 6.6s
Precision: binary64
\[x0 = 1.855 \land x1 = 0.000209 \lor x0 = 2.985 \land x1 = 0.0186\]
\[\frac{x0}{1 - x1} - x0\]
↓
\[\frac{x0 \cdot \frac{\frac{{\left({\left(\frac{x0}{{\left(1 - x1\right)}^{2}}\right)}^{3}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{{\left(\frac{1}{{\left(1 + \sqrt{x1}\right)}^{2}}\right)}^{6} \cdot {\left(\frac{x0}{{\left(1 - \sqrt{x1}\right)}^{2}}\right)}^{6} + \left({x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{{\left(1 - x1\right)}^{3}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}\]
\frac{x0}{1 - x1} - x0
↓
\frac{x0 \cdot \frac{\frac{{\left({\left(\frac{x0}{{\left(1 - x1\right)}^{2}}\right)}^{3}\right)}^{3} - {\left({x0}^{3}\right)}^{3}}{{\left(\frac{1}{{\left(1 + \sqrt{x1}\right)}^{2}}\right)}^{6} \cdot {\left(\frac{x0}{{\left(1 - \sqrt{x1}\right)}^{2}}\right)}^{6} + \left({x0}^{6} + \frac{{x0}^{6}}{{\left(1 - x1\right)}^{6}}\right)}}{\frac{x0}{1 - x1} \cdot \frac{x0}{{\left(1 - x1\right)}^{3}} + x0 \cdot \left(x0 + \frac{x0}{\left(1 - x1\right) \cdot \left(1 - x1\right)}\right)}}{x0 + \frac{x0}{1 - x1}}
(FPCore (x0 x1) :precision binary64 (- (/ x0 (- 1.0 x1)) x0))
↓
(FPCore (x0 x1)
 :precision binary64
 (/
  (*
   x0
   (/
    (/
     (- (pow (pow (/ x0 (pow (- 1.0 x1) 2.0)) 3.0) 3.0) (pow (pow x0 3.0) 3.0))
     (+
      (*
       (pow (/ 1.0 (pow (+ 1.0 (sqrt x1)) 2.0)) 6.0)
       (pow (/ x0 (pow (- 1.0 (sqrt x1)) 2.0)) 6.0))
      (+ (pow x0 6.0) (/ (pow x0 6.0) (pow (- 1.0 x1) 6.0)))))
    (+
     (* (/ x0 (- 1.0 x1)) (/ x0 (pow (- 1.0 x1) 3.0)))
     (* x0 (+ x0 (/ x0 (* (- 1.0 x1) (- 1.0 x1))))))))
  (+ x0 (/ x0 (- 1.0 x1)))))
double code(double x0, double x1) {
	return (x0 / (1.0 - x1)) - x0;
}
↓
double code(double x0, double x1) {
	return (x0 * (((pow(pow((x0 / pow((1.0 - x1), 2.0)), 3.0), 3.0) - pow(pow(x0, 3.0), 3.0)) / ((pow((1.0 / pow((1.0 + sqrt(x1)), 2.0)), 6.0) * pow((x0 / pow((1.0 - sqrt(x1)), 2.0)), 6.0)) + (pow(x0, 6.0) + (pow(x0, 6.0) / pow((1.0 - x1), 6.0))))) / (((x0 / (1.0 - x1)) * (x0 / pow((1.0 - x1), 3.0))) + (x0 * (x0 + (x0 / ((1.0 - x1) * (1.0 - x1)))))))) / (x0 + (x0 / (1.0 - x1)));
}

Error

Bits error versus x0

Bits error versus x1

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original8.4
Target0.5
Herbie5.4
\[\frac{x0 \cdot x1}{1 - x1}\]

Derivation

  1. Initial program 8.4

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

  3. Applied flip--_binary64_31687.8

    \[\leadsto \color{blue}{\frac{\frac{x0}{1 - x1} \cdot \frac{x0}{1 - x1} - x0 \cdot x0}{\frac{x0}{1 - x1} + x0}}\]

  4. Simplified6.9

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

  5. Simplified6.9

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

  7. Applied flip3--_binary64_31416.1

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

  8. Simplified6.1

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

  10. Applied flip3--_binary64_31415.4

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

  11. Simplified5.4

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

  12. Simplified5.3

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

  14. Applied add-sqr-sqrt_binary64_31275.3

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

  15. Applied *-un-lft-identity_binary64_31425.3

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

  16. Applied difference-of-squares_binary64_31715.3

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

  17. Applied unpow-prod-down_binary64_30775.4

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

  18. Applied *-un-lft-identity_binary64_31425.4

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

  19. Applied times-frac_binary64_31375.4

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

  20. Applied unpow-prod-down_binary64_30775.4

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

  21. Final simplification5.4

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

Reproduce

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

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

  (- (/ x0 (- 1.0 x1)) x0))