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{\color{blue}{1 \cdot 1} - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]
Applied difference-of-squares0.3
\[\leadsto \frac{\color{blue}{\left(1 + \tan x\right) \cdot \left(1 - \tan x\right)}}{1 + \tan x \cdot \tan x}\]
- Using strategy
rm Applied flip--0.3
\[\leadsto \frac{\left(1 + \tan x\right) \cdot \color{blue}{\frac{1 \cdot 1 - \tan x \cdot \tan x}{1 + \tan x}}}{1 + \tan x \cdot \tan x}\]
Applied flip-+0.4
\[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \tan x \cdot \tan x}{1 - \tan x}} \cdot \frac{1 \cdot 1 - \tan x \cdot \tan x}{1 + \tan x}}{1 + \tan x \cdot \tan x}\]
Applied frac-times0.4
\[\leadsto \frac{\color{blue}{\frac{\left(1 \cdot 1 - \tan x \cdot \tan x\right) \cdot \left(1 \cdot 1 - \tan x \cdot \tan x\right)}{\left(1 - \tan x\right) \cdot \left(1 + \tan x\right)}}}{1 + \tan x \cdot \tan x}\]
Applied associate-/l/0.5
\[\leadsto \color{blue}{\frac{\left(1 \cdot 1 - \tan x \cdot \tan x\right) \cdot \left(1 \cdot 1 - \tan x \cdot \tan x\right)}{\left(1 + \tan x \cdot \tan x\right) \cdot \left(\left(1 - \tan x\right) \cdot \left(1 + \tan x\right)\right)}}\]
Simplified0.5
\[\leadsto \frac{\color{blue}{\left(1 - \tan x \cdot \tan x\right) \cdot \left(1 - \tan x \cdot \tan x\right)}}{\left(1 + \tan x \cdot \tan x\right) \cdot \left(\left(1 - \tan x\right) \cdot \left(1 + \tan x\right)\right)}\]
Final simplification0.5
\[\leadsto \frac{\left(1 - \tan x \cdot \tan x\right) \cdot \left(1 - \tan x \cdot \tan x\right)}{\left(\left(1 - \tan x\right) \cdot \left(1 + \tan x\right)\right) \cdot \left(\tan x \cdot \tan x + 1\right)}\]