2frac (problem 3.3.1)

1. Initial program 80.5%

   \[\frac{1}{x + 1} - \frac{1}{x} \]
2. Step-by-step derivation

   1. frac-sub81.9%

      \[\leadsto \color{blue}{\frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\left(x + 1\right) \cdot x}} \]

   2. div-inv81.9%

      \[\leadsto \color{blue}{\left(1 \cdot x - \left(x + 1\right) \cdot 1\right) \cdot \frac{1}{\left(x + 1\right) \cdot x}} \]

   3. *-un-lft-identity81.9%

      \[\leadsto \left(\color{blue}{x} - \left(x + 1\right) \cdot 1\right) \cdot \frac{1}{\left(x + 1\right) \cdot x} \]

   4. *-rgt-identity81.9%

      \[\leadsto \left(x - \color{blue}{\left(x + 1\right)}\right) \cdot \frac{1}{\left(x + 1\right) \cdot x} \]

   5. +-commutative81.9%

      \[\leadsto \left(x - \color{blue}{\left(1 + x\right)}\right) \cdot \frac{1}{\left(x + 1\right) \cdot x} \]

   6. metadata-eval81.9%

      \[\leadsto \left(x - \left(1 + x\right)\right) \cdot \frac{\color{blue}{1 \cdot 1}}{\left(x + 1\right) \cdot x} \]

   7. frac-times81.9%

      \[\leadsto \left(x - \left(1 + x\right)\right) \cdot \color{blue}{\left(\frac{1}{x + 1} \cdot \frac{1}{x}\right)} \]

   8. clear-num81.9%

      \[\leadsto \left(x - \left(1 + x\right)\right) \cdot \left(\color{blue}{\frac{1}{\frac{x + 1}{1}}} \cdot \frac{1}{x}\right) \]

   9. associate-*l/81.9%

      \[\leadsto \left(x - \left(1 + x\right)\right) \cdot \color{blue}{\frac{1 \cdot \frac{1}{x}}{\frac{x + 1}{1}}} \]

   10. *-un-lft-identity81.9%

       \[\leadsto \left(x - \left(1 + x\right)\right) \cdot \frac{\color{blue}{\frac{1}{x}}}{\frac{x + 1}{1}} \]

   11. div-inv81.9%

       \[\leadsto \left(x - \left(1 + x\right)\right) \cdot \frac{\frac{1}{x}}{\color{blue}{\left(x + 1\right) \cdot \frac{1}{1}}} \]

   12. metadata-eval81.9%

       \[\leadsto \left(x - \left(1 + x\right)\right) \cdot \frac{\frac{1}{x}}{\left(x + 1\right) \cdot \color{blue}{1}} \]

   13. *-rgt-identity81.9%

       \[\leadsto \left(x - \left(1 + x\right)\right) \cdot \frac{\frac{1}{x}}{\color{blue}{x + 1}} \]

   14. +-commutative81.9%

       \[\leadsto \left(x - \left(1 + x\right)\right) \cdot \frac{\frac{1}{x}}{\color{blue}{1 + x}} \]

3. Applied egg-rr81.9%

   \[\leadsto \color{blue}{\left(x - \left(1 + x\right)\right) \cdot \frac{\frac{1}{x}}{1 + x}} \]

4. Taylor expanded in x around 0 99.9%

   \[\leadsto \color{blue}{-1} \cdot \frac{\frac{1}{x}}{1 + x} \]

5. Final simplification99.9%

   \[\leadsto \frac{\frac{-1}{x}}{1 + x} \]

1. Split input into 2 regimes

2. if x < -1 or 0.76000000000000001 < x

   1. Initial program 60.0%

      \[\frac{1}{x + 1} - \frac{1}{x} \]

   2. Taylor expanded in x around inf 96.5%

      \[\leadsto \color{blue}{\frac{-1}{{x}^{2}}} \]
   3. Step-by-step derivation

      1. unpow296.5%

         \[\leadsto \frac{-1}{\color{blue}{x \cdot x}} \]

   4. Simplified96.5%

      \[\leadsto \color{blue}{\frac{-1}{x \cdot x}} \]

   if -1 < x < 0.76000000000000001

   1. Initial program 100.0%

      \[\frac{1}{x + 1} - \frac{1}{x} \]

   2. Taylor expanded in x around 0 98.4%

      \[\leadsto \color{blue}{1 - \frac{1}{x}} \]
3. Recombined 2 regimes into one program.

4. Final simplification97.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq -1 \lor \neg \left(x \leq 0.76\right):\\ \;\;\;\;\frac{-1}{x \cdot x}\\ \mathbf{else}:\\ \;\;\;\;1 + \frac{-1}{x}\\ \end{array} \]

1. Initial program 80.5%

   \[\frac{1}{x + 1} - \frac{1}{x} \]
2. Step-by-step derivation

   1. sub-neg80.5%

      \[\leadsto \color{blue}{\frac{1}{x + 1} + \left(-\frac{1}{x}\right)} \]

   2. +-commutative80.5%

      \[\leadsto \frac{1}{\color{blue}{1 + x}} + \left(-\frac{1}{x}\right) \]

   3. distribute-neg-frac80.5%

      \[\leadsto \frac{1}{1 + x} + \color{blue}{\frac{-1}{x}} \]

   4. metadata-eval80.5%

      \[\leadsto \frac{1}{1 + x} + \frac{\color{blue}{-1}}{x} \]

3. Applied egg-rr80.5%

   \[\leadsto \color{blue}{\frac{1}{1 + x} + \frac{-1}{x}} \]
4. Step-by-step derivation

   1. +-commutative80.5%

      \[\leadsto \color{blue}{\frac{-1}{x} + \frac{1}{1 + x}} \]

   2. *-rgt-identity80.5%

      \[\leadsto \color{blue}{\frac{-1}{x} \cdot 1} + \frac{1}{1 + x} \]

   3. associate-*l/80.5%

      \[\leadsto \color{blue}{\frac{-1 \cdot 1}{x}} + \frac{1}{1 + x} \]

   4. associate-*r/80.5%

      \[\leadsto \color{blue}{-1 \cdot \frac{1}{x}} + \frac{1}{1 + x} \]

   5. neg-mul-180.5%

      \[\leadsto \color{blue}{\left(-\frac{1}{x}\right)} + \frac{1}{1 + x} \]

   6. neg-sub080.5%

      \[\leadsto \color{blue}{\left(0 - \frac{1}{x}\right)} + \frac{1}{1 + x} \]

   7. associate-+l-80.5%

      \[\leadsto \color{blue}{0 - \left(\frac{1}{x} - \frac{1}{1 + x}\right)} \]

   8. sub0-neg80.5%

      \[\leadsto \color{blue}{-\left(\frac{1}{x} - \frac{1}{1 + x}\right)} \]

   9. sub-neg80.5%

      \[\leadsto -\color{blue}{\left(\frac{1}{x} + \left(-\frac{1}{1 + x}\right)\right)} \]

   10. distribute-neg-out80.5%

       \[\leadsto \color{blue}{\left(-\frac{1}{x}\right) + \left(-\left(-\frac{1}{1 + x}\right)\right)} \]

   11. distribute-neg-frac80.5%

       \[\leadsto \color{blue}{\frac{-1}{x}} + \left(-\left(-\frac{1}{1 + x}\right)\right) \]

   12. metadata-eval80.5%

       \[\leadsto \frac{\color{blue}{-1}}{x} + \left(-\left(-\frac{1}{1 + x}\right)\right) \]

   13. remove-double-neg80.5%

       \[\leadsto \frac{-1}{x} + \color{blue}{\frac{1}{1 + x}} \]

   14. remove-double-neg80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{\color{blue}{-\left(-\left(1 + x\right)\right)}} \]

   15. +-commutative80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\left(-\color{blue}{\left(x + 1\right)}\right)} \]

   16. distribute-neg-in80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\color{blue}{\left(\left(-x\right) + \left(-1\right)\right)}} \]

   17. neg-mul-180.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\left(\color{blue}{-1 \cdot x} + \left(-1\right)\right)} \]

   18. metadata-eval80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\left(-1 \cdot x + \color{blue}{-1}\right)} \]

   19. fma-udef80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\color{blue}{\mathsf{fma}\left(-1, x, -1\right)}} \]

   20. neg-mul-180.5%

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

   21. associate-/r*80.5%

       \[\leadsto \frac{-1}{x} + \color{blue}{\frac{\frac{1}{-1}}{\mathsf{fma}\left(-1, x, -1\right)}} \]

   22. metadata-eval80.5%

       \[\leadsto \frac{-1}{x} + \frac{\color{blue}{-1}}{\mathsf{fma}\left(-1, x, -1\right)} \]

   23. metadata-eval80.5%

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

   24. associate-*r/80.5%

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

5. Simplified99.6%

   \[\leadsto \color{blue}{\frac{-1}{x \cdot \left(x + 1\right)}} \]

6. Final simplification99.6%

   \[\leadsto \frac{-1}{x \cdot \left(1 + x\right)} \]

1. Initial program 80.5%

   \[\frac{1}{x + 1} - \frac{1}{x} \]
2. Step-by-step derivation

   1. sub-neg80.5%

      \[\leadsto \color{blue}{\frac{1}{x + 1} + \left(-\frac{1}{x}\right)} \]

   2. +-commutative80.5%

      \[\leadsto \frac{1}{\color{blue}{1 + x}} + \left(-\frac{1}{x}\right) \]

   3. distribute-neg-frac80.5%

      \[\leadsto \frac{1}{1 + x} + \color{blue}{\frac{-1}{x}} \]

   4. metadata-eval80.5%

      \[\leadsto \frac{1}{1 + x} + \frac{\color{blue}{-1}}{x} \]

3. Applied egg-rr80.5%

   \[\leadsto \color{blue}{\frac{1}{1 + x} + \frac{-1}{x}} \]
4. Step-by-step derivation

   1. +-commutative80.5%

      \[\leadsto \color{blue}{\frac{-1}{x} + \frac{1}{1 + x}} \]

   2. *-rgt-identity80.5%

      \[\leadsto \color{blue}{\frac{-1}{x} \cdot 1} + \frac{1}{1 + x} \]

   3. associate-*l/80.5%

      \[\leadsto \color{blue}{\frac{-1 \cdot 1}{x}} + \frac{1}{1 + x} \]

   4. associate-*r/80.5%

      \[\leadsto \color{blue}{-1 \cdot \frac{1}{x}} + \frac{1}{1 + x} \]

   5. neg-mul-180.5%

      \[\leadsto \color{blue}{\left(-\frac{1}{x}\right)} + \frac{1}{1 + x} \]

   6. neg-sub080.5%

      \[\leadsto \color{blue}{\left(0 - \frac{1}{x}\right)} + \frac{1}{1 + x} \]

   7. associate-+l-80.5%

      \[\leadsto \color{blue}{0 - \left(\frac{1}{x} - \frac{1}{1 + x}\right)} \]

   8. sub0-neg80.5%

      \[\leadsto \color{blue}{-\left(\frac{1}{x} - \frac{1}{1 + x}\right)} \]

   9. sub-neg80.5%

      \[\leadsto -\color{blue}{\left(\frac{1}{x} + \left(-\frac{1}{1 + x}\right)\right)} \]

   10. distribute-neg-out80.5%

       \[\leadsto \color{blue}{\left(-\frac{1}{x}\right) + \left(-\left(-\frac{1}{1 + x}\right)\right)} \]

   11. distribute-neg-frac80.5%

       \[\leadsto \color{blue}{\frac{-1}{x}} + \left(-\left(-\frac{1}{1 + x}\right)\right) \]

   12. metadata-eval80.5%

       \[\leadsto \frac{\color{blue}{-1}}{x} + \left(-\left(-\frac{1}{1 + x}\right)\right) \]

   13. remove-double-neg80.5%

       \[\leadsto \frac{-1}{x} + \color{blue}{\frac{1}{1 + x}} \]

   14. remove-double-neg80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{\color{blue}{-\left(-\left(1 + x\right)\right)}} \]

   15. +-commutative80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\left(-\color{blue}{\left(x + 1\right)}\right)} \]

   16. distribute-neg-in80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\color{blue}{\left(\left(-x\right) + \left(-1\right)\right)}} \]

   17. neg-mul-180.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\left(\color{blue}{-1 \cdot x} + \left(-1\right)\right)} \]

   18. metadata-eval80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\left(-1 \cdot x + \color{blue}{-1}\right)} \]

   19. fma-udef80.5%

       \[\leadsto \frac{-1}{x} + \frac{1}{-\color{blue}{\mathsf{fma}\left(-1, x, -1\right)}} \]

   20. neg-mul-180.5%

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

   21. associate-/r*80.5%

       \[\leadsto \frac{-1}{x} + \color{blue}{\frac{\frac{1}{-1}}{\mathsf{fma}\left(-1, x, -1\right)}} \]

   22. metadata-eval80.5%

       \[\leadsto \frac{-1}{x} + \frac{\color{blue}{-1}}{\mathsf{fma}\left(-1, x, -1\right)} \]

   23. metadata-eval80.5%

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

   24. associate-*r/80.5%

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

5. Simplified99.6%

   \[\leadsto \color{blue}{\frac{-1}{x \cdot \left(x + 1\right)}} \]
6. Step-by-step derivation

   1. distribute-rgt-in99.6%

      \[\leadsto \frac{-1}{\color{blue}{x \cdot x + 1 \cdot x}} \]

   2. *-un-lft-identity99.6%

      \[\leadsto \frac{-1}{x \cdot x + \color{blue}{x}} \]

7. Applied egg-rr99.6%

   \[\leadsto \frac{-1}{\color{blue}{x \cdot x + x}} \]

8. Final simplification99.6%

   \[\leadsto \frac{-1}{x + x \cdot x} \]

1. Initial program 80.5%

   \[\frac{1}{x + 1} - \frac{1}{x} \]
2. Step-by-step derivation

   1. frac-sub81.9%

      \[\leadsto \color{blue}{\frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\left(x + 1\right) \cdot x}} \]

   2. *-rgt-identity81.9%

      \[\leadsto \frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\color{blue}{\left(\left(x + 1\right) \cdot 1\right)} \cdot x} \]

   3. metadata-eval81.9%

      \[\leadsto \frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\left(\left(x + 1\right) \cdot \color{blue}{\frac{1}{1}}\right) \cdot x} \]

   4. div-inv81.9%

      \[\leadsto \frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\color{blue}{\frac{x + 1}{1}} \cdot x} \]

   5. associate-/r*81.9%

      \[\leadsto \color{blue}{\frac{\frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\frac{x + 1}{1}}}{x}} \]

   6. *-un-lft-identity81.9%

      \[\leadsto \frac{\frac{\color{blue}{x} - \left(x + 1\right) \cdot 1}{\frac{x + 1}{1}}}{x} \]

   7. *-rgt-identity81.9%

      \[\leadsto \frac{\frac{x - \color{blue}{\left(x + 1\right)}}{\frac{x + 1}{1}}}{x} \]

   8. +-commutative81.9%

      \[\leadsto \frac{\frac{x - \color{blue}{\left(1 + x\right)}}{\frac{x + 1}{1}}}{x} \]

   9. div-inv81.9%

      \[\leadsto \frac{\frac{x - \left(1 + x\right)}{\color{blue}{\left(x + 1\right) \cdot \frac{1}{1}}}}{x} \]

   10. metadata-eval81.9%

       \[\leadsto \frac{\frac{x - \left(1 + x\right)}{\left(x + 1\right) \cdot \color{blue}{1}}}{x} \]

   11. *-rgt-identity81.9%

       \[\leadsto \frac{\frac{x - \left(1 + x\right)}{\color{blue}{x + 1}}}{x} \]

   12. +-commutative81.9%

       \[\leadsto \frac{\frac{x - \left(1 + x\right)}{\color{blue}{1 + x}}}{x} \]

3. Applied egg-rr81.9%

   \[\leadsto \color{blue}{\frac{\frac{x - \left(1 + x\right)}{1 + x}}{x}} \]
4. Step-by-step derivation

   1. frac-2neg81.9%

      \[\leadsto \frac{\color{blue}{\frac{-\left(x - \left(1 + x\right)\right)}{-\left(1 + x\right)}}}{x} \]

   2. div-inv81.9%

      \[\leadsto \frac{\color{blue}{\left(-\left(x - \left(1 + x\right)\right)\right) \cdot \frac{1}{-\left(1 + x\right)}}}{x} \]

   3. +-commutative81.9%

      \[\leadsto \frac{\left(-\left(x - \color{blue}{\left(x + 1\right)}\right)\right) \cdot \frac{1}{-\left(1 + x\right)}}{x} \]

   4. +-commutative81.9%

      \[\leadsto \frac{\left(-\left(x - \left(x + 1\right)\right)\right) \cdot \frac{1}{-\color{blue}{\left(x + 1\right)}}}{x} \]

   5. distribute-neg-in81.9%

      \[\leadsto \frac{\left(-\left(x - \left(x + 1\right)\right)\right) \cdot \frac{1}{\color{blue}{\left(-x\right) + \left(-1\right)}}}{x} \]

   6. neg-mul-181.9%

      \[\leadsto \frac{\left(-\left(x - \left(x + 1\right)\right)\right) \cdot \frac{1}{\color{blue}{-1 \cdot x} + \left(-1\right)}}{x} \]

   7. metadata-eval81.9%

      \[\leadsto \frac{\left(-\left(x - \left(x + 1\right)\right)\right) \cdot \frac{1}{-1 \cdot x + \color{blue}{-1}}}{x} \]

   8. fma-def81.9%

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

5. Applied egg-rr81.9%

   \[\leadsto \frac{\color{blue}{\left(-\left(x - \left(x + 1\right)\right)\right) \cdot \frac{1}{\mathsf{fma}\left(-1, x, -1\right)}}}{x} \]
6. Step-by-step derivation

   1. associate-*r/81.9%

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

   2. *-rgt-identity81.9%

      \[\leadsto \frac{\frac{\color{blue}{-\left(x - \left(x + 1\right)\right)}}{\mathsf{fma}\left(-1, x, -1\right)}}{x} \]

   3. distribute-neg-frac81.9%

      \[\leadsto \frac{\color{blue}{-\frac{x - \left(x + 1\right)}{\mathsf{fma}\left(-1, x, -1\right)}}}{x} \]

   4. neg-mul-181.9%

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

   5. associate--r+99.9%

      \[\leadsto \frac{-1 \cdot \frac{\color{blue}{\left(x - x\right) - 1}}{\mathsf{fma}\left(-1, x, -1\right)}}{x} \]

   6. +-inverses99.9%

      \[\leadsto \frac{-1 \cdot \frac{\color{blue}{0} - 1}{\mathsf{fma}\left(-1, x, -1\right)}}{x} \]

   7. metadata-eval99.9%

      \[\leadsto \frac{-1 \cdot \frac{\color{blue}{-1}}{\mathsf{fma}\left(-1, x, -1\right)}}{x} \]

   8. associate-*r/99.9%

      \[\leadsto \frac{\color{blue}{\frac{-1 \cdot -1}{\mathsf{fma}\left(-1, x, -1\right)}}}{x} \]

   9. metadata-eval99.9%

      \[\leadsto \frac{\frac{\color{blue}{1}}{\mathsf{fma}\left(-1, x, -1\right)}}{x} \]

   10. fma-udef99.9%

       \[\leadsto \frac{\frac{1}{\color{blue}{-1 \cdot x + -1}}}{x} \]

   11. neg-mul-199.9%

       \[\leadsto \frac{\frac{1}{\color{blue}{\left(-x\right)} + -1}}{x} \]

   12. +-commutative99.9%

       \[\leadsto \frac{\frac{1}{\color{blue}{-1 + \left(-x\right)}}}{x} \]

   13. unsub-neg99.9%

       \[\leadsto \frac{\frac{1}{\color{blue}{-1 - x}}}{x} \]

7. Simplified99.9%

   \[\leadsto \frac{\color{blue}{\frac{1}{-1 - x}}}{x} \]

8. Final simplification99.9%

   \[\leadsto \frac{\frac{1}{-1 - x}}{x} \]

1. Initial program 80.5%

   \[\frac{1}{x + 1} - \frac{1}{x} \]

2. Taylor expanded in x around 0 53.0%

   \[\leadsto \color{blue}{\frac{-1}{x}} \]

3. Final simplification53.0%

   \[\leadsto \frac{-1}{x} \]

1. Initial program 80.5%

   \[\frac{1}{x + 1} - \frac{1}{x} \]
2. Step-by-step derivation

   1. frac-sub81.9%

      \[\leadsto \color{blue}{\frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\left(x + 1\right) \cdot x}} \]

   2. *-rgt-identity81.9%

      \[\leadsto \frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\color{blue}{\left(\left(x + 1\right) \cdot 1\right)} \cdot x} \]

   3. metadata-eval81.9%

      \[\leadsto \frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\left(\left(x + 1\right) \cdot \color{blue}{\frac{1}{1}}\right) \cdot x} \]

   4. div-inv81.9%

      \[\leadsto \frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\color{blue}{\frac{x + 1}{1}} \cdot x} \]

   5. associate-/r*81.9%

      \[\leadsto \color{blue}{\frac{\frac{1 \cdot x - \left(x + 1\right) \cdot 1}{\frac{x + 1}{1}}}{x}} \]

   6. *-un-lft-identity81.9%

      \[\leadsto \frac{\frac{\color{blue}{x} - \left(x + 1\right) \cdot 1}{\frac{x + 1}{1}}}{x} \]

   7. *-rgt-identity81.9%

      \[\leadsto \frac{\frac{x - \color{blue}{\left(x + 1\right)}}{\frac{x + 1}{1}}}{x} \]

   8. +-commutative81.9%

      \[\leadsto \frac{\frac{x - \color{blue}{\left(1 + x\right)}}{\frac{x + 1}{1}}}{x} \]

   9. div-inv81.9%

      \[\leadsto \frac{\frac{x - \left(1 + x\right)}{\color{blue}{\left(x + 1\right) \cdot \frac{1}{1}}}}{x} \]

   10. metadata-eval81.9%

       \[\leadsto \frac{\frac{x - \left(1 + x\right)}{\left(x + 1\right) \cdot \color{blue}{1}}}{x} \]

   11. *-rgt-identity81.9%

       \[\leadsto \frac{\frac{x - \left(1 + x\right)}{\color{blue}{x + 1}}}{x} \]

   12. +-commutative81.9%

       \[\leadsto \frac{\frac{x - \left(1 + x\right)}{\color{blue}{1 + x}}}{x} \]

3. Applied egg-rr81.9%

   \[\leadsto \color{blue}{\frac{\frac{x - \left(1 + x\right)}{1 + x}}{x}} \]

4. Taylor expanded in x around 0 51.6%

   \[\leadsto \frac{\color{blue}{x - 1}}{x} \]

5. Taylor expanded in x around inf 3.0%

   \[\leadsto \color{blue}{1} \]

6. Final simplification3.0%

   \[\leadsto 1 \]

herbie shell --seed 2023166 
(FPCore (x)
  :name "2frac (problem 3.3.1)"
  :precision binary64
  (- (/ 1.0 (+ x 1.0)) (/ 1.0 x)))