Error

Try it out

Target

Derivation

1. Initial program 62.4

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

3. Applied add-log-exp58.2

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

5. Applied add-sqr-sqrt58.2

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

6. Applied log-prod58.2

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

7. Applied associate--l+58.2

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

9. Applied add-sqr-sqrt58.2

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

10. Applied sqrt-prod58.1

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

11. Applied log-prod58.2

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

12. Applied associate-+l+58.2

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

13. Taylor expanded around 0 58.2

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

14. Simplified57.8

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

15. Final simplification57.8

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

Runtime

Time bar (total: 35.5s)Debug logProfile

herbie shell --seed 2018255 +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)))))