Average Error: 15.1 → 14.6
Time: 2.1m
Precision: 64
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\frac{\left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} + \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right) \cdot \left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} - \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right)}{\mathsf{fma}\left(\sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}, 1, \mathsf{fma}\left(1, 1, \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right)\right) \cdot \mathsf{fma}\left(\left(1 \cdot 1\right) \cdot 1, \left(1 \cdot 1\right) \cdot 1, \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5} + \left(1 \cdot 1\right) \cdot 1\right) \cdot \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)\right)}\]
1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\frac{\left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} + \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right) \cdot \left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} - \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right)}{\mathsf{fma}\left(\sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}, 1, \mathsf{fma}\left(1, 1, \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right)\right) \cdot \mathsf{fma}\left(\left(1 \cdot 1\right) \cdot 1, \left(1 \cdot 1\right) \cdot 1, \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5} + \left(1 \cdot 1\right) \cdot 1\right) \cdot \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)\right)}
double f(double x) {
        double r9729120 = 1.0;
        double r9729121 = 0.5;
        double r9729122 = x;
        double r9729123 = hypot(r9729120, r9729122);
        double r9729124 = r9729120 / r9729123;
        double r9729125 = r9729120 + r9729124;
        double r9729126 = r9729121 * r9729125;
        double r9729127 = sqrt(r9729126);
        double r9729128 = r9729120 - r9729127;
        return r9729128;
}
↓
double f(double x) {
        double r9729129 = 1.0;
        double r9729130 = r9729129 * r9729129;
        double r9729131 = r9729130 * r9729129;
        double r9729132 = 3.0;
        double r9729133 = pow(r9729131, r9729132);
        double r9729134 = sqrt(r9729133);
        double r9729135 = x;
        double r9729136 = hypot(r9729129, r9729135);
        double r9729137 = r9729129 / r9729136;
        double r9729138 = r9729137 + r9729129;
        double r9729139 = 0.5;
        double r9729140 = r9729138 * r9729139;
        double r9729141 = sqrt(r9729140);
        double r9729142 = r9729140 * r9729141;
        double r9729143 = pow(r9729142, r9729132);
        double r9729144 = sqrt(r9729143);
        double r9729145 = r9729134 + r9729144;
        double r9729146 = r9729134 - r9729144;
        double r9729147 = r9729145 * r9729146;
        double r9729148 = fma(r9729129, r9729129, r9729140);
        double r9729149 = fma(r9729141, r9729129, r9729148);
        double r9729150 = r9729142 + r9729131;
        double r9729151 = r9729150 * r9729142;
        double r9729152 = fma(r9729131, r9729131, r9729151);
        double r9729153 = r9729149 * r9729152;
        double r9729154 = r9729147 / r9729153;
        return r9729154;
}

Error

Bits error versus x

Derivation

  1. Initial program 15.1

    \[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
  2. Using strategy rm

  3. Applied flip3--15.3

    \[\leadsto \color{blue}{\frac{{1}^{3} - {\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}{1 \cdot 1 + \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}}\]

  4. Simplified15.1

    \[\leadsto \frac{\color{blue}{\left(1 \cdot 1\right) \cdot 1 - \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}{1 \cdot 1 + \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1 \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}\]

  5. Simplified14.6

    \[\leadsto \frac{\left(1 \cdot 1\right) \cdot 1 - \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}{\color{blue}{\mathsf{fma}\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 1, \mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}}\]
  6. Using strategy rm

  7. Applied flip3--15.1

    \[\leadsto \frac{\color{blue}{\frac{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3} - {\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}{\left(\left(1 \cdot 1\right) \cdot 1\right) \cdot \left(\left(1 \cdot 1\right) \cdot 1\right) + \left(\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right) \cdot \left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right) + \left(\left(1 \cdot 1\right) \cdot 1\right) \cdot \left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)\right)}}}{\mathsf{fma}\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 1, \mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)}\]

  8. Applied associate-/l/15.1

    \[\leadsto \color{blue}{\frac{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3} - {\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}{\mathsf{fma}\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 1, \mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right) \cdot \left(\left(\left(1 \cdot 1\right) \cdot 1\right) \cdot \left(\left(1 \cdot 1\right) \cdot 1\right) + \left(\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right) \cdot \left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right) + \left(\left(1 \cdot 1\right) \cdot 1\right) \cdot \left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)\right)\right)}}\]

  9. Simplified14.6

    \[\leadsto \frac{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3} - {\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}{\color{blue}{\mathsf{fma}\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 1, \mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right) \cdot \mathsf{fma}\left(\left(1 \cdot 1\right) \cdot 1, \left(1 \cdot 1\right) \cdot 1, \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right) \cdot \left(\left(1 \cdot 1\right) \cdot 1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)\right)}}\]
  10. Using strategy rm

  11. Applied add-sqr-sqrt14.6

    \[\leadsto \frac{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3} - \color{blue}{\sqrt{{\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}} \cdot \sqrt{{\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}}}{\mathsf{fma}\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 1, \mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right) \cdot \mathsf{fma}\left(\left(1 \cdot 1\right) \cdot 1, \left(1 \cdot 1\right) \cdot 1, \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right) \cdot \left(\left(1 \cdot 1\right) \cdot 1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)\right)}\]

  12. Applied add-sqr-sqrt14.6

    \[\leadsto \frac{\color{blue}{\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} \cdot \sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}}} - \sqrt{{\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}} \cdot \sqrt{{\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}}{\mathsf{fma}\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 1, \mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right) \cdot \mathsf{fma}\left(\left(1 \cdot 1\right) \cdot 1, \left(1 \cdot 1\right) \cdot 1, \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right) \cdot \left(\left(1 \cdot 1\right) \cdot 1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)\right)}\]

  13. Applied difference-of-squares14.6

    \[\leadsto \frac{\color{blue}{\left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} + \sqrt{{\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}\right) \cdot \left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} - \sqrt{{\left(\left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right) \cdot \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\right)}^{3}}\right)}}{\mathsf{fma}\left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}, 1, \mathsf{fma}\left(1, 1, 0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right) \cdot \mathsf{fma}\left(\left(1 \cdot 1\right) \cdot 1, \left(1 \cdot 1\right) \cdot 1, \left(\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right) \cdot \left(\left(1 \cdot 1\right) \cdot 1 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} \cdot \left(0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)\right)\right)\right)}\]

  14. Final simplification14.6

    \[\leadsto \frac{\left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} + \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right) \cdot \left(\sqrt{{\left(\left(1 \cdot 1\right) \cdot 1\right)}^{3}} - \sqrt{{\left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)}^{3}}\right)}{\mathsf{fma}\left(\sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}, 1, \mathsf{fma}\left(1, 1, \left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right)\right) \cdot \mathsf{fma}\left(\left(1 \cdot 1\right) \cdot 1, \left(1 \cdot 1\right) \cdot 1, \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5} + \left(1 \cdot 1\right) \cdot 1\right) \cdot \left(\left(\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5\right) \cdot \sqrt{\left(\frac{1}{\mathsf{hypot}\left(1, x\right)} + 1\right) \cdot 0.5}\right)\right)}\]

Reproduce

herbie shell --seed 2019200 +o rules:numerics
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))