Initial program 99.4%
\[\frac{1}{\sqrt{1 + \frac{\frac{1}{\frac{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right) \cdot \cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right)}{alphax \cdot alphax} + \frac{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right) \cdot \sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right)}{alphay \cdot alphay}} \cdot u0}{1 - u0}}}
\]
Simplified99.4%
\[\leadsto \color{blue}{\frac{1}{\sqrt{1 + \frac{u0}{\mathsf{fma}\left(\frac{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \left(2 \cdot u1 + 0.5\right)\right)\right)}{alphay}, \frac{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \left(2 \cdot u1 + 0.5\right)\right)\right)}{alphay}, \frac{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \left(2 \cdot u1 + 0.5\right)\right)\right)}{alphax} \cdot \frac{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \left(2 \cdot u1 + 0.5\right)\right)\right)}{alphax}\right) \cdot \left(1 - u0\right)}}}}
\]
Proof
[Start]99.4 | \[ \frac{1}{\sqrt{1 + \frac{\frac{1}{\frac{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right) \cdot \cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right)}{alphax \cdot alphax} + \frac{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right) \cdot \sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\left(2 \cdot \pi\right) \cdot u1 + 0.5 \cdot \pi\right)\right)}{alphay \cdot alphay}} \cdot u0}{1 - u0}}}
\] |
|---|
Taylor expanded in alphay around 0 99.4%
\[\leadsto \frac{1}{\sqrt{1 + \frac{u0}{\color{blue}{\left(\frac{{\sin \tan^{-1} \left(\frac{\tan \left(\left(2 \cdot u1 + 0.5\right) \cdot \pi\right) \cdot alphay}{alphax}\right)}^{2}}{{alphay}^{2}} + \frac{{\cos \tan^{-1} \left(\frac{\tan \left(\left(2 \cdot u1 + 0.5\right) \cdot \pi\right) \cdot alphay}{alphax}\right)}^{2}}{{alphax}^{2}}\right)} \cdot \left(1 - u0\right)}}}
\]
Simplified99.4%
\[\leadsto \frac{1}{\sqrt{1 + \frac{u0}{\color{blue}{\left(\frac{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphax \cdot alphax} + \frac{{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphay \cdot alphay}\right)} \cdot \left(1 - u0\right)}}}
\]
Proof
[Start]99.4 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{{\sin \tan^{-1} \left(\frac{\tan \left(\left(2 \cdot u1 + 0.5\right) \cdot \pi\right) \cdot alphay}{alphax}\right)}^{2}}{{alphay}^{2}} + \frac{{\cos \tan^{-1} \left(\frac{\tan \left(\left(2 \cdot u1 + 0.5\right) \cdot \pi\right) \cdot alphay}{alphax}\right)}^{2}}{{alphax}^{2}}\right) \cdot \left(1 - u0\right)}}}
\] |
|---|
+-commutative [=>]99.4 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\color{blue}{\left(\frac{{\cos \tan^{-1} \left(\frac{\tan \left(\left(2 \cdot u1 + 0.5\right) \cdot \pi\right) \cdot alphay}{alphax}\right)}^{2}}{{alphax}^{2}} + \frac{{\sin \tan^{-1} \left(\frac{\tan \left(\left(2 \cdot u1 + 0.5\right) \cdot \pi\right) \cdot alphay}{alphax}\right)}^{2}}{{alphay}^{2}}\right)} \cdot \left(1 - u0\right)}}}
\] |
|---|
Applied egg-rr99.4%
\[\leadsto \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \color{blue}{\left(\frac{\left(\left(2 \cdot u1\right) \cdot \left(2 \cdot u1\right) - 0.25\right) \cdot \pi}{2 \cdot u1 - 0.5}\right)}\right)}^{2}}{alphax \cdot alphax} + \frac{{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\]
Proof
[Start]99.4 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphax \cdot alphax} + \frac{{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\] |
|---|
*-commutative [=>]99.4 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \color{blue}{\left(\mathsf{fma}\left(2, u1, 0.5\right) \cdot \pi\right)}\right)}^{2}}{alphax \cdot alphax} + \frac{{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\] |
|---|
fma-udef [=>]99.4 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\color{blue}{\left(2 \cdot u1 + 0.5\right)} \cdot \pi\right)\right)}^{2}}{alphax \cdot alphax} + \frac{{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\] |
|---|
flip-+ [=>]99.4 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\color{blue}{\frac{\left(2 \cdot u1\right) \cdot \left(2 \cdot u1\right) - 0.5 \cdot 0.5}{2 \cdot u1 - 0.5}} \cdot \pi\right)\right)}^{2}}{alphax \cdot alphax} + \frac{{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\] |
|---|
associate-*l/ [=>]99.4 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \color{blue}{\left(\frac{\left(\left(2 \cdot u1\right) \cdot \left(2 \cdot u1\right) - 0.5 \cdot 0.5\right) \cdot \pi}{2 \cdot u1 - 0.5}\right)}\right)}^{2}}{alphax \cdot alphax} + \frac{{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\] |
|---|
metadata-eval [=>]99.4 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\frac{\left(\left(2 \cdot u1\right) \cdot \left(2 \cdot u1\right) - \color{blue}{0.25}\right) \cdot \pi}{2 \cdot u1 - 0.5}\right)\right)}^{2}}{alphax \cdot alphax} + \frac{{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\] |
|---|
Final simplification99.4%
\[\leadsto \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{{\cos \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\frac{\left(\left(2 \cdot u1\right) \cdot \left(2 \cdot u1\right) + -0.25\right) \cdot \pi}{2 \cdot u1 + -0.5}\right)\right)}^{2}}{alphax \cdot alphax} + \frac{{\sin \tan^{-1} \left(\frac{alphay}{alphax} \cdot \tan \left(\pi \cdot \mathsf{fma}\left(2, u1, 0.5\right)\right)\right)}^{2}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\]