Initial program 0.3
\[\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]
- Using strategy
rm Applied *-un-lft-identity0.3
\[\leadsto \frac{1 - \tan x \cdot \tan x}{\color{blue}{1 \cdot \left(1 + \tan x \cdot \tan x\right)}}\]
Applied associate-/r*0.3
\[\leadsto \color{blue}{\frac{\frac{1 - \tan x \cdot \tan x}{1}}{1 + \tan x \cdot \tan x}}\]
Simplified0.3
\[\leadsto \frac{\frac{1 - \tan x \cdot \tan x}{1}}{\color{blue}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}}\]
- Using strategy
rm Applied *-un-lft-identity0.3
\[\leadsto \frac{\color{blue}{1 \cdot \frac{1 - \tan x \cdot \tan x}{1}}}{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}\]
Applied associate-/l*0.4
\[\leadsto \color{blue}{\frac{1}{\frac{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}{\frac{1 - \tan x \cdot \tan x}{1}}}}\]
Final simplification0.4
\[\leadsto \frac{1}{\frac{(\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*}{1 - \tan x \cdot \tan x}}\]