Initial program 16.9
\[\pi \cdot \ell - \frac{1}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]
- Using strategy
rm Applied *-un-lft-identity16.9
\[\leadsto \pi \cdot \ell - \frac{\color{blue}{1 \cdot 1}}{F \cdot F} \cdot \tan \left(\pi \cdot \ell\right)\]
Applied times-frac16.9
\[\leadsto \pi \cdot \ell - \color{blue}{\left(\frac{1}{F} \cdot \frac{1}{F}\right)} \cdot \tan \left(\pi \cdot \ell\right)\]
Applied associate-*l*12.7
\[\leadsto \pi \cdot \ell - \color{blue}{\frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\pi \cdot \ell\right)\right)}\]
- Using strategy
rm Applied add-sqr-sqrt12.7
\[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\color{blue}{\left(\sqrt{\pi} \cdot \sqrt{\pi}\right)} \cdot \ell\right)\right)\]
Applied associate-*l*12.7
\[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \color{blue}{\left(\sqrt{\pi} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)}\right)\]
- Using strategy
rm Applied add-sqr-sqrt12.7
\[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\sqrt{\color{blue}{\sqrt{\pi} \cdot \sqrt{\pi}}} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)\right)\]
Applied sqrt-prod12.7
\[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\color{blue}{\left(\sqrt{\sqrt{\pi}} \cdot \sqrt{\sqrt{\pi}}\right)} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)\right)\]
Applied associate-*l*12.7
\[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \color{blue}{\left(\sqrt{\sqrt{\pi}} \cdot \left(\sqrt{\sqrt{\pi}} \cdot \left(\sqrt{\pi} \cdot \ell\right)\right)\right)}\right)\]
- Using strategy
rm Applied add-sqr-sqrt12.7
\[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\sqrt{\sqrt{\pi}} \cdot \left(\sqrt{\sqrt{\pi}} \cdot \left(\sqrt{\color{blue}{\sqrt{\pi} \cdot \sqrt{\pi}}} \cdot \ell\right)\right)\right)\right)\]
Applied sqrt-prod12.7
\[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\sqrt{\sqrt{\pi}} \cdot \left(\sqrt{\sqrt{\pi}} \cdot \left(\color{blue}{\left(\sqrt{\sqrt{\pi}} \cdot \sqrt{\sqrt{\pi}}\right)} \cdot \ell\right)\right)\right)\right)\]
Final simplification12.7
\[\leadsto \pi \cdot \ell - \frac{1}{F} \cdot \left(\frac{1}{F} \cdot \tan \left(\sqrt{\sqrt{\pi}} \cdot \left(\sqrt{\sqrt{\pi}} \cdot \left(\left(\sqrt{\sqrt{\pi}} \cdot \sqrt{\sqrt{\pi}}\right) \cdot \ell\right)\right)\right)\right)\]