Given's Rotation SVD example, simplified

Average Error: 15.4 → 15.1

Time: 11.9s

Precision: binary64

Math

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

↓

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

Error

Bits error versus x

Derivation

1. Initial program 15.4

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

3. Applied flip-- 15.4

   \[\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 14.9

   \[\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 associate-*r/ 14.9

   \[\leadsto \frac{1 \cdot \left(1 - 0.5\right) - \color{blue}{\frac{0.5 \cdot 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 flip-- 14.9

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

8. Applied associate-*r/ 14.9

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

9. Applied frac-sub 14.9

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

10. Simplified 14.9

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

12. Applied flip-+ 14.9

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

13. Applied associate-*r/ 14.9

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

14. Applied flip3-- 14.9

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

15. Applied associate-*l/ 15.1

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

16. Applied frac-sub 15.1

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

17. Simplified 15.1

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

18. Simplified 15.1

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

20. Applied flip3-- 15.1

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

21. Applied flip-- 15.1

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

22. Applied associate-*l/ 15.1

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

23. Applied frac-times 15.1

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

24. Applied flip3-- 15.1

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

25. Applied associate-*r/ 15.1

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

26. Applied associate-*r/ 15.1

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

27. Applied frac-add 15.1

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

28. Applied associate-/l/ 15.1

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

29. Simplified 15.1

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

30. Final simplification 15.1

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

Reproduce

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