Error

Try it out

Target

Derivation

1. Initial program 20.0

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

3. Applied frac-sub20.0

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

4. Simplified20.0

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

5. Simplified20.0

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

7. Applied flip--19.8

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

8. Applied associate-/l/19.8

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

9. Simplified19.4

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

11. Applied add-sqr-sqrt19.4

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

12. Applied times-frac19.4

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

13. Simplified19.3

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

14. Simplified5.2

    \[\leadsto \sqrt{\frac{\frac{1 + 0}{x + 1}}{x}} \cdot \color{blue}{\frac{\sqrt{1 + 0}}{\sqrt{x + 1} + \sqrt{x}}}\]
15. Using strategy rm

16. Applied div-inv5.2

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

17. Applied sqrt-prod0.3

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

18. Applied associate-*l*0.3

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

19. Simplified0.3

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

20. Final simplification0.3

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

Runtime

Time bar (total: 2.5m)Debug logProfile

herbie shell --seed 2018214 
(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)))))