Average Error: 0.4 → 0.4
Time: 11.9s
Precision: 64
\[1.0009999999999999 \le x \le 2 \land 1.0009999999999999 \le y \le 2\]
\[\frac{x \cdot y - 1}{\left(x \cdot y\right) \cdot \left(x \cdot y\right) - 1}\]
\[\frac{\frac{x \cdot y - 1}{x \cdot y + \sqrt{1}}}{x \cdot y - \sqrt{1}}\]
\frac{x \cdot y - 1}{\left(x \cdot y\right) \cdot \left(x \cdot y\right) - 1}
\frac{\frac{x \cdot y - 1}{x \cdot y + \sqrt{1}}}{x \cdot y - \sqrt{1}}
double f(double x, double y) {
        double r151114 = x;
        double r151115 = y;
        double r151116 = r151114 * r151115;
        double r151117 = 1.0;
        double r151118 = r151116 - r151117;
        double r151119 = r151116 * r151116;
        double r151120 = r151119 - r151117;
        double r151121 = r151118 / r151120;
        return r151121;
}

double f(double x, double y) {
        double r151122 = x;
        double r151123 = y;
        double r151124 = r151122 * r151123;
        double r151125 = 1.0;
        double r151126 = r151124 - r151125;
        double r151127 = sqrt(r151125);
        double r151128 = r151124 + r151127;
        double r151129 = r151126 / r151128;
        double r151130 = r151124 - r151127;
        double r151131 = r151129 / r151130;
        return r151131;
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 0.4

    \[\frac{x \cdot y - 1}{\left(x \cdot y\right) \cdot \left(x \cdot y\right) - 1}\]
  2. Using strategy rm
  3. Applied add-sqr-sqrt0.4

    \[\leadsto \frac{x \cdot y - 1}{\left(x \cdot y\right) \cdot \left(x \cdot y\right) - \color{blue}{\sqrt{1} \cdot \sqrt{1}}}\]
  4. Applied difference-of-squares0.4

    \[\leadsto \frac{x \cdot y - 1}{\color{blue}{\left(x \cdot y + \sqrt{1}\right) \cdot \left(x \cdot y - \sqrt{1}\right)}}\]
  5. Applied associate-/r*0.4

    \[\leadsto \color{blue}{\frac{\frac{x \cdot y - 1}{x \cdot y + \sqrt{1}}}{x \cdot y - \sqrt{1}}}\]
  6. Final simplification0.4

    \[\leadsto \frac{\frac{x \cdot y - 1}{x \cdot y + \sqrt{1}}}{x \cdot y - \sqrt{1}}\]

Reproduce

herbie shell --seed 1 
(FPCore (x y)
  :name "sec4-example"
  :pre (and (<= 1.001 x 2.0) (<= 1.001 y 2.0))
  (/ (- (* x y) 1.0) (- (* (* x y) (* x y)) 1.0)))