Initial program 13.8
\[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Applied egg-rr14.7
\[\leadsto \sqrt{-\color{blue}{\left(\log \left(1 - {u1}^{3}\right) - \log \left(1 + \mathsf{fma}\left(u1, u1, u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Simplified0.5
\[\leadsto \sqrt{-\color{blue}{\left(\mathsf{log1p}\left(-{u1}^{3}\right) - \mathsf{log1p}\left(\mathsf{fma}\left(u1, u1, u1\right)\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Proof
[Start]14.7 | \[ \sqrt{-\left(\log \left(1 - {u1}^{3}\right) - \log \left(1 + \mathsf{fma}\left(u1, u1, u1\right)\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
sub-neg [=>]14.7 | \[ \sqrt{-\left(\log \color{blue}{\left(1 + \left(-{u1}^{3}\right)\right)} - \log \left(1 + \mathsf{fma}\left(u1, u1, u1\right)\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
log1p-def [=>]14.2 | \[ \sqrt{-\left(\color{blue}{\mathsf{log1p}\left(-{u1}^{3}\right)} - \log \left(1 + \mathsf{fma}\left(u1, u1, u1\right)\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
log1p-def [=>]0.5 | \[ \sqrt{-\left(\mathsf{log1p}\left(-{u1}^{3}\right) - \color{blue}{\mathsf{log1p}\left(\mathsf{fma}\left(u1, u1, u1\right)\right)}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
Taylor expanded in u2 around inf 14.8
\[\leadsto \color{blue}{\sin \left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot \sqrt{\log \left({u1}^{2} + \left(1 + u1\right)\right) - \log \left(1 - {u1}^{3}\right)}}
\]
Simplified0.5
\[\leadsto \color{blue}{\sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(\mathsf{fma}\left(u1, u1, u1\right)\right) - \mathsf{log1p}\left(-{u1}^{3}\right)}}
\]
Proof
[Start]14.8 | \[ \sin \left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot \sqrt{\log \left({u1}^{2} + \left(1 + u1\right)\right) - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
associate-*r* [=>]14.8 | \[ \sin \color{blue}{\left(\left(2 \cdot u2\right) \cdot \pi\right)} \cdot \sqrt{\log \left({u1}^{2} + \left(1 + u1\right)\right) - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
*-commutative [=>]14.8 | \[ \sin \color{blue}{\left(\pi \cdot \left(2 \cdot u2\right)\right)} \cdot \sqrt{\log \left({u1}^{2} + \left(1 + u1\right)\right) - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
associate-+r+ [=>]14.7 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\log \color{blue}{\left(\left({u1}^{2} + 1\right) + u1\right)} - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
+-commutative [=>]14.7 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\log \left(\color{blue}{\left(1 + {u1}^{2}\right)} + u1\right) - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
associate-+r+ [<=]14.7 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\log \color{blue}{\left(1 + \left({u1}^{2} + u1\right)\right)} - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
unpow2 [=>]14.7 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\log \left(1 + \left(\color{blue}{u1 \cdot u1} + u1\right)\right) - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
fma-udef [<=]14.7 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\log \left(1 + \color{blue}{\mathsf{fma}\left(u1, u1, u1\right)}\right) - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
log1p-def [=>]1.1 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\color{blue}{\mathsf{log1p}\left(\mathsf{fma}\left(u1, u1, u1\right)\right)} - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
sub-neg [=>]1.1 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(\mathsf{fma}\left(u1, u1, u1\right)\right) - \log \color{blue}{\left(1 + \left(-{u1}^{3}\right)\right)}}
\] |
|---|
log1p-def [=>]0.5 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(\mathsf{fma}\left(u1, u1, u1\right)\right) - \color{blue}{\mathsf{log1p}\left(-{u1}^{3}\right)}}
\] |
|---|
Final simplification0.5
\[\leadsto \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(\mathsf{fma}\left(u1, u1, u1\right)\right) - \mathsf{log1p}\left(-{u1}^{3}\right)}
\]