Average Error: 0.5 → 0.5
Time: 19.4s
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{\sqrt{a1 \cdot a1 + a2 \cdot a2}}{\frac{\frac{\sqrt{2}}{\cos th}}{\sqrt{a1 \cdot a1 + a2 \cdot a2}}}\]
\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)
↓
\frac{\sqrt{a1 \cdot a1 + a2 \cdot a2}}{\frac{\frac{\sqrt{2}}{\cos th}}{\sqrt{a1 \cdot a1 + a2 \cdot a2}}}
double f(double a1, double a2, double th) {
        double r64119 = th;
        double r64120 = cos(r64119);
        double r64121 = 2.0;
        double r64122 = sqrt(r64121);
        double r64123 = r64120 / r64122;
        double r64124 = a1;
        double r64125 = r64124 * r64124;
        double r64126 = r64123 * r64125;
        double r64127 = a2;
        double r64128 = r64127 * r64127;
        double r64129 = r64123 * r64128;
        double r64130 = r64126 + r64129;
        return r64130;
}
↓
double f(double a1, double a2, double th) {
        double r64131 = a1;
        double r64132 = r64131 * r64131;
        double r64133 = a2;
        double r64134 = r64133 * r64133;
        double r64135 = r64132 + r64134;
        double r64136 = sqrt(r64135);
        double r64137 = 2.0;
        double r64138 = sqrt(r64137);
        double r64139 = th;
        double r64140 = cos(r64139);
        double r64141 = r64138 / r64140;
        double r64142 = r64141 / r64136;
        double r64143 = r64136 / r64142;
        return r64143;
}

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 \frac{\cos th}{\color{blue}{1 \cdot \sqrt{2}}} \cdot \left(a1 \cdot a1 + a2 \cdot a2\right)\]

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

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

  6. Applied times-frac0.5

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

  7. Applied associate-*l*0.5

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

  8. Simplified0.5

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

  10. Applied associate-/l*0.5

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

  12. Applied add-sqr-sqrt0.5

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

  13. Applied associate-/l*0.5

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

  14. Final simplification0.5

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

Reproduce

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