Initial program 0.2
\[\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}}}
\]
Simplified0.2
\[\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]0.2 | \[ \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 0.2
\[\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)}}}
\]
Simplified0.2
\[\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]0.2 | \[ \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 [=>]0.2 | \[ \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-rr0.2
\[\leadsto \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{\color{blue}{\frac{1}{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)}}}
\]
Simplified0.2
\[\leadsto \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{\color{blue}{\frac{1}{1 + {\left(\frac{alphay}{alphax} \cdot \tan \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)}}}
\]
Proof
[Start]0.2 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{\frac{1}{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 [=>]0.2 | \[ \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{\frac{1}{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)}}}
\] |
|---|
Applied egg-rr0.2
\[\leadsto \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{\frac{1}{1 + {\left(\frac{alphay}{alphax} \cdot \tan \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 \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}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\]
Final simplification0.2
\[\leadsto \frac{1}{\sqrt{1 + \frac{u0}{\left(\frac{\frac{1}{1 + {\left(\frac{alphay}{alphax} \cdot \tan \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(\frac{\pi \cdot \left(\left(2 \cdot u1\right) \cdot \left(2 \cdot u1\right) + -0.25\right)}{2 \cdot u1 + -0.5}\right)\right)}^{2}}{alphay \cdot alphay}\right) \cdot \left(1 - u0\right)}}}
\]