Error

Try it out

Target

Derivation

1. Initial program 19.7

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

3. Applied add-sqr-sqrt19.9

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

5. Applied frac-sub19.9

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

6. Simplified19.9

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

8. Applied add-log-exp19.9

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

10. Applied add-sqr-sqrt19.9

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

11. Applied log-prod19.9

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

12. Final simplification19.9

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

Reproduce

herbie shell --seed 2019004 +o rules:numerics
(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)))))

Details

Time bar (total: 27.2s)Debug log