ENA, Section 1.4, Exercise 4b, n=5

1. Split input into 2 regimes

2. if (-.f64 (pow.f64 (+.f64 x eps) 5) (pow.f64 x 5)) < -2.0000000000019e-312 or 0.0 < (-.f64 (pow.f64 (+.f64 x eps) 5) (pow.f64 x 5))

   1. Initial program 97.7%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   if -2.0000000000019e-312 < (-.f64 (pow.f64 (+.f64 x eps) 5) (pow.f64 x 5)) < 0.0

   1. Initial program 86.1%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around inf 99.9%

      \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4}} \]
   3. Step-by-step derivation

      1. distribute-lft1-in99.9%

         \[\leadsto \color{blue}{\left(\left(4 + 1\right) \cdot \varepsilon\right)} \cdot {x}^{4} \]

      2. metadata-eval99.9%

         \[\leadsto \left(\color{blue}{5} \cdot \varepsilon\right) \cdot {x}^{4} \]

      3. associate-*l*99.9%

         \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]

   4. Simplified99.9%

      \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]
   5. Step-by-step derivation

      1. associate-*r*99.9%

         \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} \]

      2. *-commutative99.9%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} \]

      3. associate-*l*99.9%

         \[\leadsto \color{blue}{\varepsilon \cdot \left(5 \cdot {x}^{4}\right)} \]

      4. metadata-eval99.9%

         \[\leadsto \varepsilon \cdot \left(\color{blue}{\left(4 + 1\right)} \cdot {x}^{4}\right) \]

      5. distribute-lft1-in99.9%

         \[\leadsto \varepsilon \cdot \color{blue}{\left(4 \cdot {x}^{4} + {x}^{4}\right)} \]

      6. distribute-lft-in99.9%

         \[\leadsto \color{blue}{\varepsilon \cdot \left(4 \cdot {x}^{4}\right) + \varepsilon \cdot {x}^{4}} \]

      7. *-commutative99.9%

         \[\leadsto \color{blue}{\left(4 \cdot {x}^{4}\right) \cdot \varepsilon} + \varepsilon \cdot {x}^{4} \]

      8. *-commutative99.9%

         \[\leadsto \color{blue}{\left({x}^{4} \cdot 4\right)} \cdot \varepsilon + \varepsilon \cdot {x}^{4} \]

      9. associate-*l*99.9%

         \[\leadsto \color{blue}{{x}^{4} \cdot \left(4 \cdot \varepsilon\right)} + \varepsilon \cdot {x}^{4} \]

      10. fma-def99.9%

          \[\leadsto \color{blue}{\mathsf{fma}\left({x}^{4}, 4 \cdot \varepsilon, \varepsilon \cdot {x}^{4}\right)} \]

   6. Applied egg-rr99.9%

      \[\leadsto \color{blue}{\mathsf{fma}\left({x}^{4}, 4 \cdot \varepsilon, \varepsilon \cdot {x}^{4}\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification99.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;{\left(x + \varepsilon\right)}^{5} - {x}^{5} \leq -2 \cdot 10^{-312} \lor \neg \left({\left(x + \varepsilon\right)}^{5} - {x}^{5} \leq 0\right):\\ \;\;\;\;{\left(x + \varepsilon\right)}^{5} - {x}^{5}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left({x}^{4}, \varepsilon \cdot 4, \varepsilon \cdot {x}^{4}\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if (-.f64 (pow.f64 (+.f64 x eps) 5) (pow.f64 x 5)) < -2.0000000000019e-312 or 0.0 < (-.f64 (pow.f64 (+.f64 x eps) 5) (pow.f64 x 5))

   1. Initial program 97.7%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   if -2.0000000000019e-312 < (-.f64 (pow.f64 (+.f64 x eps) 5) (pow.f64 x 5)) < 0.0

   1. Initial program 86.1%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around inf 99.9%

      \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4} + \left(\left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]
   3. Step-by-step derivation

      1. fma-def99.9%

         \[\leadsto \color{blue}{\mathsf{fma}\left(4 \cdot \varepsilon + \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]

      2. distribute-lft1-in99.9%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\left(4 + 1\right) \cdot \varepsilon}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      3. metadata-eval99.9%

         \[\leadsto \mathsf{fma}\left(\color{blue}{5} \cdot \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      4. *-commutative99.9%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\varepsilon \cdot 5}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      5. +-commutative99.9%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}}\right) \]

      6. *-commutative99.9%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right)} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}\right) \]

      7. *-commutative99.9%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{3} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)}\right) \]

      8. unpow399.9%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      9. unpow299.9%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \left(\color{blue}{{x}^{2}} \cdot x\right) \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      10. associate-*l*99.9%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{2} \cdot \left(x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

      11. distribute-lft-out99.9%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

   4. Simplified99.9%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \left(x \cdot x\right) \cdot \left({\varepsilon}^{3} \cdot 10 + x \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)\right)\right)} \]

   5. Taylor expanded in eps around 0 99.9%

      \[\leadsto \color{blue}{10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + 5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]
   6. Step-by-step derivation

      1. +-commutative99.9%

         \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)} \]

      2. associate-*r*99.9%

         \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      3. *-commutative99.9%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      4. metadata-eval99.9%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot {x}^{\color{blue}{\left(2 \cdot 2\right)}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      5. pow-sqr99.9%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \color{blue}{\left({x}^{2} \cdot {x}^{2}\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      6. unpow299.9%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\color{blue}{\left(x \cdot x\right)} \cdot {x}^{2}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      7. unpow299.9%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\left(x \cdot x\right) \cdot \color{blue}{\left(x \cdot x\right)}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      8. associate-*l*99.9%

         \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot 5\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      9. associate-*l*99.9%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(5 \cdot \left(x \cdot x\right)\right)\right)} \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      10. *-commutative99.9%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot 5\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      11. associate-*r*99.9%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(x \cdot \left(x \cdot 5\right)\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      12. associate-*l*99.9%

          \[\leadsto \color{blue}{\varepsilon \cdot \left(\left(x \cdot \left(x \cdot 5\right)\right) \cdot \left(x \cdot x\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      13. *-commutative99.9%

          \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      14. associate-*l*99.9%

          \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      15. associate-*r*99.9%

          \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      16. unpow299.9%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + 10 \cdot \left(\color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot {x}^{3}\right) \]

      17. associate-*r*99.9%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(10 \cdot \left(\varepsilon \cdot \varepsilon\right)\right) \cdot {x}^{3}} \]

      18. *-commutative99.9%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot 10\right)} \cdot {x}^{3} \]

      19. associate-*r*99.9%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \cdot {x}^{3} \]

      20. *-commutative99.9%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{{x}^{3} \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \]

      21. associate-*r*99.9%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left({x}^{3} \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot 10\right)} \]

   7. Simplified99.9%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot {x}^{3}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right)} \]
   8. Step-by-step derivation

      1. unpow399.9%

         \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right) \]

   9. Applied egg-rr99.9%

      \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right) \]
3. Recombined 2 regimes into one program.

4. Final simplification99.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;{\left(x + \varepsilon\right)}^{5} - {x}^{5} \leq -2 \cdot 10^{-312} \lor \neg \left({\left(x + \varepsilon\right)}^{5} - {x}^{5} \leq 0\right):\\ \;\;\;\;{\left(x + \varepsilon\right)}^{5} - {x}^{5}\\ \mathbf{else}:\\ \;\;\;\;\left(\varepsilon \cdot \left(x \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot 5 + \varepsilon \cdot 10\right)\\ \end{array} \]

1. Split input into 3 regimes

2. if x < -1.3500000000000001e-63

   1. Initial program 67.4%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around inf 92.4%

      \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4} + \left(\left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]
   3. Step-by-step derivation

      1. fma-def92.4%

         \[\leadsto \color{blue}{\mathsf{fma}\left(4 \cdot \varepsilon + \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]

      2. distribute-lft1-in92.4%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\left(4 + 1\right) \cdot \varepsilon}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      3. metadata-eval92.4%

         \[\leadsto \mathsf{fma}\left(\color{blue}{5} \cdot \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      4. *-commutative92.4%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\varepsilon \cdot 5}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      5. +-commutative92.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}}\right) \]

      6. *-commutative92.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right)} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}\right) \]

      7. *-commutative92.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{3} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)}\right) \]

      8. unpow392.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      9. unpow292.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \left(\color{blue}{{x}^{2}} \cdot x\right) \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      10. associate-*l*92.4%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{2} \cdot \left(x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

      11. distribute-lft-out92.4%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

   4. Simplified92.4%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \left(x \cdot x\right) \cdot \left({\varepsilon}^{3} \cdot 10 + x \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)\right)\right)} \]

   5. Taylor expanded in eps around 0 92.2%

      \[\leadsto \color{blue}{10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + \left(5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right)\right)} \]
   6. Step-by-step derivation

      1. associate-+r+92.2%

         \[\leadsto \color{blue}{\left(10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + 5 \cdot \left(\varepsilon \cdot {x}^{4}\right)\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right)} \]

      2. +-commutative92.2%

         \[\leadsto \color{blue}{\left(5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)\right)} + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right) \]

      3. associate-*r*92.3%

         \[\leadsto \left(\color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right) \]

      4. *-commutative92.3%

         \[\leadsto \left(\color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right) \]

      5. *-commutative92.3%

         \[\leadsto \left(\color{blue}{{x}^{4} \cdot \left(\varepsilon \cdot 5\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)\right) + 10 \cdot \left({\varepsilon}^{3} \cdot {x}^{2}\right) \]

      6. unpow292.3%

         \[\leadsto \left({x}^{4} \cdot \left(\varepsilon \cdot 5\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)\right) + 10 \cdot \left({\varepsilon}^{3} \cdot \color{blue}{\left(x \cdot x\right)}\right) \]

      7. associate-*r*92.3%

         \[\leadsto \left({x}^{4} \cdot \left(\varepsilon \cdot 5\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)\right) + \color{blue}{\left(10 \cdot {\varepsilon}^{3}\right) \cdot \left(x \cdot x\right)} \]

      8. *-commutative92.3%

         \[\leadsto \left({x}^{4} \cdot \left(\varepsilon \cdot 5\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)\right) + \color{blue}{\left(x \cdot x\right) \cdot \left(10 \cdot {\varepsilon}^{3}\right)} \]

      9. associate-+r+92.3%

         \[\leadsto \color{blue}{{x}^{4} \cdot \left(\varepsilon \cdot 5\right) + \left(10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + \left(x \cdot x\right) \cdot \left(10 \cdot {\varepsilon}^{3}\right)\right)} \]

      10. *-commutative92.3%

          \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right) \cdot {x}^{4}} + \left(10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + \left(x \cdot x\right) \cdot \left(10 \cdot {\varepsilon}^{3}\right)\right) \]

      11. associate-*r*92.3%

          \[\leadsto \color{blue}{\varepsilon \cdot \left(5 \cdot {x}^{4}\right)} + \left(10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + \left(x \cdot x\right) \cdot \left(10 \cdot {\varepsilon}^{3}\right)\right) \]

   7. Simplified92.4%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\varepsilon, 5 \cdot {x}^{4}, \left(10 \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right)\right)\right) \cdot \left(x \cdot x\right)\right)} \]
   8. Step-by-step derivation

      1. fma-udef92.4%

         \[\leadsto \color{blue}{\varepsilon \cdot \left(5 \cdot {x}^{4}\right) + \left(10 \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right)\right)\right) \cdot \left(x \cdot x\right)} \]

      2. associate-*l*92.3%

         \[\leadsto \varepsilon \cdot \left(5 \cdot {x}^{4}\right) + \color{blue}{10 \cdot \left(\left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\varepsilon + x\right)\right) \cdot \left(x \cdot x\right)\right)} \]

      3. associate-*l*92.3%

         \[\leadsto \varepsilon \cdot \left(5 \cdot {x}^{4}\right) + 10 \cdot \color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\left(\varepsilon + x\right) \cdot \left(x \cdot x\right)\right)\right)} \]

   9. Applied egg-rr92.3%

      \[\leadsto \color{blue}{\varepsilon \cdot \left(5 \cdot {x}^{4}\right) + 10 \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\left(\varepsilon + x\right) \cdot \left(x \cdot x\right)\right)\right)} \]

   if -1.3500000000000001e-63 < x < 1.25e-63

   1. Initial program 100.0%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around 0 99.8%

      \[\leadsto \color{blue}{{\varepsilon}^{5}} \]

   if 1.25e-63 < x

   1. Initial program 35.6%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around inf 99.5%

      \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4} + \left(\left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]
   3. Step-by-step derivation

      1. fma-def99.5%

         \[\leadsto \color{blue}{\mathsf{fma}\left(4 \cdot \varepsilon + \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]

      2. distribute-lft1-in99.5%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\left(4 + 1\right) \cdot \varepsilon}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      3. metadata-eval99.5%

         \[\leadsto \mathsf{fma}\left(\color{blue}{5} \cdot \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      4. *-commutative99.5%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\varepsilon \cdot 5}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      5. +-commutative99.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}}\right) \]

      6. *-commutative99.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right)} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}\right) \]

      7. *-commutative99.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{3} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)}\right) \]

      8. unpow399.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      9. unpow299.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \left(\color{blue}{{x}^{2}} \cdot x\right) \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      10. associate-*l*99.5%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{2} \cdot \left(x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

      11. distribute-lft-out99.5%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

   4. Simplified99.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \left(x \cdot x\right) \cdot \left({\varepsilon}^{3} \cdot 10 + x \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)\right)\right)} \]

   5. Taylor expanded in eps around 0 99.5%

      \[\leadsto \color{blue}{10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + 5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]
   6. Step-by-step derivation

      1. +-commutative99.5%

         \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)} \]

      2. associate-*r*99.5%

         \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      3. *-commutative99.5%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      4. metadata-eval99.5%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot {x}^{\color{blue}{\left(2 \cdot 2\right)}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      5. pow-sqr99.6%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \color{blue}{\left({x}^{2} \cdot {x}^{2}\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      6. unpow299.6%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\color{blue}{\left(x \cdot x\right)} \cdot {x}^{2}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      7. unpow299.6%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\left(x \cdot x\right) \cdot \color{blue}{\left(x \cdot x\right)}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      8. associate-*l*99.5%

         \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot 5\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      9. associate-*l*99.4%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(5 \cdot \left(x \cdot x\right)\right)\right)} \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      10. *-commutative99.4%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot 5\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      11. associate-*r*99.6%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(x \cdot \left(x \cdot 5\right)\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      12. associate-*l*99.6%

          \[\leadsto \color{blue}{\varepsilon \cdot \left(\left(x \cdot \left(x \cdot 5\right)\right) \cdot \left(x \cdot x\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      13. *-commutative99.6%

          \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      14. associate-*l*99.3%

          \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      15. associate-*r*99.4%

          \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      16. unpow299.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + 10 \cdot \left(\color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot {x}^{3}\right) \]

      17. associate-*r*99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(10 \cdot \left(\varepsilon \cdot \varepsilon\right)\right) \cdot {x}^{3}} \]

      18. *-commutative99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot 10\right)} \cdot {x}^{3} \]

      19. associate-*r*99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \cdot {x}^{3} \]

      20. *-commutative99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{{x}^{3} \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \]

      21. associate-*r*99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left({x}^{3} \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot 10\right)} \]

   7. Simplified99.6%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot {x}^{3}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right)} \]
3. Recombined 3 regimes into one program.

4. Final simplification99.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1.35 \cdot 10^{-63}:\\ \;\;\;\;\varepsilon \cdot \left(5 \cdot {x}^{4}\right) + 10 \cdot \left(\left(\varepsilon \cdot \varepsilon\right) \cdot \left(\left(x + \varepsilon\right) \cdot \left(x \cdot x\right)\right)\right)\\ \mathbf{elif}\;x \leq 1.25 \cdot 10^{-63}:\\ \;\;\;\;{\varepsilon}^{5}\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 5 + \varepsilon \cdot 10\right) \cdot \left(\varepsilon \cdot {x}^{3}\right)\\ \end{array} \]

1. Split input into 3 regimes

2. if x < -1.3500000000000001e-63

   1. Initial program 67.4%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around inf 92.4%

      \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4} + \left(\left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]
   3. Step-by-step derivation

      1. fma-def92.4%

         \[\leadsto \color{blue}{\mathsf{fma}\left(4 \cdot \varepsilon + \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]

      2. distribute-lft1-in92.4%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\left(4 + 1\right) \cdot \varepsilon}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      3. metadata-eval92.4%

         \[\leadsto \mathsf{fma}\left(\color{blue}{5} \cdot \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      4. *-commutative92.4%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\varepsilon \cdot 5}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      5. +-commutative92.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}}\right) \]

      6. *-commutative92.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right)} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}\right) \]

      7. *-commutative92.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{3} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)}\right) \]

      8. unpow392.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      9. unpow292.4%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \left(\color{blue}{{x}^{2}} \cdot x\right) \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      10. associate-*l*92.4%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{2} \cdot \left(x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

      11. distribute-lft-out92.4%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

   4. Simplified92.4%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \left(x \cdot x\right) \cdot \left({\varepsilon}^{3} \cdot 10 + x \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)\right)\right)} \]

   5. Taylor expanded in eps around 0 91.8%

      \[\leadsto \color{blue}{10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + 5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]
   6. Step-by-step derivation

      1. +-commutative91.8%

         \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)} \]

      2. associate-*r*92.0%

         \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      3. *-commutative92.0%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      4. metadata-eval92.0%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot {x}^{\color{blue}{\left(2 \cdot 2\right)}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      5. pow-sqr92.0%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \color{blue}{\left({x}^{2} \cdot {x}^{2}\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      6. unpow292.0%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\color{blue}{\left(x \cdot x\right)} \cdot {x}^{2}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      7. unpow292.0%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\left(x \cdot x\right) \cdot \color{blue}{\left(x \cdot x\right)}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      8. associate-*l*92.1%

         \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot 5\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      9. associate-*l*92.0%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(5 \cdot \left(x \cdot x\right)\right)\right)} \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      10. *-commutative92.0%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot 5\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      11. associate-*r*92.0%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(x \cdot \left(x \cdot 5\right)\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      12. associate-*l*92.1%

          \[\leadsto \color{blue}{\varepsilon \cdot \left(\left(x \cdot \left(x \cdot 5\right)\right) \cdot \left(x \cdot x\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      13. *-commutative92.1%

          \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      14. associate-*l*92.0%

          \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      15. associate-*r*92.0%

          \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      16. unpow292.0%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + 10 \cdot \left(\color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot {x}^{3}\right) \]

      17. associate-*r*92.0%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(10 \cdot \left(\varepsilon \cdot \varepsilon\right)\right) \cdot {x}^{3}} \]

      18. *-commutative92.0%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot 10\right)} \cdot {x}^{3} \]

      19. associate-*r*92.0%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \cdot {x}^{3} \]

      20. *-commutative92.0%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{{x}^{3} \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \]

      21. associate-*r*92.0%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left({x}^{3} \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot 10\right)} \]

   7. Simplified92.1%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot {x}^{3}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right)} \]
   8. Step-by-step derivation

      1. unpow392.2%

         \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right) \]

   9. Applied egg-rr92.2%

      \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right) \]

   if -1.3500000000000001e-63 < x < 1.25000000000000008e-64

   1. Initial program 100.0%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around 0 99.8%

      \[\leadsto \color{blue}{{\varepsilon}^{5}} \]

   if 1.25000000000000008e-64 < x

   1. Initial program 35.6%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around inf 99.5%

      \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4} + \left(\left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]
   3. Step-by-step derivation

      1. fma-def99.5%

         \[\leadsto \color{blue}{\mathsf{fma}\left(4 \cdot \varepsilon + \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]

      2. distribute-lft1-in99.5%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\left(4 + 1\right) \cdot \varepsilon}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      3. metadata-eval99.5%

         \[\leadsto \mathsf{fma}\left(\color{blue}{5} \cdot \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      4. *-commutative99.5%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\varepsilon \cdot 5}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      5. +-commutative99.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}}\right) \]

      6. *-commutative99.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right)} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}\right) \]

      7. *-commutative99.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{3} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)}\right) \]

      8. unpow399.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      9. unpow299.5%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \left(\color{blue}{{x}^{2}} \cdot x\right) \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      10. associate-*l*99.5%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{2} \cdot \left(x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

      11. distribute-lft-out99.5%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

   4. Simplified99.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \left(x \cdot x\right) \cdot \left({\varepsilon}^{3} \cdot 10 + x \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)\right)\right)} \]

   5. Taylor expanded in eps around 0 99.5%

      \[\leadsto \color{blue}{10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + 5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]
   6. Step-by-step derivation

      1. +-commutative99.5%

         \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)} \]

      2. associate-*r*99.5%

         \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      3. *-commutative99.5%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      4. metadata-eval99.5%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot {x}^{\color{blue}{\left(2 \cdot 2\right)}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      5. pow-sqr99.6%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \color{blue}{\left({x}^{2} \cdot {x}^{2}\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      6. unpow299.6%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\color{blue}{\left(x \cdot x\right)} \cdot {x}^{2}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      7. unpow299.6%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\left(x \cdot x\right) \cdot \color{blue}{\left(x \cdot x\right)}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      8. associate-*l*99.5%

         \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot 5\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      9. associate-*l*99.4%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(5 \cdot \left(x \cdot x\right)\right)\right)} \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      10. *-commutative99.4%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot 5\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      11. associate-*r*99.6%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(x \cdot \left(x \cdot 5\right)\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      12. associate-*l*99.6%

          \[\leadsto \color{blue}{\varepsilon \cdot \left(\left(x \cdot \left(x \cdot 5\right)\right) \cdot \left(x \cdot x\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      13. *-commutative99.6%

          \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      14. associate-*l*99.3%

          \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      15. associate-*r*99.4%

          \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      16. unpow299.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + 10 \cdot \left(\color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot {x}^{3}\right) \]

      17. associate-*r*99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(10 \cdot \left(\varepsilon \cdot \varepsilon\right)\right) \cdot {x}^{3}} \]

      18. *-commutative99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot 10\right)} \cdot {x}^{3} \]

      19. associate-*r*99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \cdot {x}^{3} \]

      20. *-commutative99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{{x}^{3} \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \]

      21. associate-*r*99.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left({x}^{3} \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot 10\right)} \]

   7. Simplified99.6%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot {x}^{3}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right)} \]
3. Recombined 3 regimes into one program.

4. Final simplification99.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1.35 \cdot 10^{-63}:\\ \;\;\;\;\left(\varepsilon \cdot \left(x \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot 5 + \varepsilon \cdot 10\right)\\ \mathbf{elif}\;x \leq 1.25 \cdot 10^{-64}:\\ \;\;\;\;{\varepsilon}^{5}\\ \mathbf{else}:\\ \;\;\;\;\left(x \cdot 5 + \varepsilon \cdot 10\right) \cdot \left(\varepsilon \cdot {x}^{3}\right)\\ \end{array} \]

1. Split input into 2 regimes

2. if x < -1.3500000000000001e-63 or 1.25e-63 < x

   1. Initial program 48.2%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around inf 96.7%

      \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4} + \left(\left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]
   3. Step-by-step derivation

      1. fma-def96.7%

         \[\leadsto \color{blue}{\mathsf{fma}\left(4 \cdot \varepsilon + \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]

      2. distribute-lft1-in96.7%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\left(4 + 1\right) \cdot \varepsilon}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      3. metadata-eval96.7%

         \[\leadsto \mathsf{fma}\left(\color{blue}{5} \cdot \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      4. *-commutative96.7%

         \[\leadsto \mathsf{fma}\left(\color{blue}{\varepsilon \cdot 5}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

      5. +-commutative96.7%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}}\right) \]

      6. *-commutative96.7%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right)} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}\right) \]

      7. *-commutative96.7%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{3} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)}\right) \]

      8. unpow396.7%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      9. unpow296.7%

         \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \left(\color{blue}{{x}^{2}} \cdot x\right) \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

      10. associate-*l*96.7%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{2} \cdot \left(x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

      11. distribute-lft-out96.7%

          \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

   4. Simplified96.7%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \left(x \cdot x\right) \cdot \left({\varepsilon}^{3} \cdot 10 + x \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)\right)\right)} \]

   5. Taylor expanded in eps around 0 96.4%

      \[\leadsto \color{blue}{10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + 5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]
   6. Step-by-step derivation

      1. +-commutative96.4%

         \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)} \]

      2. associate-*r*96.5%

         \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      3. *-commutative96.5%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      4. metadata-eval96.5%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot {x}^{\color{blue}{\left(2 \cdot 2\right)}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      5. pow-sqr96.6%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \color{blue}{\left({x}^{2} \cdot {x}^{2}\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      6. unpow296.6%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\color{blue}{\left(x \cdot x\right)} \cdot {x}^{2}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      7. unpow296.6%

         \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\left(x \cdot x\right) \cdot \color{blue}{\left(x \cdot x\right)}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      8. associate-*l*96.6%

         \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot 5\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      9. associate-*l*96.5%

         \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(5 \cdot \left(x \cdot x\right)\right)\right)} \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      10. *-commutative96.5%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot 5\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      11. associate-*r*96.6%

          \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(x \cdot \left(x \cdot 5\right)\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      12. associate-*l*96.6%

          \[\leadsto \color{blue}{\varepsilon \cdot \left(\left(x \cdot \left(x \cdot 5\right)\right) \cdot \left(x \cdot x\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      13. *-commutative96.6%

          \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      14. associate-*l*96.4%

          \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      15. associate-*r*96.4%

          \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

      16. unpow296.4%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + 10 \cdot \left(\color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot {x}^{3}\right) \]

      17. associate-*r*96.5%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(10 \cdot \left(\varepsilon \cdot \varepsilon\right)\right) \cdot {x}^{3}} \]

      18. *-commutative96.5%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot 10\right)} \cdot {x}^{3} \]

      19. associate-*r*96.5%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \cdot {x}^{3} \]

      20. *-commutative96.5%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{{x}^{3} \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \]

      21. associate-*r*96.5%

          \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left({x}^{3} \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot 10\right)} \]

   7. Simplified96.6%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot {x}^{3}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right)} \]
   8. Step-by-step derivation

      1. unpow396.6%

         \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right) \]

   9. Applied egg-rr96.6%

      \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right) \]

   if -1.3500000000000001e-63 < x < 1.25e-63

   1. Initial program 100.0%

      \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

   2. Taylor expanded in x around 0 99.8%

      \[\leadsto \color{blue}{{\varepsilon}^{5}} \]
3. Recombined 2 regimes into one program.

4. Final simplification99.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1.35 \cdot 10^{-63} \lor \neg \left(x \leq 1.25 \cdot 10^{-63}\right):\\ \;\;\;\;\left(\varepsilon \cdot \left(x \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot 5 + \varepsilon \cdot 10\right)\\ \mathbf{else}:\\ \;\;\;\;{\varepsilon}^{5}\\ \end{array} \]

1. Initial program 88.3%

   \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

2. Taylor expanded in x around inf 84.0%

   \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4} + \left(\left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]
3. Step-by-step derivation

   1. fma-def84.0%

      \[\leadsto \color{blue}{\mathsf{fma}\left(4 \cdot \varepsilon + \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right)} \]

   2. distribute-lft1-in84.0%

      \[\leadsto \mathsf{fma}\left(\color{blue}{\left(4 + 1\right) \cdot \varepsilon}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

   3. metadata-eval84.0%

      \[\leadsto \mathsf{fma}\left(\color{blue}{5} \cdot \varepsilon, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

   4. *-commutative84.0%

      \[\leadsto \mathsf{fma}\left(\color{blue}{\varepsilon \cdot 5}, {x}^{4}, \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3} + \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2}\right) \]

   5. +-commutative84.0%

      \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) \cdot {x}^{2} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}}\right) \]

   6. *-commutative84.0%

      \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right)} + \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right) \cdot {x}^{3}\right) \]

   7. *-commutative84.0%

      \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{3} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)}\right) \]

   8. unpow384.0%

      \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)} \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

   9. unpow284.0%

      \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \left(\color{blue}{{x}^{2}} \cdot x\right) \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right) \]

   10. associate-*l*84.0%

       \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, {x}^{2} \cdot \left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + \color{blue}{{x}^{2} \cdot \left(x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

   11. distribute-lft-out84.0%

       \[\leadsto \mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \color{blue}{{x}^{2} \cdot \left(\left(\left(2 \cdot {\varepsilon}^{2} + 4 \cdot {\varepsilon}^{2}\right) \cdot \varepsilon + 4 \cdot {\varepsilon}^{3}\right) + x \cdot \left(2 \cdot {\varepsilon}^{2} + 8 \cdot {\varepsilon}^{2}\right)\right)}\right) \]

4. Simplified84.0%

   \[\leadsto \color{blue}{\mathsf{fma}\left(\varepsilon \cdot 5, {x}^{4}, \left(x \cdot x\right) \cdot \left({\varepsilon}^{3} \cdot 10 + x \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)\right)\right)} \]

5. Taylor expanded in eps around 0 84.0%

   \[\leadsto \color{blue}{10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) + 5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]
6. Step-by-step derivation

   1. +-commutative84.0%

      \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right)} \]

   2. associate-*r*84.0%

      \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   3. *-commutative84.0%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   4. metadata-eval84.0%

      \[\leadsto \left(\varepsilon \cdot 5\right) \cdot {x}^{\color{blue}{\left(2 \cdot 2\right)}} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   5. pow-sqr84.0%

      \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \color{blue}{\left({x}^{2} \cdot {x}^{2}\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   6. unpow284.0%

      \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\color{blue}{\left(x \cdot x\right)} \cdot {x}^{2}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   7. unpow284.0%

      \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\left(x \cdot x\right) \cdot \color{blue}{\left(x \cdot x\right)}\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   8. associate-*l*84.0%

      \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot 5\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   9. associate-*l*84.0%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(5 \cdot \left(x \cdot x\right)\right)\right)} \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   10. *-commutative84.0%

       \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot 5\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   11. associate-*r*84.0%

       \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(x \cdot \left(x \cdot 5\right)\right)}\right) \cdot \left(x \cdot x\right) + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   12. associate-*l*84.0%

       \[\leadsto \color{blue}{\varepsilon \cdot \left(\left(x \cdot \left(x \cdot 5\right)\right) \cdot \left(x \cdot x\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   13. *-commutative84.0%

       \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   14. associate-*l*84.0%

       \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot \left(x \cdot 5\right)\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   15. associate-*r*84.0%

       \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right)} + 10 \cdot \left({\varepsilon}^{2} \cdot {x}^{3}\right) \]

   16. unpow284.0%

       \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + 10 \cdot \left(\color{blue}{\left(\varepsilon \cdot \varepsilon\right)} \cdot {x}^{3}\right) \]

   17. associate-*r*84.0%

       \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(10 \cdot \left(\varepsilon \cdot \varepsilon\right)\right) \cdot {x}^{3}} \]

   18. *-commutative84.0%

       \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\left(\varepsilon \cdot \varepsilon\right) \cdot 10\right)} \cdot {x}^{3} \]

   19. associate-*r*84.0%

       \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \cdot {x}^{3} \]

   20. *-commutative84.0%

       \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{{x}^{3} \cdot \left(\varepsilon \cdot \left(\varepsilon \cdot 10\right)\right)} \]

   21. associate-*r*84.0%

       \[\leadsto \left(\left(\varepsilon \cdot \left(x \cdot x\right)\right) \cdot x\right) \cdot \left(x \cdot 5\right) + \color{blue}{\left({x}^{3} \cdot \varepsilon\right) \cdot \left(\varepsilon \cdot 10\right)} \]

7. Simplified84.0%

   \[\leadsto \color{blue}{\left(\varepsilon \cdot {x}^{3}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right)} \]
8. Step-by-step derivation

   1. unpow384.0%

      \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right) \]

9. Applied egg-rr84.0%

   \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot x\right)}\right) \cdot \left(x \cdot 5 + 10 \cdot \varepsilon\right) \]

10. Final simplification84.0%

    \[\leadsto \left(\varepsilon \cdot \left(x \cdot \left(x \cdot x\right)\right)\right) \cdot \left(x \cdot 5 + \varepsilon \cdot 10\right) \]

1. Initial program 88.3%

   \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

2. Taylor expanded in eps around 0 83.8%

   \[\leadsto \color{blue}{\varepsilon \cdot \left(4 \cdot {x}^{4} + {x}^{4}\right)} \]
3. Step-by-step derivation

   1. distribute-lft1-in83.8%

      \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(4 + 1\right) \cdot {x}^{4}\right)} \]

   2. metadata-eval83.8%

      \[\leadsto \varepsilon \cdot \left(\color{blue}{5} \cdot {x}^{4}\right) \]

   3. *-commutative83.8%

      \[\leadsto \varepsilon \cdot \color{blue}{\left({x}^{4} \cdot 5\right)} \]

   4. sqr-pow83.8%

      \[\leadsto \varepsilon \cdot \left(\color{blue}{\left({x}^{\left(\frac{4}{2}\right)} \cdot {x}^{\left(\frac{4}{2}\right)}\right)} \cdot 5\right) \]

   5. associate-*l*83.8%

      \[\leadsto \varepsilon \cdot \color{blue}{\left({x}^{\left(\frac{4}{2}\right)} \cdot \left({x}^{\left(\frac{4}{2}\right)} \cdot 5\right)\right)} \]

   6. metadata-eval83.8%

      \[\leadsto \varepsilon \cdot \left({x}^{\color{blue}{2}} \cdot \left({x}^{\left(\frac{4}{2}\right)} \cdot 5\right)\right) \]

   7. pow283.8%

      \[\leadsto \varepsilon \cdot \left(\color{blue}{\left(x \cdot x\right)} \cdot \left({x}^{\left(\frac{4}{2}\right)} \cdot 5\right)\right) \]

   8. metadata-eval83.8%

      \[\leadsto \varepsilon \cdot \left(\left(x \cdot x\right) \cdot \left({x}^{\color{blue}{2}} \cdot 5\right)\right) \]

   9. pow283.8%

      \[\leadsto \varepsilon \cdot \left(\left(x \cdot x\right) \cdot \left(\color{blue}{\left(x \cdot x\right)} \cdot 5\right)\right) \]

4. Applied egg-rr83.8%

   \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 5\right)\right)} \]

5. Final simplification83.8%

   \[\leadsto \varepsilon \cdot \left(\left(x \cdot x\right) \cdot \left(5 \cdot \left(x \cdot x\right)\right)\right) \]

1. Initial program 88.3%

   \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

2. Taylor expanded in x around inf 83.8%

   \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4}} \]
3. Step-by-step derivation

   1. distribute-lft1-in83.8%

      \[\leadsto \color{blue}{\left(\left(4 + 1\right) \cdot \varepsilon\right)} \cdot {x}^{4} \]

   2. metadata-eval83.8%

      \[\leadsto \left(\color{blue}{5} \cdot \varepsilon\right) \cdot {x}^{4} \]

   3. associate-*l*83.8%

      \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]

4. Simplified83.8%

   \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]
5. Step-by-step derivation

   1. associate-*r*83.8%

      \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} \]

   2. *-commutative83.8%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} \]

   3. add-sqr-sqrt78.3%

      \[\leadsto \color{blue}{\sqrt{\left(\varepsilon \cdot 5\right) \cdot {x}^{4}} \cdot \sqrt{\left(\varepsilon \cdot 5\right) \cdot {x}^{4}}} \]

   4. pow278.3%

      \[\leadsto \color{blue}{{\left(\sqrt{\left(\varepsilon \cdot 5\right) \cdot {x}^{4}}\right)}^{2}} \]

   5. sqrt-prod42.2%

      \[\leadsto {\color{blue}{\left(\sqrt{\varepsilon \cdot 5} \cdot \sqrt{{x}^{4}}\right)}}^{2} \]

   6. *-commutative42.2%

      \[\leadsto {\left(\sqrt{\color{blue}{5 \cdot \varepsilon}} \cdot \sqrt{{x}^{4}}\right)}^{2} \]

   7. sqrt-pow142.2%

      \[\leadsto {\left(\sqrt{5 \cdot \varepsilon} \cdot \color{blue}{{x}^{\left(\frac{4}{2}\right)}}\right)}^{2} \]

   8. metadata-eval42.2%

      \[\leadsto {\left(\sqrt{5 \cdot \varepsilon} \cdot {x}^{\color{blue}{2}}\right)}^{2} \]

   9. pow242.2%

      \[\leadsto {\left(\sqrt{5 \cdot \varepsilon} \cdot \color{blue}{\left(x \cdot x\right)}\right)}^{2} \]

6. Applied egg-rr42.2%

   \[\leadsto \color{blue}{{\left(\sqrt{5 \cdot \varepsilon} \cdot \left(x \cdot x\right)\right)}^{2}} \]
7. Step-by-step derivation

   1. unpow242.2%

      \[\leadsto \color{blue}{\left(\sqrt{5 \cdot \varepsilon} \cdot \left(x \cdot x\right)\right) \cdot \left(\sqrt{5 \cdot \varepsilon} \cdot \left(x \cdot x\right)\right)} \]

   2. swap-sqr42.2%

      \[\leadsto \color{blue}{\left(\sqrt{5 \cdot \varepsilon} \cdot \sqrt{5 \cdot \varepsilon}\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)} \]

   3. add-sqr-sqrt83.8%

      \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right)} \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \]

   4. *-commutative83.8%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \]

   5. pow283.8%

      \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left(\color{blue}{{x}^{2}} \cdot \left(x \cdot x\right)\right) \]

   6. pow283.8%

      \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \left({x}^{2} \cdot \color{blue}{{x}^{2}}\right) \]

   7. pow-prod-up83.8%

      \[\leadsto \left(\varepsilon \cdot 5\right) \cdot \color{blue}{{x}^{\left(2 + 2\right)}} \]

   8. metadata-eval83.8%

      \[\leadsto \left(\varepsilon \cdot 5\right) \cdot {x}^{\color{blue}{4}} \]

   9. associate-*r*83.8%

      \[\leadsto \color{blue}{\varepsilon \cdot \left(5 \cdot {x}^{4}\right)} \]

   10. *-commutative83.8%

       \[\leadsto \varepsilon \cdot \color{blue}{\left({x}^{4} \cdot 5\right)} \]

   11. metadata-eval83.8%

       \[\leadsto \varepsilon \cdot \left({x}^{\color{blue}{\left(2 + 2\right)}} \cdot 5\right) \]

   12. pow-prod-up83.8%

       \[\leadsto \varepsilon \cdot \left(\color{blue}{\left({x}^{2} \cdot {x}^{2}\right)} \cdot 5\right) \]

   13. pow283.8%

       \[\leadsto \varepsilon \cdot \left(\left(\color{blue}{\left(x \cdot x\right)} \cdot {x}^{2}\right) \cdot 5\right) \]

   14. pow283.8%

       \[\leadsto \varepsilon \cdot \left(\left(\left(x \cdot x\right) \cdot \color{blue}{\left(x \cdot x\right)}\right) \cdot 5\right) \]

   15. associate-*r*83.8%

       \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot 5\right)\right)} \]

   16. *-commutative83.8%

       \[\leadsto \varepsilon \cdot \color{blue}{\left(\left(\left(x \cdot x\right) \cdot 5\right) \cdot \left(x \cdot x\right)\right)} \]

   17. associate-*r*83.8%

       \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(\left(x \cdot x\right) \cdot 5\right)\right) \cdot \left(x \cdot x\right)} \]

   18. associate-*l*83.8%

       \[\leadsto \left(\varepsilon \cdot \color{blue}{\left(x \cdot \left(x \cdot 5\right)\right)}\right) \cdot \left(x \cdot x\right) \]

8. Applied egg-rr83.8%

   \[\leadsto \color{blue}{\left(\varepsilon \cdot \left(x \cdot \left(x \cdot 5\right)\right)\right) \cdot \left(x \cdot x\right)} \]

9. Final simplification83.8%

   \[\leadsto \left(x \cdot x\right) \cdot \left(\varepsilon \cdot \left(x \cdot \left(x \cdot 5\right)\right)\right) \]

1. Initial program 88.3%

   \[{\left(x + \varepsilon\right)}^{5} - {x}^{5} \]

2. Taylor expanded in x around inf 83.8%

   \[\leadsto \color{blue}{\left(4 \cdot \varepsilon + \varepsilon\right) \cdot {x}^{4}} \]
3. Step-by-step derivation

   1. distribute-lft1-in83.8%

      \[\leadsto \color{blue}{\left(\left(4 + 1\right) \cdot \varepsilon\right)} \cdot {x}^{4} \]

   2. metadata-eval83.8%

      \[\leadsto \left(\color{blue}{5} \cdot \varepsilon\right) \cdot {x}^{4} \]

   3. associate-*l*83.8%

      \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]

4. Simplified83.8%

   \[\leadsto \color{blue}{5 \cdot \left(\varepsilon \cdot {x}^{4}\right)} \]
5. Step-by-step derivation

   1. associate-*r*83.8%

      \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right) \cdot {x}^{4}} \]

   2. *-commutative83.8%

      \[\leadsto \color{blue}{\left(\varepsilon \cdot 5\right)} \cdot {x}^{4} \]

   3. add-sqr-sqrt78.3%

      \[\leadsto \color{blue}{\sqrt{\left(\varepsilon \cdot 5\right) \cdot {x}^{4}} \cdot \sqrt{\left(\varepsilon \cdot 5\right) \cdot {x}^{4}}} \]

   4. pow278.3%

      \[\leadsto \color{blue}{{\left(\sqrt{\left(\varepsilon \cdot 5\right) \cdot {x}^{4}}\right)}^{2}} \]

   5. sqrt-prod42.2%

      \[\leadsto {\color{blue}{\left(\sqrt{\varepsilon \cdot 5} \cdot \sqrt{{x}^{4}}\right)}}^{2} \]

   6. *-commutative42.2%

      \[\leadsto {\left(\sqrt{\color{blue}{5 \cdot \varepsilon}} \cdot \sqrt{{x}^{4}}\right)}^{2} \]

   7. sqrt-pow142.2%

      \[\leadsto {\left(\sqrt{5 \cdot \varepsilon} \cdot \color{blue}{{x}^{\left(\frac{4}{2}\right)}}\right)}^{2} \]

   8. metadata-eval42.2%

      \[\leadsto {\left(\sqrt{5 \cdot \varepsilon} \cdot {x}^{\color{blue}{2}}\right)}^{2} \]

   9. pow242.2%

      \[\leadsto {\left(\sqrt{5 \cdot \varepsilon} \cdot \color{blue}{\left(x \cdot x\right)}\right)}^{2} \]

6. Applied egg-rr42.2%

   \[\leadsto \color{blue}{{\left(\sqrt{5 \cdot \varepsilon} \cdot \left(x \cdot x\right)\right)}^{2}} \]
7. Step-by-step derivation

   1. unpow242.2%

      \[\leadsto \color{blue}{\left(\sqrt{5 \cdot \varepsilon} \cdot \left(x \cdot x\right)\right) \cdot \left(\sqrt{5 \cdot \varepsilon} \cdot \left(x \cdot x\right)\right)} \]

   2. swap-sqr42.2%

      \[\leadsto \color{blue}{\left(\sqrt{5 \cdot \varepsilon} \cdot \sqrt{5 \cdot \varepsilon}\right) \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right)} \]

   3. add-sqr-sqrt83.8%

      \[\leadsto \color{blue}{\left(5 \cdot \varepsilon\right)} \cdot \left(\left(x \cdot x\right) \cdot \left(x \cdot x\right)\right) \]

   4. associate-*r*83.8%

      \[\leadsto \color{blue}{\left(\left(5 \cdot \varepsilon\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)} \]

   5. *-commutative83.8%

      \[\leadsto \left(\color{blue}{\left(\varepsilon \cdot 5\right)} \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right) \]

8. Applied egg-rr83.8%

   \[\leadsto \color{blue}{\left(\left(\varepsilon \cdot 5\right) \cdot \left(x \cdot x\right)\right) \cdot \left(x \cdot x\right)} \]

9. Final simplification83.8%

   \[\leadsto \left(x \cdot x\right) \cdot \left(\left(x \cdot x\right) \cdot \left(\varepsilon \cdot 5\right)\right) \]

herbie shell --seed 2023166 
(FPCore (x eps)
  :name "ENA, Section 1.4, Exercise 4b, n=5"
  :precision binary64
  :pre (and (and (<= -1000000000.0 x) (<= x 1000000000.0)) (and (<= -1.0 eps) (<= eps 1.0)))
  (- (pow (+ x eps) 5.0) (pow x 5.0)))