Average Error: 15.6 → 15.4
Time: 13.3s
Precision: binary64
\[1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}\]
↓
\[\frac{1 \cdot \frac{\frac{\mathsf{hypot}\left(1, x\right) \cdot \left(\left(\left({\left({1}^{6}\right)}^{3} - {\left({0.5}^{6}\right)}^{3}\right) \cdot \left({1}^{4} + 0.5 \cdot \left(\left(0.5 - 1\right) \cdot \left(0.5 \cdot \left(1 - 0.5\right)\right)\right)\right)\right) \cdot \left({1}^{8} + \left({0.5}^{4} + 1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right)\right) \cdot \left({0.5}^{4} + \left(1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right) - {1}^{4}\right)\right)\right)\right) + \left({1}^{12} + \left({0.5}^{12} + {1}^{6} \cdot {0.5}^{6}\right)\right) \cdot \left(\left(0.5 \cdot \left(\left({1}^{3} + {0.5}^{3}\right) \cdot \left({1}^{12} + {\left({0.5}^{4} + 1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right)\right)}^{3}\right)\right)\right) \cdot \left(0.5 \cdot \left(0.5 - 1\right) - 1 \cdot 1\right)\right)}{\left({1}^{8} + \left({0.5}^{4} + 1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right)\right) \cdot \left({0.5}^{4} + \left(1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right) - {1}^{4}\right)\right)\right) \cdot \left(\left({1}^{12} + \left({0.5}^{12} + {1}^{6} \cdot {0.5}^{6}\right)\right) \cdot \left(1 \cdot 1 + 0.5 \cdot \left(1 - 0.5\right)\right)\right)}}{\left(0.5 \cdot \left(0.5 - 1\right) + 1 \cdot 1\right) \cdot \left({1}^{4} + \left({0.5}^{4} + 1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right)\right)\right)}}{\mathsf{hypot}\left(1, x\right) \cdot \left(\left(1 + 0.5\right) \cdot \left(1 + \sqrt{1 \cdot \left(0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right)}\right)\right)}\]
1 - \sqrt{0.5 \cdot \left(1 + \frac{1}{\mathsf{hypot}\left(1, x\right)}\right)}
↓
\frac{1 \cdot \frac{\frac{\mathsf{hypot}\left(1, x\right) \cdot \left(\left(\left({\left({1}^{6}\right)}^{3} - {\left({0.5}^{6}\right)}^{3}\right) \cdot \left({1}^{4} + 0.5 \cdot \left(\left(0.5 - 1\right) \cdot \left(0.5 \cdot \left(1 - 0.5\right)\right)\right)\right)\right) \cdot \left({1}^{8} + \left({0.5}^{4} + 1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right)\right) \cdot \left({0.5}^{4} + \left(1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right) - {1}^{4}\right)\right)\right)\right) + \left({1}^{12} + \left({0.5}^{12} + {1}^{6} \cdot {0.5}^{6}\right)\right) \cdot \left(\left(0.5 \cdot \left(\left({1}^{3} + {0.5}^{3}\right) \cdot \left({1}^{12} + {\left({0.5}^{4} + 1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right)\right)}^{3}\right)\right)\right) \cdot \left(0.5 \cdot \left(0.5 - 1\right) - 1 \cdot 1\right)\right)}{\left({1}^{8} + \left({0.5}^{4} + 1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right)\right) \cdot \left({0.5}^{4} + \left(1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right) - {1}^{4}\right)\right)\right) \cdot \left(\left({1}^{12} + \left({0.5}^{12} + {1}^{6} \cdot {0.5}^{6}\right)\right) \cdot \left(1 \cdot 1 + 0.5 \cdot \left(1 - 0.5\right)\right)\right)}}{\left(0.5 \cdot \left(0.5 - 1\right) + 1 \cdot 1\right) \cdot \left({1}^{4} + \left({0.5}^{4} + 1 \cdot \left(1 \cdot \left(0.5 \cdot 0.5\right)\right)\right)\right)}}{\mathsf{hypot}\left(1, x\right) \cdot \left(\left(1 + 0.5\right) \cdot \left(1 + \sqrt{1 \cdot \left(0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}\right)}\right)\right)}
(FPCore (x)
 :precision binary64
 (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))
↓
(FPCore (x)
 :precision binary64
 (/
  (*
   1.0
   (/
    (/
     (+
      (*
       (hypot 1.0 x)
       (*
        (*
         (- (pow (pow 1.0 6.0) 3.0) (pow (pow 0.5 6.0) 3.0))
         (+ (pow 1.0 4.0) (* 0.5 (* (- 0.5 1.0) (* 0.5 (- 1.0 0.5))))))
        (+
         (pow 1.0 8.0)
         (*
          (+ (pow 0.5 4.0) (* 1.0 (* 1.0 (* 0.5 0.5))))
          (+ (pow 0.5 4.0) (- (* 1.0 (* 1.0 (* 0.5 0.5))) (pow 1.0 4.0)))))))
      (*
       (+ (pow 1.0 12.0) (+ (pow 0.5 12.0) (* (pow 1.0 6.0) (pow 0.5 6.0))))
       (*
        (*
         0.5
         (*
          (+ (pow 1.0 3.0) (pow 0.5 3.0))
          (+
           (pow 1.0 12.0)
           (pow (+ (pow 0.5 4.0) (* 1.0 (* 1.0 (* 0.5 0.5)))) 3.0))))
        (- (* 0.5 (- 0.5 1.0)) (* 1.0 1.0)))))
     (*
      (+
       (pow 1.0 8.0)
       (*
        (+ (pow 0.5 4.0) (* 1.0 (* 1.0 (* 0.5 0.5))))
        (+ (pow 0.5 4.0) (- (* 1.0 (* 1.0 (* 0.5 0.5))) (pow 1.0 4.0)))))
      (*
       (+ (pow 1.0 12.0) (+ (pow 0.5 12.0) (* (pow 1.0 6.0) (pow 0.5 6.0))))
       (+ (* 1.0 1.0) (* 0.5 (- 1.0 0.5))))))
    (*
     (+ (* 0.5 (- 0.5 1.0)) (* 1.0 1.0))
     (+ (pow 1.0 4.0) (+ (pow 0.5 4.0) (* 1.0 (* 1.0 (* 0.5 0.5))))))))
  (*
   (hypot 1.0 x)
   (* (+ 1.0 0.5) (+ 1.0 (sqrt (* 1.0 (+ 0.5 (/ 0.5 (hypot 1.0 x))))))))))
double code(double x) {
	return ((double) (1.0 - ((double) sqrt(((double) (0.5 * ((double) (1.0 + (1.0 / ((double) hypot(1.0, x)))))))))));
}
↓
double code(double x) {
	return (((double) (1.0 * ((((double) (((double) (((double) hypot(1.0, x)) * ((double) (((double) (((double) (((double) pow(((double) pow(1.0, 6.0)), 3.0)) - ((double) pow(((double) pow(0.5, 6.0)), 3.0)))) * ((double) (((double) pow(1.0, 4.0)) + ((double) (0.5 * ((double) (((double) (0.5 - 1.0)) * ((double) (0.5 * ((double) (1.0 - 0.5)))))))))))) * ((double) (((double) pow(1.0, 8.0)) + ((double) (((double) (((double) pow(0.5, 4.0)) + ((double) (1.0 * ((double) (1.0 * ((double) (0.5 * 0.5)))))))) * ((double) (((double) pow(0.5, 4.0)) + ((double) (((double) (1.0 * ((double) (1.0 * ((double) (0.5 * 0.5)))))) - ((double) pow(1.0, 4.0)))))))))))))) + ((double) (((double) (((double) pow(1.0, 12.0)) + ((double) (((double) pow(0.5, 12.0)) + ((double) (((double) pow(1.0, 6.0)) * ((double) pow(0.5, 6.0)))))))) * ((double) (((double) (0.5 * ((double) (((double) (((double) pow(1.0, 3.0)) + ((double) pow(0.5, 3.0)))) * ((double) (((double) pow(1.0, 12.0)) + ((double) pow(((double) (((double) pow(0.5, 4.0)) + ((double) (1.0 * ((double) (1.0 * ((double) (0.5 * 0.5)))))))), 3.0)))))))) * ((double) (((double) (0.5 * ((double) (0.5 - 1.0)))) - ((double) (1.0 * 1.0)))))))))) / ((double) (((double) (((double) pow(1.0, 8.0)) + ((double) (((double) (((double) pow(0.5, 4.0)) + ((double) (1.0 * ((double) (1.0 * ((double) (0.5 * 0.5)))))))) * ((double) (((double) pow(0.5, 4.0)) + ((double) (((double) (1.0 * ((double) (1.0 * ((double) (0.5 * 0.5)))))) - ((double) pow(1.0, 4.0)))))))))) * ((double) (((double) (((double) pow(1.0, 12.0)) + ((double) (((double) pow(0.5, 12.0)) + ((double) (((double) pow(1.0, 6.0)) * ((double) pow(0.5, 6.0)))))))) * ((double) (((double) (1.0 * 1.0)) + ((double) (0.5 * ((double) (1.0 - 0.5))))))))))) / ((double) (((double) (((double) (0.5 * ((double) (0.5 - 1.0)))) + ((double) (1.0 * 1.0)))) * ((double) (((double) pow(1.0, 4.0)) + ((double) (((double) pow(0.5, 4.0)) + ((double) (1.0 * ((double) (1.0 * ((double) (0.5 * 0.5))))))))))))))) / ((double) (((double) hypot(1.0, x)) * ((double) (((double) (1.0 + 0.5)) * ((double) (1.0 + ((double) sqrt(((double) (1.0 * ((double) (0.5 + (0.5 / ((double) hypot(1.0, x))))))))))))))));
}

Error

Bits error versus x

Try it out

Your Program's Arguments

Results

Enter valid numbers for all inputs

Derivation

  1. Initial program Error: 15.6 bits

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

  3. Applied flip--Error: 15.6 bits

    \[\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. SimplifiedError: 15.1 bits

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

  5. SimplifiedError: 15.1 bits

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

  7. Applied flip--Error: 15.1 bits

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

  8. Applied frac-subError: 15.1 bits

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

  9. Applied associate-*r/Error: 15.1 bits

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

  10. Applied associate-/l/Error: 15.1 bits

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

  11. SimplifiedError: 15.4 bits

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

  13. Applied flip3-+Error: 15.4 bits

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

  14. Applied associate-*l/Error: 15.4 bits

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

  15. Applied flip3--Error: 15.4 bits

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

  16. Applied associate-*l/Error: 15.4 bits

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

  17. Applied frac-subError: 15.4 bits

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

  18. SimplifiedError: 15.4 bits

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

  19. SimplifiedError: 15.4 bits

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

  21. Applied flip3-+Error: 15.4 bits

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

  22. Applied associate-*l/Error: 15.4 bits

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

  23. Applied associate-*r/Error: 15.4 bits

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

  24. Applied flip-+Error: 15.4 bits

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

  25. Applied flip3--Error: 15.4 bits

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

  26. Applied frac-timesError: 15.4 bits

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

  27. Applied associate-*r/Error: 15.4 bits

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

  28. Applied frac-subError: 15.4 bits

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

  29. SimplifiedError: 15.4 bits

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

  30. SimplifiedError: 15.4 bits

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

  31. Final simplificationError: 15.4 bits

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

Reproduce

herbie shell --seed 2020203 
(FPCore (x)
  :name "Given's Rotation SVD example, simplified"
  :precision binary64
  (- 1.0 (sqrt (* 0.5 (+ 1.0 (/ 1.0 (hypot 1.0 x)))))))