Average Error: 0.5 → 0.5
Time: 21.9s
Precision: 64
\[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\]
↓
\[\frac{a1 \cdot a1 + a2 \cdot a2}{\frac{\sqrt{2}}{\cos th}}\]
\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)
↓
\frac{a1 \cdot a1 + a2 \cdot a2}{\frac{\sqrt{2}}{\cos th}}
double f(double a1, double a2, double th) {
        double r86548 = th;
        double r86549 = cos(r86548);
        double r86550 = 2.0;
        double r86551 = sqrt(r86550);
        double r86552 = r86549 / r86551;
        double r86553 = a1;
        double r86554 = r86553 * r86553;
        double r86555 = r86552 * r86554;
        double r86556 = a2;
        double r86557 = r86556 * r86556;
        double r86558 = r86552 * r86557;
        double r86559 = r86555 + r86558;
        return r86559;
}
↓
double f(double a1, double a2, double th) {
        double r86560 = a1;
        double r86561 = r86560 * r86560;
        double r86562 = a2;
        double r86563 = r86562 * r86562;
        double r86564 = r86561 + r86563;
        double r86565 = 2.0;
        double r86566 = sqrt(r86565);
        double r86567 = th;
        double r86568 = cos(r86567);
        double r86569 = r86566 / r86568;
        double r86570 = r86564 / r86569;
        return r86570;
}

Error

Bits error versus a1

Bits error versus a2

Bits error versus th

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 0.5

    \[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\]

  2. Simplified0.5

    \[\leadsto \color{blue}{\frac{a1 \cdot a1 + a2 \cdot a2}{\frac{\sqrt{2}}{\cos th}}}\]
  3. Using strategy rm

  4. Applied *-un-lft-identity0.5

    \[\leadsto \frac{a1 \cdot a1 + a2 \cdot a2}{\frac{\sqrt{2}}{\color{blue}{1 \cdot \cos th}}}\]

  5. Applied *-un-lft-identity0.5

    \[\leadsto \frac{a1 \cdot a1 + a2 \cdot a2}{\frac{\sqrt{\color{blue}{1 \cdot 2}}}{1 \cdot \cos th}}\]

  6. Applied sqrt-prod0.5

    \[\leadsto \frac{a1 \cdot a1 + a2 \cdot a2}{\frac{\color{blue}{\sqrt{1} \cdot \sqrt{2}}}{1 \cdot \cos th}}\]

  7. Applied times-frac0.5

    \[\leadsto \frac{a1 \cdot a1 + a2 \cdot a2}{\color{blue}{\frac{\sqrt{1}}{1} \cdot \frac{\sqrt{2}}{\cos th}}}\]

  8. Simplified0.5

    \[\leadsto \frac{a1 \cdot a1 + a2 \cdot a2}{\color{blue}{1} \cdot \frac{\sqrt{2}}{\cos th}}\]

  9. Final simplification0.5

    \[\leadsto \frac{a1 \cdot a1 + a2 \cdot a2}{\frac{\sqrt{2}}{\cos th}}\]

Reproduce

herbie shell --seed 2019174 
(FPCore (a1 a2 th)
  :name "Migdal et al, Equation (64)"
  (+ (* (/ (cos th) (sqrt 2.0)) (* a1 a1)) (* (/ (cos th) (sqrt 2.0)) (* a2 a2))))