Error

Target

Derivation

1. Initial program 19.1

   \[\frac{1}{\sqrt{x}} - \frac{1}{\sqrt{x + 1}}\]
2. Using strategy rm

3. Applied flip--19.1

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

4. Applied simplify19.1

   \[\leadsto \frac{\color{blue}{\frac{1}{x} - \frac{1}{x + 1}}}{\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}}\]
5. Using strategy rm

6. Applied frac-sub18.5

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

7. Applied associate-/l/18.5

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

9. Applied add-exp-log21.2

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

10. Applied add-exp-log20.8

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

11. Applied prod-exp20.8

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

12. Applied add-exp-log20.8

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

13. Applied div-exp20.8

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

14. Applied simplify4.5

    \[\leadsto e^{\color{blue}{\left(\left(-\log x\right) - \log \left(x + 1\right)\right) - \log \left(\frac{1}{\sqrt{x}} + \frac{1}{\sqrt{x + 1}}\right)}}\]
15. Using strategy rm

16. Applied sub-neg4.5

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

17. Applied associate--l+4.5

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

18. Applied exp-sum4.4

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

19. Applied simplify3.9

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

20. Applied simplify0.4

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

Runtime

Time bar (total: 1.1m)Debug logProfile

herbie shell --seed '#(1071373924 2949776965 1885069702 3247780810 90874544 2263903749)' 
(FPCore (x)
  :name "2isqrt (example 3.6)"

  :herbie-target
  (/ 1 (+ (* (+ x 1) (sqrt x)) (* x (sqrt (+ x 1)))))

  (- (/ 1 (sqrt x)) (/ 1 (sqrt (+ x 1)))))