Error

Try it out

Target

Derivation

1. Initial program 3.8

   \[\frac{{\left(\frac{1}{1 + e^{-s}}\right)}^{c_p} \cdot {\left(1 - \frac{1}{1 + e^{-s}}\right)}^{c_n}}{{\left(\frac{1}{1 + e^{-t}}\right)}^{c_p} \cdot {\left(1 - \frac{1}{1 + e^{-t}}\right)}^{c_n}}\]
2. Using strategy rm

3. Applied add-exp-log3.8

   \[\leadsto \frac{{\left(\frac{1}{1 + e^{-s}}\right)}^{c_p} \cdot {\left(1 - \frac{1}{1 + e^{-s}}\right)}^{c_n}}{{\left(\frac{1}{1 + e^{-t}}\right)}^{c_p} \cdot {\color{blue}{\left(e^{\log \left(1 - \frac{1}{1 + e^{-t}}\right)}\right)}}^{c_n}}\]

4. Applied pow-exp3.8

   \[\leadsto \frac{{\left(\frac{1}{1 + e^{-s}}\right)}^{c_p} \cdot {\left(1 - \frac{1}{1 + e^{-s}}\right)}^{c_n}}{{\left(\frac{1}{1 + e^{-t}}\right)}^{c_p} \cdot \color{blue}{e^{\log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}}\]

5. Applied add-exp-log3.8

   \[\leadsto \frac{{\left(\frac{1}{1 + e^{-s}}\right)}^{c_p} \cdot {\left(1 - \frac{1}{1 + e^{-s}}\right)}^{c_n}}{{\left(\frac{1}{\color{blue}{e^{\log \left(1 + e^{-t}\right)}}}\right)}^{c_p} \cdot e^{\log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}\]

6. Applied rec-exp3.8

   \[\leadsto \frac{{\left(\frac{1}{1 + e^{-s}}\right)}^{c_p} \cdot {\left(1 - \frac{1}{1 + e^{-s}}\right)}^{c_n}}{{\color{blue}{\left(e^{-\log \left(1 + e^{-t}\right)}\right)}}^{c_p} \cdot e^{\log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}\]

7. Applied pow-exp3.8

   \[\leadsto \frac{{\left(\frac{1}{1 + e^{-s}}\right)}^{c_p} \cdot {\left(1 - \frac{1}{1 + e^{-s}}\right)}^{c_n}}{\color{blue}{e^{\left(-\log \left(1 + e^{-t}\right)\right) \cdot c_p}} \cdot e^{\log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}\]

8. Applied prod-exp3.8

   \[\leadsto \frac{{\left(\frac{1}{1 + e^{-s}}\right)}^{c_p} \cdot {\left(1 - \frac{1}{1 + e^{-s}}\right)}^{c_n}}{\color{blue}{e^{\left(-\log \left(1 + e^{-t}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}}\]

9. Applied add-exp-log3.8

   \[\leadsto \frac{{\left(\frac{1}{1 + e^{-s}}\right)}^{c_p} \cdot {\color{blue}{\left(e^{\log \left(1 - \frac{1}{1 + e^{-s}}\right)}\right)}}^{c_n}}{e^{\left(-\log \left(1 + e^{-t}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}\]

10. Applied pow-exp3.8

    \[\leadsto \frac{{\left(\frac{1}{1 + e^{-s}}\right)}^{c_p} \cdot \color{blue}{e^{\log \left(1 - \frac{1}{1 + e^{-s}}\right) \cdot c_n}}}{e^{\left(-\log \left(1 + e^{-t}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}\]

11. Applied add-exp-log3.8

    \[\leadsto \frac{{\left(\frac{1}{\color{blue}{e^{\log \left(1 + e^{-s}\right)}}}\right)}^{c_p} \cdot e^{\log \left(1 - \frac{1}{1 + e^{-s}}\right) \cdot c_n}}{e^{\left(-\log \left(1 + e^{-t}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}\]

12. Applied rec-exp3.8

    \[\leadsto \frac{{\color{blue}{\left(e^{-\log \left(1 + e^{-s}\right)}\right)}}^{c_p} \cdot e^{\log \left(1 - \frac{1}{1 + e^{-s}}\right) \cdot c_n}}{e^{\left(-\log \left(1 + e^{-t}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}\]

13. Applied pow-exp3.8

    \[\leadsto \frac{\color{blue}{e^{\left(-\log \left(1 + e^{-s}\right)\right) \cdot c_p}} \cdot e^{\log \left(1 - \frac{1}{1 + e^{-s}}\right) \cdot c_n}}{e^{\left(-\log \left(1 + e^{-t}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}\]

14. Applied prod-exp3.8

    \[\leadsto \frac{\color{blue}{e^{\left(-\log \left(1 + e^{-s}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-s}}\right) \cdot c_n}}}{e^{\left(-\log \left(1 + e^{-t}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n}}\]

15. Applied div-exp1.6

    \[\leadsto \color{blue}{e^{\left(\left(-\log \left(1 + e^{-s}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-s}}\right) \cdot c_n\right) - \left(\left(-\log \left(1 + e^{-t}\right)\right) \cdot c_p + \log \left(1 - \frac{1}{1 + e^{-t}}\right) \cdot c_n\right)}}\]

16. Applied simplify1.6

    \[\leadsto e^{\color{blue}{\left(\log \left(1 - \frac{1}{1 + e^{-s}}\right) - \log \left(1 - \frac{1}{e^{-t} + 1}\right)\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}}\]
17. Using strategy rm

18. Applied flip3--1.6

    \[\leadsto e^{\left(\log \left(1 - \frac{1}{1 + e^{-s}}\right) - \log \color{blue}{\left(\frac{{1}^{3} - {\left(\frac{1}{e^{-t} + 1}\right)}^{3}}{1 \cdot 1 + \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + 1 \cdot \frac{1}{e^{-t} + 1}\right)}\right)}\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

19. Applied log-div1.6

    \[\leadsto e^{\left(\log \left(1 - \frac{1}{1 + e^{-s}}\right) - \color{blue}{\left(\log \left({1}^{3} - {\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right) - \log \left(1 \cdot 1 + \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + 1 \cdot \frac{1}{e^{-t} + 1}\right)\right)\right)}\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

20. Applied associate--r-1.6

    \[\leadsto e^{\color{blue}{\left(\left(\log \left(1 - \frac{1}{1 + e^{-s}}\right) - \log \left({1}^{3} - {\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)\right) + \log \left(1 \cdot 1 + \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + 1 \cdot \frac{1}{e^{-t} + 1}\right)\right)\right)} \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]
21. Using strategy rm

22. Applied flip3--1.6

    \[\leadsto e^{\left(\left(\log \left(1 - \frac{1}{1 + e^{-s}}\right) - \log \color{blue}{\left(\frac{{\left({1}^{3}\right)}^{3} - {\left({\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}^{3}}{{1}^{3} \cdot {1}^{3} + \left({\left(\frac{1}{e^{-t} + 1}\right)}^{3} \cdot {\left(\frac{1}{e^{-t} + 1}\right)}^{3} + {1}^{3} \cdot {\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}\right)}\right) + \log \left(1 \cdot 1 + \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + 1 \cdot \frac{1}{e^{-t} + 1}\right)\right)\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

23. Applied log-div1.6

    \[\leadsto e^{\left(\left(\log \left(1 - \frac{1}{1 + e^{-s}}\right) - \color{blue}{\left(\log \left({\left({1}^{3}\right)}^{3} - {\left({\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}^{3}\right) - \log \left({1}^{3} \cdot {1}^{3} + \left({\left(\frac{1}{e^{-t} + 1}\right)}^{3} \cdot {\left(\frac{1}{e^{-t} + 1}\right)}^{3} + {1}^{3} \cdot {\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)\right)\right)}\right) + \log \left(1 \cdot 1 + \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + 1 \cdot \frac{1}{e^{-t} + 1}\right)\right)\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

24. Applied associate--r-1.6

    \[\leadsto e^{\left(\color{blue}{\left(\left(\log \left(1 - \frac{1}{1 + e^{-s}}\right) - \log \left({\left({1}^{3}\right)}^{3} - {\left({\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}^{3}\right)\right) + \log \left({1}^{3} \cdot {1}^{3} + \left({\left(\frac{1}{e^{-t} + 1}\right)}^{3} \cdot {\left(\frac{1}{e^{-t} + 1}\right)}^{3} + {1}^{3} \cdot {\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)\right)\right)} + \log \left(1 \cdot 1 + \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + 1 \cdot \frac{1}{e^{-t} + 1}\right)\right)\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

25. Applied associate-+l+1.6

    \[\leadsto e^{\color{blue}{\left(\left(\log \left(1 - \frac{1}{1 + e^{-s}}\right) - \log \left({\left({1}^{3}\right)}^{3} - {\left({\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}^{3}\right)\right) + \left(\log \left({1}^{3} \cdot {1}^{3} + \left({\left(\frac{1}{e^{-t} + 1}\right)}^{3} \cdot {\left(\frac{1}{e^{-t} + 1}\right)}^{3} + {1}^{3} \cdot {\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)\right) + \log \left(1 \cdot 1 + \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + 1 \cdot \frac{1}{e^{-t} + 1}\right)\right)\right)\right)} \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

26. Applied simplify1.6

    \[\leadsto e^{\left(\left(\log \left(1 - \frac{1}{1 + e^{-s}}\right) - \log \left({\left({1}^{3}\right)}^{3} - {\left({\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}^{3}\right)\right) + \color{blue}{\left(\log \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + \left(\frac{1}{e^{-t} + 1} + 1\right)\right) + \log \left(\frac{\frac{1}{e^{-t} + 1}}{{\left(e^{-t} + 1\right)}^{\left(\left(3 + 1\right) + 1\right)}} + \left(\frac{\frac{1}{e^{-t} + 1}}{\left(e^{-t} + 1\right) \cdot \left(e^{-t} + 1\right)} + 1\right)\right)\right)}\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]
27. Using strategy rm

28. Applied add-sqr-sqrt1.7

    \[\leadsto e^{\left(\left(\log \color{blue}{\left(\sqrt{1 - \frac{1}{1 + e^{-s}}} \cdot \sqrt{1 - \frac{1}{1 + e^{-s}}}\right)} - \log \left({\left({1}^{3}\right)}^{3} - {\left({\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}^{3}\right)\right) + \left(\log \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + \left(\frac{1}{e^{-t} + 1} + 1\right)\right) + \log \left(\frac{\frac{1}{e^{-t} + 1}}{{\left(e^{-t} + 1\right)}^{\left(\left(3 + 1\right) + 1\right)}} + \left(\frac{\frac{1}{e^{-t} + 1}}{\left(e^{-t} + 1\right) \cdot \left(e^{-t} + 1\right)} + 1\right)\right)\right)\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

29. Applied log-prod1.7

    \[\leadsto e^{\left(\left(\color{blue}{\left(\log \left(\sqrt{1 - \frac{1}{1 + e^{-s}}}\right) + \log \left(\sqrt{1 - \frac{1}{1 + e^{-s}}}\right)\right)} - \log \left({\left({1}^{3}\right)}^{3} - {\left({\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}^{3}\right)\right) + \left(\log \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + \left(\frac{1}{e^{-t} + 1} + 1\right)\right) + \log \left(\frac{\frac{1}{e^{-t} + 1}}{{\left(e^{-t} + 1\right)}^{\left(\left(3 + 1\right) + 1\right)}} + \left(\frac{\frac{1}{e^{-t} + 1}}{\left(e^{-t} + 1\right) \cdot \left(e^{-t} + 1\right)} + 1\right)\right)\right)\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

30. Applied associate--l+1.6

    \[\leadsto e^{\left(\color{blue}{\left(\log \left(\sqrt{1 - \frac{1}{1 + e^{-s}}}\right) + \left(\log \left(\sqrt{1 - \frac{1}{1 + e^{-s}}}\right) - \log \left({\left({1}^{3}\right)}^{3} - {\left({\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}^{3}\right)\right)\right)} + \left(\log \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + \left(\frac{1}{e^{-t} + 1} + 1\right)\right) + \log \left(\frac{\frac{1}{e^{-t} + 1}}{{\left(e^{-t} + 1\right)}^{\left(\left(3 + 1\right) + 1\right)}} + \left(\frac{\frac{1}{e^{-t} + 1}}{\left(e^{-t} + 1\right) \cdot \left(e^{-t} + 1\right)} + 1\right)\right)\right)\right) \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

31. Applied associate-+l+1.7

    \[\leadsto e^{\color{blue}{\left(\log \left(\sqrt{1 - \frac{1}{1 + e^{-s}}}\right) + \left(\left(\log \left(\sqrt{1 - \frac{1}{1 + e^{-s}}}\right) - \log \left({\left({1}^{3}\right)}^{3} - {\left({\left(\frac{1}{e^{-t} + 1}\right)}^{3}\right)}^{3}\right)\right) + \left(\log \left(\frac{1}{e^{-t} + 1} \cdot \frac{1}{e^{-t} + 1} + \left(\frac{1}{e^{-t} + 1} + 1\right)\right) + \log \left(\frac{\frac{1}{e^{-t} + 1}}{{\left(e^{-t} + 1\right)}^{\left(\left(3 + 1\right) + 1\right)}} + \left(\frac{\frac{1}{e^{-t} + 1}}{\left(e^{-t} + 1\right) \cdot \left(e^{-t} + 1\right)} + 1\right)\right)\right)\right)\right)} \cdot c_n - \left(\log \left(1 + e^{-s}\right) - \log \left(e^{-t} + 1\right)\right) \cdot c_p}\]

Runtime

Time bar (total: 5.6m)Debug logProfile

herbie shell --seed 2018193 
(FPCore (c_p c_n t s)
  :name "Harley's example"
  :pre (and (< 0 c_p) (< 0 c_n))

  :herbie-target
  (* (pow (/ (+ 1 (exp (- t))) (+ 1 (exp (- s)))) c_p) (pow (/ (+ 1 (exp t)) (+ 1 (exp s))) c_n))

  (/ (* (pow (/ 1 (+ 1 (exp (- s)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- s))))) c_n)) (* (pow (/ 1 (+ 1 (exp (- t)))) c_p) (pow (- 1 (/ 1 (+ 1 (exp (- t))))) c_n))))