Average Error: 30.7 → 0.5
Time: 4.2s
Precision: binary64
\[\sqrt{2 \cdot {x}^{2}}\]
↓
\[\sqrt{2} \cdot \left|{\left(\frac{1}{{\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1}}\right)}^{1}\right|\]

Error

Bits error versus x

Derivation

  1. Initial program 30.7

    \[\sqrt{2 \cdot {x}^{2}}\]
  2. Using strategy rm

  3. Applied pow1/230.7

    \[\leadsto \color{blue}{{\left(2 \cdot {x}^{2}\right)}^{\frac{1}{2}}}\]

  4. Taylor expanded around inf 49.0

    \[\leadsto \color{blue}{{\left(2 \cdot {\left(\frac{1}{{\left(e^{2 \cdot \left(\log \left(\frac{1}{x}\right) + \log 1\right)}\right)}^{1}}\right)}^{1}\right)}^{\frac{1}{2}}}\]

  5. Simplified31.3

    \[\leadsto \color{blue}{\sqrt{2 \cdot {\left(\frac{1}{{\left({x}^{\left(-2\right)}\right)}^{1}}\right)}^{1}}}\]
  6. Using strategy rm

  7. Applied sqrt-prod31.4

    \[\leadsto \color{blue}{\sqrt{2} \cdot \sqrt{{\left(\frac{1}{{\left({x}^{\left(-2\right)}\right)}^{1}}\right)}^{1}}}\]
  8. Using strategy rm

  9. Applied sqr-pow31.4

    \[\leadsto \sqrt{2} \cdot \sqrt{{\left(\frac{1}{{\color{blue}{\left({x}^{\left(\frac{-2}{2}\right)} \cdot {x}^{\left(\frac{-2}{2}\right)}\right)}}^{1}}\right)}^{1}}\]

  10. Applied unpow-prod-down31.4

    \[\leadsto \sqrt{2} \cdot \sqrt{{\left(\frac{1}{\color{blue}{{\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1} \cdot {\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1}}}\right)}^{1}}\]

  11. Applied *-un-lft-identity31.4

    \[\leadsto \sqrt{2} \cdot \sqrt{{\left(\frac{\color{blue}{1 \cdot 1}}{{\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1} \cdot {\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1}}\right)}^{1}}\]

  12. Applied times-frac30.9

    \[\leadsto \sqrt{2} \cdot \sqrt{{\color{blue}{\left(\frac{1}{{\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1}} \cdot \frac{1}{{\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1}}\right)}}^{1}}\]

  13. Applied unpow-prod-down30.9

    \[\leadsto \sqrt{2} \cdot \sqrt{\color{blue}{{\left(\frac{1}{{\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1}}\right)}^{1} \cdot {\left(\frac{1}{{\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1}}\right)}^{1}}}\]

  14. Applied rem-sqrt-square0.5

    \[\leadsto \sqrt{2} \cdot \color{blue}{\left|{\left(\frac{1}{{\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1}}\right)}^{1}\right|}\]

  15. Final simplification0.5

    \[\leadsto \sqrt{2} \cdot \left|{\left(\frac{1}{{\left({x}^{\left(\frac{-2}{2}\right)}\right)}^{1}}\right)}^{1}\right|\]

Reproduce

herbie shell --seed 2020182 
(FPCore (x)
  :name "sqrt D"
  :precision binary64
  (sqrt (* 2.0 (pow x 2.0))))