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-sub0.4

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

5. Applied add-sqr-sqrt0.5

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

6. Applied associate-/r*0.5

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

7. Applied add-sqr-sqrt0.5

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

8. Applied associate-/r*0.5

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

9. Applied frac-sub0.5

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

10. Simplified0.5

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

11. Simplified0.3

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

12. Final simplification0.3

    \[\leadsto \frac{1 - \tan x \cdot \tan x}{\tan x \cdot \tan x + 1}\]

Reproduce

herbie shell --seed 2019072 
(FPCore (x)
  :name "Trigonometry B"
  (/ (- 1 (* (tan x) (tan x))) (+ 1 (* (tan x) (tan x)))))