Average Error: 0.5 → 0.5
Time: 58.0s
Precision: 64
\[\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)\]
↓
\[\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}\]
\frac{\cos th}{\sqrt{2}} \cdot \left(a1 \cdot a1\right) + \frac{\cos th}{\sqrt{2}} \cdot \left(a2 \cdot a2\right)
↓
\cos th \cdot \frac{a1 \cdot a1 + a2 \cdot a2}{\sqrt{2}}
double f(double a1, double a2, double th) {
        double r3325104 = th;
        double r3325105 = cos(r3325104);
        double r3325106 = 2.0;
        double r3325107 = sqrt(r3325106);
        double r3325108 = r3325105 / r3325107;
        double r3325109 = a1;
        double r3325110 = r3325109 * r3325109;
        double r3325111 = r3325108 * r3325110;
        double r3325112 = a2;
        double r3325113 = r3325112 * r3325112;
        double r3325114 = r3325108 * r3325113;
        double r3325115 = r3325111 + r3325114;
        return r3325115;
}
↓
double f(double a1, double a2, double th) {
        double r3325116 = th;
        double r3325117 = cos(r3325116);
        double r3325118 = a1;
        double r3325119 = r3325118 * r3325118;
        double r3325120 = a2;
        double r3325121 = r3325120 * r3325120;
        double r3325122 = r3325119 + r3325121;
        double r3325123 = 2.0;
        double r3325124 = sqrt(r3325123);
        double r3325125 = r3325122 / r3325124;
        double r3325126 = r3325117 * r3325125;
        return r3325126;
}

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 add-sqr-sqrt0.5

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

  6. Applied sqrt-prod0.6

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

  7. Applied times-frac0.6

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

  8. Applied associate-/r*0.5

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

  9. Simplified0.5

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

  11. Applied associate-/r/0.5

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

  12. Simplified0.5

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

  13. Final simplification0.5

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

Reproduce

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