Given's Rotation SVD example, simplified

Average Error: 15.7 → 15.2

Time: 46.6s

Precision: 64

Math

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

↓

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

C

double code(double x) {
	return (1.0 - sqrt((0.5 * (1.0 + (1.0 / hypot(1.0, x))))));
}

↓

double code(double x) {
	return (((((((1.0 * (pow(1.0, 3.0) - pow(0.5, 3.0))) * (1.0 * ((1.0 * 1.0) - (0.5 * 0.5)))) * hypot(1.0, x)) * ((((1.0 * 1.0) * (1.0 * 1.0)) + ((((0.5 * 0.5) + (1.0 * 0.5)) * ((0.5 * 0.5) + (1.0 * 0.5))) - ((1.0 * 1.0) * ((0.5 * 0.5) + (1.0 * 0.5))))) * (1.0 - 0.5))) - (1.0 * (((pow((1.0 * 1.0), 3.0) + pow(((0.5 * 0.5) + (1.0 * 0.5)), 3.0)) * ((1.0 * 1.0) - (0.5 * 0.5))) * ((0.5 * (1.0 / hypot(1.0, x))) * 0.5)))) / ((((1.0 + 0.5) * ((1.0 * 1.0) + ((0.5 * 0.5) + (1.0 * 0.5)))) * (hypot(1.0, x) / 1.0)) * (1.0 * ((((1.0 * 1.0) * (1.0 * 1.0)) + ((((0.5 * 0.5) + (1.0 * 0.5)) * ((0.5 * 0.5) + (1.0 * 0.5))) - ((1.0 * 1.0) * ((0.5 * 0.5) + (1.0 * 0.5))))) * (1.0 - 0.5))))) / ((1.0 + sqrt((0.5 * (1.0 + (1.0 / hypot(1.0, x)))))) * ((1.0 * (1.0 - 0.5)) + (0.5 * (1.0 / hypot(1.0, x))))));
}

Error

Bits error versus x

Derivation

1. Initial program 15.7

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

3. Applied flip-- 15.7

   \[\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. Simplified 15.2

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

6. Applied flip-- 15.2

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

7. Applied associate-/l/ 15.2

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

9. Applied clear-num 15.2

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

10. Applied un-div-inv 15.2

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

11. Applied associate-*r/ 15.2

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

12. Applied flip-- 15.2

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

13. Applied associate-*r/ 15.2

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

14. Applied flip3-- 15.2

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

15. Applied associate-*r/ 15.2

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

16. Applied frac-times 15.2

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

17. Applied frac-sub 15.2

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

18. Simplified 15.2

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

20. Applied flip-+ 15.2

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

21. Applied flip3-+ 15.2

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

22. Applied frac-times 15.2

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

23. Applied associate-*l/ 15.2

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

24. Applied associate-*r/ 15.2

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

25. Applied frac-sub 15.3

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

26. Applied associate-/l/ 15.2

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

27. Final simplification 15.2

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

Reproduce

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