_multiplyComplex, real part

Average Error: 0.0 → 0.0

Time: 2.4s

Precision: 64

Math

\[x.re \cdot y.re - x.im \cdot y.im\]

↓

\[x.re \cdot y.re - x.im \cdot y.im\]

C

double f(double x_re, double x_im, double y_re, double y_im) {
        double r50776 = x_re;
        double r50777 = y_re;
        double r50778 = r50776 * r50777;
        double r50779 = x_im;
        double r50780 = y_im;
        double r50781 = r50779 * r50780;
        double r50782 = r50778 - r50781;
        return r50782;
}

↓

double f(double x_re, double x_im, double y_re, double y_im) {
        double r50783 = x_re;
        double r50784 = y_re;
        double r50785 = r50783 * r50784;
        double r50786 = x_im;
        double r50787 = y_im;
        double r50788 = r50786 * r50787;
        double r50789 = r50785 - r50788;
        return r50789;
}

Error

Bits error versus x.re

Bits error versus x.im

Bits error versus y.re

Bits error versus y.im

Derivation

1. Initial program 0.0

   \[x.re \cdot y.re - x.im \cdot y.im\]
2. Using strategy rm

3. Applied flip-- 27.2

   \[\leadsto \color{blue}{\frac{\left(x.re \cdot y.re\right) \cdot \left(x.re \cdot y.re\right) - \left(x.im \cdot y.im\right) \cdot \left(x.im \cdot y.im\right)}{x.re \cdot y.re + x.im \cdot y.im}}\]
4. Using strategy rm

5. Applied *-un-lft-identity 27.2

   \[\leadsto \frac{\left(x.re \cdot y.re\right) \cdot \left(x.re \cdot y.re\right) - \left(x.im \cdot y.im\right) \cdot \left(x.im \cdot y.im\right)}{\color{blue}{1 \cdot \left(x.re \cdot y.re + x.im \cdot y.im\right)}}\]

6. Applied difference-of-squares 27.2

   \[\leadsto \frac{\color{blue}{\left(x.re \cdot y.re + x.im \cdot y.im\right) \cdot \left(x.re \cdot y.re - x.im \cdot y.im\right)}}{1 \cdot \left(x.re \cdot y.re + x.im \cdot y.im\right)}\]

7. Applied times-frac 1.0

   \[\leadsto \color{blue}{\frac{x.re \cdot y.re + x.im \cdot y.im}{1} \cdot \frac{x.re \cdot y.re - x.im \cdot y.im}{x.re \cdot y.re + x.im \cdot y.im}}\]

8. Simplified 1.0

   \[\leadsto \color{blue}{\left(x.re \cdot y.re + x.im \cdot y.im\right)} \cdot \frac{x.re \cdot y.re - x.im \cdot y.im}{x.re \cdot y.re + x.im \cdot y.im}\]
9. Using strategy rm

10. Applied flip-+ 27.3

    \[\leadsto \left(x.re \cdot y.re + x.im \cdot y.im\right) \cdot \frac{x.re \cdot y.re - x.im \cdot y.im}{\color{blue}{\frac{\left(x.re \cdot y.re\right) \cdot \left(x.re \cdot y.re\right) - \left(x.im \cdot y.im\right) \cdot \left(x.im \cdot y.im\right)}{x.re \cdot y.re - x.im \cdot y.im}}}\]

11. Applied associate-/r/ 27.4

    \[\leadsto \left(x.re \cdot y.re + x.im \cdot y.im\right) \cdot \color{blue}{\left(\frac{x.re \cdot y.re - x.im \cdot y.im}{\left(x.re \cdot y.re\right) \cdot \left(x.re \cdot y.re\right) - \left(x.im \cdot y.im\right) \cdot \left(x.im \cdot y.im\right)} \cdot \left(x.re \cdot y.re - x.im \cdot y.im\right)\right)}\]

12. Applied associate-*r* 27.4

    \[\leadsto \color{blue}{\left(\left(x.re \cdot y.re + x.im \cdot y.im\right) \cdot \frac{x.re \cdot y.re - x.im \cdot y.im}{\left(x.re \cdot y.re\right) \cdot \left(x.re \cdot y.re\right) - \left(x.im \cdot y.im\right) \cdot \left(x.im \cdot y.im\right)}\right) \cdot \left(x.re \cdot y.re - x.im \cdot y.im\right)}\]

13. Simplified 0.0

    \[\leadsto \color{blue}{1} \cdot \left(x.re \cdot y.re - x.im \cdot y.im\right)\]

14. Final simplification 0.0

    \[\leadsto x.re \cdot y.re - x.im \cdot y.im\]

Reproduce

herbie shell --seed 2019353 
(FPCore (x.re x.im y.re y.im)
  :name "_multiplyComplex, real part"
  :precision binary64
  (- (* x.re y.re) (* x.im y.im)))