Given's Rotation SVD example, simplified

Average Error: 15.4 → 14.9

Time: 30.1s

Precision: 64

Math

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

↓

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

C

double f(double x) {
        double r10279001 = 1.0;
        double r10279002 = 0.5;
        double r10279003 = x;
        double r10279004 = hypot(r10279001, r10279003);
        double r10279005 = r10279001 / r10279004;
        double r10279006 = r10279001 + r10279005;
        double r10279007 = r10279002 * r10279006;
        double r10279008 = sqrt(r10279007);
        double r10279009 = r10279001 - r10279008;
        return r10279009;
}

↓

double f(double x) {
        double r10279010 = 1.0;
        double r10279011 = 0.5;
        double r10279012 = r10279010 * r10279011;
        double r10279013 = x;
        double r10279014 = hypot(r10279010, r10279013);
        double r10279015 = r10279012 / r10279014;
        double r10279016 = r10279015 + r10279012;
        double r10279017 = sqrt(r10279016);
        double r10279018 = r10279010 + r10279017;
        double r10279019 = r10279018 * r10279010;
        double r10279020 = r10279019 * r10279019;
        double r10279021 = r10279019 * r10279016;
        double r10279022 = r10279020 - r10279021;
        double r10279023 = r10279016 * r10279016;
        double r10279024 = r10279022 + r10279023;
        double r10279025 = r10279017 * r10279017;
        double r10279026 = r10279010 * r10279017;
        double r10279027 = r10279025 - r10279026;
        double r10279028 = r10279010 * r10279010;
        double r10279029 = r10279027 + r10279028;
        double r10279030 = 3.0;
        double r10279031 = pow(r10279029, r10279030);
        double r10279032 = r10279015 * r10279015;
        double r10279033 = r10279012 * r10279015;
        double r10279034 = r10279032 - r10279033;
        double r10279035 = r10279012 * r10279012;
        double r10279036 = r10279034 + r10279035;
        double r10279037 = pow(r10279036, r10279030);
        double r10279038 = r10279031 * r10279037;
        double r10279039 = r10279010 * r10279028;
        double r10279040 = r10279014 / r10279011;
        double r10279041 = r10279010 / r10279040;
        double r10279042 = r10279041 - r10279012;
        double r10279043 = r10279041 * r10279042;
        double r10279044 = r10279043 + r10279035;
        double r10279045 = r10279044 * r10279044;
        double r10279046 = r10279044 * r10279045;
        double r10279047 = r10279012 + r10279041;
        double r10279048 = sqrt(r10279047);
        double r10279049 = r10279048 * r10279047;
        double r10279050 = r10279049 + r10279039;
        double r10279051 = r10279050 * r10279050;
        double r10279052 = r10279050 * r10279051;
        double r10279053 = r10279052 * r10279039;
        double r10279054 = r10279046 * r10279053;
        double r10279055 = r10279028 + r10279047;
        double r10279056 = r10279010 * r10279048;
        double r10279057 = r10279055 - r10279056;
        double r10279058 = r10279057 * r10279057;
        double r10279059 = r10279057 * r10279058;
        double r10279060 = r10279014 * r10279014;
        double r10279061 = r10279012 / r10279060;
        double r10279062 = r10279035 / r10279014;
        double r10279063 = r10279061 * r10279062;
        double r10279064 = r10279035 * r10279012;
        double r10279065 = r10279063 + r10279064;
        double r10279066 = r10279065 * r10279065;
        double r10279067 = r10279066 * r10279065;
        double r10279068 = r10279059 * r10279067;
        double r10279069 = r10279054 + r10279068;
        double r10279070 = r10279039 / r10279069;
        double r10279071 = r10279049 / r10279069;
        double r10279072 = r10279070 - r10279071;
        double r10279073 = r10279038 * r10279072;
        double r10279074 = r10279024 * r10279073;
        return r10279074;
}

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 flip3-- 15.7

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

4. Simplified 15.4

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

5. Simplified 14.9

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

7. Applied div-sub 14.9

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

9. Applied flip3-+ 14.9

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

10. Applied associate-/r/ 15.4

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

11. Applied flip3-+ 15.4

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

12. Applied associate-/r/ 15.4

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

13. Applied distribute-rgt-out-- 15.4

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

15. Applied flip3-+ 14.9

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

16. Applied associate-*r/ 14.9

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

17. Applied cube-div 15.4

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

18. Applied flip3-+ 15.4

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

19. Applied cube-div 15.4

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

20. Applied frac-add 14.9

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

21. Applied associate-/r/ 15.4

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

22. Applied flip3-+ 15.9

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

23. Applied associate-*r/ 15.9

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

24. Applied cube-div 15.4

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

25. Applied flip3-+ 15.4

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

26. Applied cube-div 15.4

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

27. Applied frac-add 15.9

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

28. Applied associate-/r/ 15.9

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

29. Applied distribute-rgt-out-- 15.7

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

30. Simplified 14.9

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

31. Final simplification 14.9

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

Reproduce

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