Average Error: 15.5 → 15.1
Time: 50.8s
Precision: 64
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\frac{\frac{1 \cdot 1}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1} \cdot \frac{1 \cdot 1}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1} - \frac{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1} \cdot \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1}\right)\right)}{\frac{1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}}{\frac{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1}{0.5}} + \frac{1 \cdot 1}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1}}\]
1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\frac{\frac{1 \cdot 1}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1} \cdot \frac{1 \cdot 1}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1} - \frac{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1} \cdot \mathsf{log1p}\left(\mathsf{expm1}\left(\frac{\left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right) \cdot 0.5}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1}\right)\right)}{\frac{1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}}{\frac{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1}{0.5}} + \frac{1 \cdot 1}{\sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)} + 1}}
double f(double x) {
        double r357164 = 1.0;
        double r357165 = 0.5;
        double r357166 = x;
        double r357167 = hypot(r357164, r357166);
        double r357168 = r357164 / r357167;
        double r357169 = r357164 + r357168;
        double r357170 = r357165 * r357169;
        double r357171 = sqrt(r357170);
        double r357172 = r357164 - r357171;
        return r357172;
}
↓
double f(double x) {
        double r357173 = 1.0;
        double r357174 = r357173 * r357173;
        double r357175 = 0.5;
        double r357176 = x;
        double r357177 = hypot(r357173, r357176);
        double r357178 = r357173 / r357177;
        double r357179 = r357173 + r357178;
        double r357180 = r357175 * r357179;
        double r357181 = sqrt(r357180);
        double r357182 = r357181 + r357173;
        double r357183 = r357174 / r357182;
        double r357184 = r357183 * r357183;
        double r357185 = r357179 * r357175;
        double r357186 = r357185 / r357182;
        double r357187 = expm1(r357186);
        double r357188 = log1p(r357187);
        double r357189 = r357186 * r357188;
        double r357190 = r357184 - r357189;
        double r357191 = r357182 / r357175;
        double r357192 = r357179 / r357191;
        double r357193 = r357192 + r357183;
        double r357194 = r357190 / r357193;
        return r357194;
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program 15.5

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

  3. Applied flip--15.5

    \[\leadsto \color{blue}{\frac{1 \cdot 1 - \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 + \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}}}\]

  4. Simplified15.0

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

  5. Simplified15.0

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

  7. Applied div-sub15.0

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

  9. Applied flip--15.1

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

  10. Simplified15.1

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

  12. Applied log1p-expm1-u15.1

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

  13. Final simplification15.1

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

Reproduce

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