Given's Rotation SVD example, simplified

Average Error: 16.1 → 13.9

Time: 29.9s

Precision: 64

Math

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

↓

\[\begin{array}{l} \mathbf{if}\;x \le -2.803231780383790086224129762398904475162 \cdot 10^{-8}:\\ \;\;\;\;\left(\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5} \cdot \sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5} + \left(\sqrt{1} \cdot \sqrt{1} - \sqrt{1} \cdot \sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}\right)\right) \cdot \left(\frac{1}{\mathsf{fma}\left(\sqrt{1}, 1, {\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}\right)}^{3}\right)} - \frac{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}{\mathsf{fma}\left(\sqrt{1}, 1, {\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}\right)}^{3}\right)}\right)\right) \cdot \frac{1}{\sqrt{1}}\\ \mathbf{elif}\;x \le 8.055965450229694943973940413073364652519 \cdot 10^{-5}:\\ \;\;\;\;\left(\mathsf{fma}\left(\frac{\frac{x}{1} \cdot \frac{x}{\sqrt{1}}}{\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)}, 0.25, \mathsf{fma}\left(0.00390625, \frac{\sqrt{\frac{1}{{\left(\frac{0.5}{\sqrt{1}} + 0.5\right)}^{3}}} \cdot {x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2} \cdot {\left(\sqrt{1}\right)}^{5}}, \mathsf{fma}\left(\frac{\frac{{x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{3}}}{\left(\frac{0.5}{\sqrt{1}} + 0.5\right) \cdot \left(1 \cdot 1\right)}, 0.0078125, \frac{0.5}{\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)}\right)\right)\right) - \mathsf{fma}\left(\frac{\sqrt{\frac{1}{\frac{0.5}{\sqrt{1}} + 0.5}}}{{\left(\sqrt{1}\right)}^{3}} \cdot \frac{x \cdot x}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}}, 0.0625, \mathsf{fma}\left(0.0078125, \frac{\frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5} \cdot \left(\frac{0.5}{\sqrt{1}} + 0.5\right)}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{3}}, \mathsf{fma}\left(0.046875, \frac{{x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}} \cdot \frac{\sqrt{\frac{1}{\frac{0.5}{\sqrt{1}} + 0.5}}}{1 \cdot 1}, \mathsf{fma}\left(0.1875, \frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5} \cdot \mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)}, \mathsf{fma}\left(\frac{\frac{{x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}} \cdot 0.00390625}{{\left(\sqrt{1}\right)}^{6}}, \sqrt{\frac{1}{{\left(\frac{0.5}{\sqrt{1}} + 0.5\right)}^{3}}}, \frac{\frac{0.5}{\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)}}{\sqrt{1}}\right)\right)\right)\right)\right)\right) + \left(\frac{\frac{x \cdot x}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}}}{1} \cdot 0.0625 + 0.078125 \cdot \frac{\frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5}}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}}\right) \cdot \sqrt{\frac{1}{\frac{0.5}{\sqrt{1}} + 0.5}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{1}} \cdot \left(\frac{1}{\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5} + \sqrt{1}} - \frac{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5} + \sqrt{1}\right)\right)}\right)\\ \end{array}\]

C

double f(double x) {
        double r223606 = 1.0;
        double r223607 = 0.5;
        double r223608 = x;
        double r223609 = hypot(r223606, r223608);
        double r223610 = r223606 / r223609;
        double r223611 = r223606 + r223610;
        double r223612 = r223607 * r223611;
        double r223613 = sqrt(r223612);
        double r223614 = r223606 - r223613;
        return r223614;
}

↓

double f(double x) {
        double r223615 = x;
        double r223616 = -2.80323178038379e-08;
        bool r223617 = r223615 <= r223616;
        double r223618 = 0.5;
        double r223619 = 1.0;
        double r223620 = hypot(r223619, r223615);
        double r223621 = r223618 / r223620;
        double r223622 = r223621 + r223618;
        double r223623 = sqrt(r223622);
        double r223624 = r223623 * r223623;
        double r223625 = sqrt(r223619);
        double r223626 = r223625 * r223625;
        double r223627 = r223625 * r223623;
        double r223628 = r223626 - r223627;
        double r223629 = r223624 + r223628;
        double r223630 = 3.0;
        double r223631 = pow(r223623, r223630);
        double r223632 = fma(r223625, r223619, r223631);
        double r223633 = r223619 / r223632;
        double r223634 = r223622 / r223632;
        double r223635 = r223633 - r223634;
        double r223636 = r223629 * r223635;
        double r223637 = r223619 / r223625;
        double r223638 = r223636 * r223637;
        double r223639 = 8.055965450229695e-05;
        bool r223640 = r223615 <= r223639;
        double r223641 = r223615 / r223619;
        double r223642 = r223615 / r223625;
        double r223643 = r223641 * r223642;
        double r223644 = r223618 / r223625;
        double r223645 = r223644 + r223618;
        double r223646 = sqrt(r223645);
        double r223647 = fma(r223625, r223646, r223619);
        double r223648 = r223643 / r223647;
        double r223649 = 0.25;
        double r223650 = 0.00390625;
        double r223651 = 1.0;
        double r223652 = pow(r223645, r223630);
        double r223653 = r223651 / r223652;
        double r223654 = sqrt(r223653);
        double r223655 = 4.0;
        double r223656 = pow(r223615, r223655);
        double r223657 = r223654 * r223656;
        double r223658 = 2.0;
        double r223659 = pow(r223647, r223658);
        double r223660 = 5.0;
        double r223661 = pow(r223625, r223660);
        double r223662 = r223659 * r223661;
        double r223663 = r223657 / r223662;
        double r223664 = pow(r223647, r223630);
        double r223665 = r223656 / r223664;
        double r223666 = r223619 * r223619;
        double r223667 = r223645 * r223666;
        double r223668 = r223665 / r223667;
        double r223669 = 0.0078125;
        double r223670 = r223618 / r223647;
        double r223671 = fma(r223668, r223669, r223670);
        double r223672 = fma(r223650, r223663, r223671);
        double r223673 = fma(r223648, r223649, r223672);
        double r223674 = r223651 / r223645;
        double r223675 = sqrt(r223674);
        double r223676 = pow(r223625, r223630);
        double r223677 = r223675 / r223676;
        double r223678 = r223615 * r223615;
        double r223679 = r223678 / r223659;
        double r223680 = r223677 * r223679;
        double r223681 = 0.0625;
        double r223682 = r223661 * r223645;
        double r223683 = r223656 / r223682;
        double r223684 = r223683 / r223664;
        double r223685 = 0.046875;
        double r223686 = r223656 / r223659;
        double r223687 = r223675 / r223666;
        double r223688 = r223686 * r223687;
        double r223689 = 0.1875;
        double r223690 = r223661 * r223647;
        double r223691 = r223656 / r223690;
        double r223692 = r223686 * r223650;
        double r223693 = 6.0;
        double r223694 = pow(r223625, r223693);
        double r223695 = r223692 / r223694;
        double r223696 = r223670 / r223625;
        double r223697 = fma(r223695, r223654, r223696);
        double r223698 = fma(r223689, r223691, r223697);
        double r223699 = fma(r223685, r223688, r223698);
        double r223700 = fma(r223669, r223684, r223699);
        double r223701 = fma(r223680, r223681, r223700);
        double r223702 = r223673 - r223701;
        double r223703 = r223679 / r223619;
        double r223704 = r223703 * r223681;
        double r223705 = 0.078125;
        double r223706 = r223656 / r223661;
        double r223707 = r223706 / r223659;
        double r223708 = r223705 * r223707;
        double r223709 = r223704 + r223708;
        double r223710 = r223709 * r223675;
        double r223711 = r223702 + r223710;
        double r223712 = r223623 + r223625;
        double r223713 = r223619 / r223712;
        double r223714 = log1p(r223712);
        double r223715 = expm1(r223714);
        double r223716 = r223622 / r223715;
        double r223717 = r223713 - r223716;
        double r223718 = r223637 * r223717;
        double r223719 = r223640 ? r223711 : r223718;
        double r223720 = r223617 ? r223638 : r223719;
        return r223720;
}

Error

Bits error versus x

Derivation

1. Split input into 3 regimes

2. if x < -2.80323178038379e-08

   1. Initial program 1.5

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

   2. Simplified 1.5

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

   4. Applied flip-- 1.5

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

   5. Simplified 0.5

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

   6. Simplified 0.5

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

   8. Applied add-sqr-sqrt 0.5

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

   9. Applied sqrt-prod 0.5

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

   10. Applied distribute-lft-out 0.5

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

   11. Applied times-frac 0.5

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

   12. Simplified 0.5

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

   14. Applied div-sub 0.5

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

   15. Simplified 0.5

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

   16. Simplified 0.5

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

   18. Applied flip3-+ 1.5

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

   19. Applied associate-/r/ 0.6

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

   20. Applied flip3-+ 2.0

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

   21. Applied associate-/r/ 0.6

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

   22. Applied distribute-rgt-out-- 0.5

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

   23. Simplified 0.5

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

   if -2.80323178038379e-08 < x < 8.055965450229695e-05

   1. Initial program 31.4

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

   2. Simplified 31.4

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

   4. Applied flip-- 31.4

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

   5. Simplified 31.4

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

   6. Simplified 31.4

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

   7. Taylor expanded around 0 31.4

      \[\leadsto \color{blue}{\left(0.078125 \cdot \left(\frac{{x}^{4}}{{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right)}^{2} \cdot {\left(\sqrt{1}\right)}^{5}} \cdot \sqrt{\frac{1}{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5}}\right) + \left(0.0625 \cdot \left(\frac{{x}^{2}}{{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right)}^{2} \cdot {\left(\sqrt{1}\right)}^{2}} \cdot \sqrt{\frac{1}{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5}}\right) + \left(0.25 \cdot \frac{{x}^{2}}{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right) \cdot {\left(\sqrt{1}\right)}^{3}} + \left(0.00390625 \cdot \left(\frac{{x}^{4}}{{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right)}^{2} \cdot {\left(\sqrt{1}\right)}^{5}} \cdot \sqrt{\frac{1}{{\left(0.5 \cdot \frac{1}{\sqrt{1}} + 0.5\right)}^{3}}}\right) + \left(0.0078125 \cdot \frac{{x}^{4}}{{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right)}^{3} \cdot \left(\left(0.5 \cdot \frac{1}{\sqrt{1}} + 0.5\right) \cdot {\left(\sqrt{1}\right)}^{4}\right)} + 0.5 \cdot \frac{1}{\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1}\right)\right)\right)\right)\right) - \left(0.0625 \cdot \left(\frac{{x}^{2}}{{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right)}^{2} \cdot {\left(\sqrt{1}\right)}^{3}} \cdot \sqrt{\frac{1}{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5}}\right) + \left(0.0078125 \cdot \frac{{x}^{4}}{{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right)}^{3} \cdot \left(\left(0.5 \cdot \frac{1}{\sqrt{1}} + 0.5\right) \cdot {\left(\sqrt{1}\right)}^{5}\right)} + \left(0.046875 \cdot \left(\frac{{x}^{4}}{{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right)}^{2} \cdot {\left(\sqrt{1}\right)}^{4}} \cdot \sqrt{\frac{1}{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5}}\right) + \left(0.1875 \cdot \frac{{x}^{4}}{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right) \cdot {\left(\sqrt{1}\right)}^{5}} + \left(0.5 \cdot \frac{1}{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right) \cdot \sqrt{1}} + 0.00390625 \cdot \left(\frac{{x}^{4}}{{\left(\sqrt{1} \cdot \sqrt{0.5 \cdot \frac{1}{\sqrt{1}} + 0.5} + 1\right)}^{2} \cdot {\left(\sqrt{1}\right)}^{6}} \cdot \sqrt{\frac{1}{{\left(0.5 \cdot \frac{1}{\sqrt{1}} + 0.5\right)}^{3}}}\right)\right)\right)\right)\right)\right)}\]

   8. Simplified 27.9

      \[\leadsto \color{blue}{\sqrt{\frac{1}{0.5 + \frac{0.5}{\sqrt{1}}}} \cdot \left(0.078125 \cdot \frac{\frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5}}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)\right)}^{2}} + 0.0625 \cdot \frac{\frac{x \cdot x}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)\right)}^{2}}}{1}\right) + \left(\mathsf{fma}\left(\frac{\frac{x}{\sqrt{1}} \cdot \frac{x}{1}}{\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)}, 0.25, \mathsf{fma}\left(0.00390625, \frac{\sqrt{\frac{1}{{\left(0.5 + \frac{0.5}{\sqrt{1}}\right)}^{3}}} \cdot {x}^{4}}{{\left(\sqrt{1}\right)}^{5} \cdot {\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)\right)}^{2}}, \mathsf{fma}\left(\frac{\frac{{x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)\right)}^{3}}}{\left(0.5 + \frac{0.5}{\sqrt{1}}\right) \cdot \left(1 \cdot 1\right)}, 0.0078125, \frac{0.5}{\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)}\right)\right)\right) - \mathsf{fma}\left(\frac{x \cdot x}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)\right)}^{2}} \cdot \frac{\sqrt{\frac{1}{0.5 + \frac{0.5}{\sqrt{1}}}}}{{\left(\sqrt{1}\right)}^{3}}, 0.0625, \mathsf{fma}\left(0.0078125, \frac{\frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5} \cdot \left(0.5 + \frac{0.5}{\sqrt{1}}\right)}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)\right)}^{3}}, \mathsf{fma}\left(0.046875, \frac{{x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)\right)}^{2}} \cdot \frac{\sqrt{\frac{1}{0.5 + \frac{0.5}{\sqrt{1}}}}}{1 \cdot 1}, \mathsf{fma}\left(0.1875, \frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5} \cdot \mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)}, \mathsf{fma}\left(\frac{0.00390625 \cdot \frac{{x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)\right)}^{2}}}{{\left(\sqrt{1}\right)}^{6}}, \sqrt{\frac{1}{{\left(0.5 + \frac{0.5}{\sqrt{1}}\right)}^{3}}}, \frac{\frac{0.5}{\mathsf{fma}\left(\sqrt{1}, \sqrt{0.5 + \frac{0.5}{\sqrt{1}}}, 1\right)}}{\sqrt{1}}\right)\right)\right)\right)\right)\right)}\]

   if 8.055965450229695e-05 < x

   1. Initial program 1.1

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

   2. Simplified 1.1

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

   4. Applied flip-- 1.2

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

   5. Simplified 0.2

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

   6. Simplified 0.2

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

   8. Applied add-sqr-sqrt 0.2

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

   9. Applied sqrt-prod 0.2

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

   10. Applied distribute-lft-out 0.2

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

   11. Applied times-frac 0.2

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

   12. Simplified 0.2

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

   14. Applied div-sub 0.2

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

   15. Simplified 0.2

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

   16. Simplified 0.2

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

   18. Applied expm1-log1p-u 0.2

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

   19. Simplified 0.2

       \[\leadsto \frac{1}{\sqrt{1}} \cdot \left(\frac{1}{\sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}} + \sqrt{1}} - \frac{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}{\mathsf{expm1}\left(\color{blue}{\mathsf{log1p}\left(\sqrt{1} + \sqrt{0.5 + \frac{0.5}{\mathsf{hypot}\left(1, x\right)}}\right)}\right)}\right)\]
3. Recombined 3 regimes into one program.

4. Final simplification 13.9

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \le -2.803231780383790086224129762398904475162 \cdot 10^{-8}:\\ \;\;\;\;\left(\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5} \cdot \sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5} + \left(\sqrt{1} \cdot \sqrt{1} - \sqrt{1} \cdot \sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}\right)\right) \cdot \left(\frac{1}{\mathsf{fma}\left(\sqrt{1}, 1, {\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}\right)}^{3}\right)} - \frac{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}{\mathsf{fma}\left(\sqrt{1}, 1, {\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}\right)}^{3}\right)}\right)\right) \cdot \frac{1}{\sqrt{1}}\\ \mathbf{elif}\;x \le 8.055965450229694943973940413073364652519 \cdot 10^{-5}:\\ \;\;\;\;\left(\mathsf{fma}\left(\frac{\frac{x}{1} \cdot \frac{x}{\sqrt{1}}}{\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)}, 0.25, \mathsf{fma}\left(0.00390625, \frac{\sqrt{\frac{1}{{\left(\frac{0.5}{\sqrt{1}} + 0.5\right)}^{3}}} \cdot {x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2} \cdot {\left(\sqrt{1}\right)}^{5}}, \mathsf{fma}\left(\frac{\frac{{x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{3}}}{\left(\frac{0.5}{\sqrt{1}} + 0.5\right) \cdot \left(1 \cdot 1\right)}, 0.0078125, \frac{0.5}{\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)}\right)\right)\right) - \mathsf{fma}\left(\frac{\sqrt{\frac{1}{\frac{0.5}{\sqrt{1}} + 0.5}}}{{\left(\sqrt{1}\right)}^{3}} \cdot \frac{x \cdot x}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}}, 0.0625, \mathsf{fma}\left(0.0078125, \frac{\frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5} \cdot \left(\frac{0.5}{\sqrt{1}} + 0.5\right)}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{3}}, \mathsf{fma}\left(0.046875, \frac{{x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}} \cdot \frac{\sqrt{\frac{1}{\frac{0.5}{\sqrt{1}} + 0.5}}}{1 \cdot 1}, \mathsf{fma}\left(0.1875, \frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5} \cdot \mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)}, \mathsf{fma}\left(\frac{\frac{{x}^{4}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}} \cdot 0.00390625}{{\left(\sqrt{1}\right)}^{6}}, \sqrt{\frac{1}{{\left(\frac{0.5}{\sqrt{1}} + 0.5\right)}^{3}}}, \frac{\frac{0.5}{\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)}}{\sqrt{1}}\right)\right)\right)\right)\right)\right) + \left(\frac{\frac{x \cdot x}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}}}{1} \cdot 0.0625 + 0.078125 \cdot \frac{\frac{{x}^{4}}{{\left(\sqrt{1}\right)}^{5}}}{{\left(\mathsf{fma}\left(\sqrt{1}, \sqrt{\frac{0.5}{\sqrt{1}} + 0.5}, 1\right)\right)}^{2}}\right) \cdot \sqrt{\frac{1}{\frac{0.5}{\sqrt{1}} + 0.5}}\\ \mathbf{else}:\\ \;\;\;\;\frac{1}{\sqrt{1}} \cdot \left(\frac{1}{\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5} + \sqrt{1}} - \frac{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5}{\mathsf{expm1}\left(\mathsf{log1p}\left(\sqrt{\frac{0.5}{\mathsf{hypot}\left(1, x\right)} + 0.5} + \sqrt{1}\right)\right)}\right)\\ \end{array}\]

Reproduce

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