Error

Derivation

1. Initial program 0.3

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

3. Applied div-inv0.4

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

5. Applied pow10.4

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

6. Applied pow10.4

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

7. Applied pow-prod-down0.4

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

8. Simplified0.3

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

10. Applied div-sub0.4

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

12. Applied *-un-lft-identity0.4

    \[\leadsto {\left(\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*} - \frac{\tan x \cdot \tan x}{\color{blue}{1 \cdot (\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}}\right)}^{1}\]

13. Applied times-frac0.4

    \[\leadsto {\left(\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*} - \color{blue}{\frac{\tan x}{1} \cdot \frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}}\right)}^{1}\]

14. Applied add-cube-cbrt0.7

    \[\leadsto {\left(\color{blue}{\left(\sqrt[3]{\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}} \cdot \sqrt[3]{\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}}\right) \cdot \sqrt[3]{\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}}} - \frac{\tan x}{1} \cdot \frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\right)}^{1}\]

15. Applied prod-diff0.7

    \[\leadsto {\color{blue}{\left((\left(\sqrt[3]{\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}} \cdot \sqrt[3]{\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}}\right) \cdot \left(\sqrt[3]{\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}}\right) + \left(-\frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*} \cdot \frac{\tan x}{1}\right))_* + (\left(-\frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\right) \cdot \left(\frac{\tan x}{1}\right) + \left(\frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*} \cdot \frac{\tan x}{1}\right))_*\right)}}^{1}\]

16. Simplified0.4

    \[\leadsto {\left(\color{blue}{(\left(-\tan x\right) \cdot \left(\frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\right) + \left(\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\right))_*} + (\left(-\frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\right) \cdot \left(\frac{\tan x}{1}\right) + \left(\frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*} \cdot \frac{\tan x}{1}\right))_*\right)}^{1}\]

17. Simplified0.4

    \[\leadsto {\left((\left(-\tan x\right) \cdot \left(\frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\right) + \left(\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\right))_* + \color{blue}{0}\right)}^{1}\]

18. Final simplification0.4

    \[\leadsto (\left(-\tan x\right) \cdot \left(\frac{\tan x}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\right) + \left(\frac{1}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\right))_*\]

Reproduce

herbie shell --seed 2019053 +o rules:numerics
(FPCore (x)
  :name "Trigonometry B"
  (/ (- 1 (* (tan x) (tan x))) (+ 1 (* (tan x) (tan x)))))