Average Error: 0.5 → 0.5
Time: 11.5s
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{\frac{\left(\cos th \cdot \sqrt{a1 \cdot a1 + a2 \cdot a2}\right) \cdot \sqrt{a1 \cdot a1 + a2 \cdot a2}}{\sqrt[3]{\sqrt{2}} \cdot \sqrt[3]{\sqrt{2}}}}{\sqrt[3]{\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{\frac{\left(\cos th \cdot \sqrt{a1 \cdot a1 + a2 \cdot a2}\right) \cdot \sqrt{a1 \cdot a1 + a2 \cdot a2}}{\sqrt[3]{\sqrt{2}} \cdot \sqrt[3]{\sqrt{2}}}}{\sqrt[3]{\sqrt{2}}}
double f(double a1, double a2, double th) {
        double r92983 = th;
        double r92984 = cos(r92983);
        double r92985 = 2.0;
        double r92986 = sqrt(r92985);
        double r92987 = r92984 / r92986;
        double r92988 = a1;
        double r92989 = r92988 * r92988;
        double r92990 = r92987 * r92989;
        double r92991 = a2;
        double r92992 = r92991 * r92991;
        double r92993 = r92987 * r92992;
        double r92994 = r92990 + r92993;
        return r92994;
}
↓
double f(double a1, double a2, double th) {
        double r92995 = th;
        double r92996 = cos(r92995);
        double r92997 = a1;
        double r92998 = r92997 * r92997;
        double r92999 = a2;
        double r93000 = r92999 * r92999;
        double r93001 = r92998 + r93000;
        double r93002 = sqrt(r93001);
        double r93003 = r92996 * r93002;
        double r93004 = r93003 * r93002;
        double r93005 = 2.0;
        double r93006 = sqrt(r93005);
        double r93007 = cbrt(r93006);
        double r93008 = r93007 * r93007;
        double r93009 = r93004 / r93008;
        double r93010 = r93009 / r93007;
        return r93010;
}

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{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}\]
  3. Using strategy rm

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

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

  5. Applied associate-*l*0.5

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

  6. Simplified0.5

    \[\leadsto 1 \cdot \color{blue}{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt{2}}}\]
  7. Using strategy rm

  8. Applied add-cube-cbrt0.5

    \[\leadsto 1 \cdot \frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\color{blue}{\left(\sqrt[3]{\sqrt{2}} \cdot \sqrt[3]{\sqrt{2}}\right) \cdot \sqrt[3]{\sqrt{2}}}}\]

  9. Applied associate-/r*0.5

    \[\leadsto 1 \cdot \color{blue}{\frac{\frac{\cos th \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)}{\sqrt[3]{\sqrt{2}} \cdot \sqrt[3]{\sqrt{2}}}}{\sqrt[3]{\sqrt{2}}}}\]
  10. Using strategy rm

  11. Applied add-sqr-sqrt0.5

    \[\leadsto 1 \cdot \frac{\frac{\cos th \cdot \color{blue}{\left(\sqrt{a1 \cdot a1 + a2 \cdot a2} \cdot \sqrt{a1 \cdot a1 + a2 \cdot a2}\right)}}{\sqrt[3]{\sqrt{2}} \cdot \sqrt[3]{\sqrt{2}}}}{\sqrt[3]{\sqrt{2}}}\]

  12. Applied associate-*r*0.5

    \[\leadsto 1 \cdot \frac{\frac{\color{blue}{\left(\cos th \cdot \sqrt{a1 \cdot a1 + a2 \cdot a2}\right) \cdot \sqrt{a1 \cdot a1 + a2 \cdot a2}}}{\sqrt[3]{\sqrt{2}} \cdot \sqrt[3]{\sqrt{2}}}}{\sqrt[3]{\sqrt{2}}}\]

  13. Final simplification0.5

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

Reproduce

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