Average Error: 0.5 → 0.5
Time: 23.6s
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{1}{\frac{\cos th}{\sqrt{2}}}}\]
\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{1}{\frac{\cos th}{\sqrt{2}}}}
double f(double a1, double a2, double th) {
        double r86717 = th;
        double r86718 = cos(r86717);
        double r86719 = 2.0;
        double r86720 = sqrt(r86719);
        double r86721 = r86718 / r86720;
        double r86722 = a1;
        double r86723 = r86722 * r86722;
        double r86724 = r86721 * r86723;
        double r86725 = a2;
        double r86726 = r86725 * r86725;
        double r86727 = r86721 * r86726;
        double r86728 = r86724 + r86727;
        return r86728;
}
↓
double f(double a1, double a2, double th) {
        double r86729 = a1;
        double r86730 = r86729 * r86729;
        double r86731 = a2;
        double r86732 = r86731 * r86731;
        double r86733 = r86730 + r86732;
        double r86734 = 1.0;
        double r86735 = th;
        double r86736 = cos(r86735);
        double r86737 = 2.0;
        double r86738 = sqrt(r86737);
        double r86739 = r86736 / r86738;
        double r86740 = r86734 / r86739;
        double r86741 = r86733 / r86740;
        return r86741;
}

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{\color{blue}{1 \cdot 2}}}{\cos th}}\]

  5. Applied sqrt-prod0.5

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

  6. Applied associate-/l*0.5

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

  7. Final simplification0.5

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

Reproduce

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