Average Error: 0.0 → 0.0
Time: 3.3s
Precision: 64
\[\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]
↓
\[y \cdot y + x \cdot \left(2 \cdot y + x\right)\]
\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y
↓
y \cdot y + x \cdot \left(2 \cdot y + x\right)
double f(double x, double y) {
        double r519416 = x;
        double r519417 = r519416 * r519416;
        double r519418 = 2.0;
        double r519419 = r519416 * r519418;
        double r519420 = y;
        double r519421 = r519419 * r519420;
        double r519422 = r519417 + r519421;
        double r519423 = r519420 * r519420;
        double r519424 = r519422 + r519423;
        return r519424;
}
↓
double f(double x, double y) {
        double r519425 = y;
        double r519426 = r519425 * r519425;
        double r519427 = x;
        double r519428 = 2.0;
        double r519429 = r519428 * r519425;
        double r519430 = r519429 + r519427;
        double r519431 = r519427 * r519430;
        double r519432 = r519426 + r519431;
        return r519432;
}

Error

Bits error versus x

Bits error versus y

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Target

Original0.0
Target0.0
Herbie0.0
\[x \cdot x + \left(y \cdot y + \left(x \cdot y\right) \cdot 2\right)\]

Derivation

  1. Initial program 0.0

    \[\left(x \cdot x + \left(x \cdot 2\right) \cdot y\right) + y \cdot y\]

  2. Simplified0.0

    \[\leadsto \color{blue}{y \cdot y + x \cdot \left(2 \cdot y + x\right)}\]

  3. Final simplification0.0

    \[\leadsto y \cdot y + x \cdot \left(2 \cdot y + x\right)\]

Reproduce

herbie shell --seed 2019208 
(FPCore (x y)
  :name "Examples.Basics.ProofTests:f4 from sbv-4.4"
  :precision binary64

  :herbie-target
  (+ (* x x) (+ (* y y) (* (* x y) 2)))

  (+ (+ (* x x) (* (* x 2) y)) (* y y)))