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 \left(1 - \tan x \cdot \tan x\right)}}{1 + \tan x \cdot \tan x}\]
Applied associate-/l*0.4
\[\leadsto \color{blue}{\frac{1}{\frac{1 + \tan x \cdot \tan x}{1 - \tan x \cdot \tan x}}}\]
- Using strategy
rm Applied div-inv0.4
\[\leadsto \frac{1}{\color{blue}{\left(1 + \tan x \cdot \tan x\right) \cdot \frac{1}{1 - \tan x \cdot \tan x}}}\]
Applied associate-/r*0.4
\[\leadsto \color{blue}{\frac{\frac{1}{1 + \tan x \cdot \tan x}}{\frac{1}{1 - \tan x \cdot \tan x}}}\]
- Using strategy
rm Applied flip3--0.5
\[\leadsto \frac{\frac{1}{1 + \tan x \cdot \tan x}}{\frac{1}{\color{blue}{\frac{{1}^{3} - {\left(\tan x \cdot \tan x\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) + 1 \cdot \left(\tan x \cdot \tan x\right)\right)}}}}\]
Applied associate-/r/0.5
\[\leadsto \frac{\frac{1}{1 + \tan x \cdot \tan x}}{\color{blue}{\frac{1}{{1}^{3} - {\left(\tan x \cdot \tan x\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) + 1 \cdot \left(\tan x \cdot \tan x\right)\right)\right)}}\]
Applied flip3-+0.5
\[\leadsto \frac{\frac{1}{\color{blue}{\frac{{1}^{3} + {\left(\tan x \cdot \tan x\right)}^{3}}{1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) - 1 \cdot \left(\tan x \cdot \tan x\right)\right)}}}}{\frac{1}{{1}^{3} - {\left(\tan x \cdot \tan x\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) + 1 \cdot \left(\tan x \cdot \tan x\right)\right)\right)}\]
Applied associate-/r/0.5
\[\leadsto \frac{\color{blue}{\frac{1}{{1}^{3} + {\left(\tan x \cdot \tan x\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) - 1 \cdot \left(\tan x \cdot \tan x\right)\right)\right)}}{\frac{1}{{1}^{3} - {\left(\tan x \cdot \tan x\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) + 1 \cdot \left(\tan x \cdot \tan x\right)\right)\right)}\]
Applied times-frac0.5
\[\leadsto \color{blue}{\frac{\frac{1}{{1}^{3} + {\left(\tan x \cdot \tan x\right)}^{3}}}{\frac{1}{{1}^{3} - {\left(\tan x \cdot \tan x\right)}^{3}}} \cdot \frac{1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) - 1 \cdot \left(\tan x \cdot \tan x\right)\right)}{1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) + 1 \cdot \left(\tan x \cdot \tan x\right)\right)}}\]
Simplified0.4
\[\leadsto \color{blue}{\frac{(\left(-\tan x\right) \cdot \left({\left(\tan x\right)}^{5}\right) + 1)_*}{(\left({\left(\tan x\right)}^{5}\right) \cdot \left(\tan x\right) + 1)_*}} \cdot \frac{1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) - 1 \cdot \left(\tan x \cdot \tan x\right)\right)}{1 \cdot 1 + \left(\left(\tan x \cdot \tan x\right) \cdot \left(\tan x \cdot \tan x\right) + 1 \cdot \left(\tan x \cdot \tan x\right)\right)}\]
Simplified0.4
\[\leadsto \frac{(\left(-\tan x\right) \cdot \left({\left(\tan x\right)}^{5}\right) + 1)_*}{(\left({\left(\tan x\right)}^{5}\right) \cdot \left(\tan x\right) + 1)_*} \cdot \color{blue}{\frac{(\left((\left(\tan x\right) \cdot \left(\tan x\right) + -1)_*\right) \cdot \left(\tan x \cdot \tan x\right) + 1)_*}{(\left((\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*\right) \cdot \left(\tan x \cdot \tan x\right) + 1)_*}}\]
Final simplification0.4
\[\leadsto \frac{(\left((\left(\tan x\right) \cdot \left(\tan x\right) + -1)_*\right) \cdot \left(\tan x \cdot \tan x\right) + 1)_*}{(\left((\left(\tan x\right) \cdot \left(\tan x\right) + 1)_*\right) \cdot \left(\tan x \cdot \tan x\right) + 1)_*} \cdot \frac{(\left(-\tan x\right) \cdot \left({\left(\tan x\right)}^{5}\right) + 1)_*}{(\left({\left(\tan x\right)}^{5}\right) \cdot \left(\tan x\right) + 1)_*}\]
