Error

Try it out

Derivation

1. Initial program 31.2

   \[\frac{1 - \cos x}{x \cdot x}\]

2. Initial simplification31.2

   \[\leadsto \frac{1 - \cos x}{x \cdot x}\]
3. Using strategy rm

4. Applied flip--31.3

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

5. Applied associate-/l/31.3

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

6. Simplified15.5

   \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(x \cdot x\right) \cdot \left(1 + \cos x\right)}\]
7. Using strategy rm

8. Applied flip3-+15.5

   \[\leadsto \frac{\sin x \cdot \sin x}{\left(x \cdot x\right) \cdot \color{blue}{\frac{{1}^{3} + {\left(\cos x\right)}^{3}}{1 \cdot 1 + \left(\cos x \cdot \cos x - 1 \cdot \cos x\right)}}}\]

9. Applied associate-*r/15.5

   \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\frac{\left(x \cdot x\right) \cdot \left({1}^{3} + {\left(\cos x\right)}^{3}\right)}{1 \cdot 1 + \left(\cos x \cdot \cos x - 1 \cdot \cos x\right)}}}\]

10. Simplified15.5

    \[\leadsto \frac{\sin x \cdot \sin x}{\frac{\left(x \cdot x\right) \cdot \left({1}^{3} + {\left(\cos x\right)}^{3}\right)}{\color{blue}{\cos x \cdot \cos x - \left(\cos x + -1\right)}}}\]
11. Using strategy rm

12. Applied flip3-+15.5

    \[\leadsto \frac{\sin x \cdot \sin x}{\frac{\left(x \cdot x\right) \cdot \left({1}^{3} + {\left(\cos x\right)}^{3}\right)}{\cos x \cdot \cos x - \color{blue}{\frac{{\left(\cos x\right)}^{3} + {-1}^{3}}{\cos x \cdot \cos x + \left(-1 \cdot -1 - \cos x \cdot -1\right)}}}}\]

13. Applied cos-mult15.5

    \[\leadsto \frac{\sin x \cdot \sin x}{\frac{\left(x \cdot x\right) \cdot \left({1}^{3} + {\left(\cos x\right)}^{3}\right)}{\color{blue}{\frac{\cos \left(x + x\right) + \cos \left(x - x\right)}{2}} - \frac{{\left(\cos x\right)}^{3} + {-1}^{3}}{\cos x \cdot \cos x + \left(-1 \cdot -1 - \cos x \cdot -1\right)}}}\]

14. Applied frac-sub15.5

    \[\leadsto \frac{\sin x \cdot \sin x}{\frac{\left(x \cdot x\right) \cdot \left({1}^{3} + {\left(\cos x\right)}^{3}\right)}{\color{blue}{\frac{\left(\cos \left(x + x\right) + \cos \left(x - x\right)\right) \cdot \left(\cos x \cdot \cos x + \left(-1 \cdot -1 - \cos x \cdot -1\right)\right) - 2 \cdot \left({\left(\cos x\right)}^{3} + {-1}^{3}\right)}{2 \cdot \left(\cos x \cdot \cos x + \left(-1 \cdot -1 - \cos x \cdot -1\right)\right)}}}}\]

15. Applied associate-/r/15.9

    \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\frac{\left(x \cdot x\right) \cdot \left({1}^{3} + {\left(\cos x\right)}^{3}\right)}{\left(\cos \left(x + x\right) + \cos \left(x - x\right)\right) \cdot \left(\cos x \cdot \cos x + \left(-1 \cdot -1 - \cos x \cdot -1\right)\right) - 2 \cdot \left({\left(\cos x\right)}^{3} + {-1}^{3}\right)} \cdot \left(2 \cdot \left(\cos x \cdot \cos x + \left(-1 \cdot -1 - \cos x \cdot -1\right)\right)\right)}}\]

16. Applied times-frac16.0

    \[\leadsto \color{blue}{\frac{\sin x}{\frac{\left(x \cdot x\right) \cdot \left({1}^{3} + {\left(\cos x\right)}^{3}\right)}{\left(\cos \left(x + x\right) + \cos \left(x - x\right)\right) \cdot \left(\cos x \cdot \cos x + \left(-1 \cdot -1 - \cos x \cdot -1\right)\right) - 2 \cdot \left({\left(\cos x\right)}^{3} + {-1}^{3}\right)}} \cdot \frac{\sin x}{2 \cdot \left(\cos x \cdot \cos x + \left(-1 \cdot -1 - \cos x \cdot -1\right)\right)}}\]

17. Simplified0.5

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

18. Simplified0.5

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

19. Final simplification0.5

    \[\leadsto \frac{\frac{\sin x}{2}}{\left(\cos x + 1\right) + \cos x \cdot \cos x} \cdot \left(\left(\left(\cos \left(x + x\right) + 1\right) \cdot \left(\left(\cos x + 1\right) + \cos x \cdot \cos x\right) - \left(-2 + \left(\cos x \cdot \cos x\right) \cdot \left(\cos x \cdot 2\right)\right)\right) \cdot \frac{\frac{\sin x}{x}}{x + \left(\cos x \cdot \cos x\right) \cdot \left(\cos x \cdot x\right)}\right)\]

Runtime

Time bar (total: 28.0s)Debug logProfile

herbie shell --seed 2018274 
(FPCore (x)
  :name "cos2 (problem 3.4.1)"
  (/ (- 1 (cos x)) (* x x)))