Initial program 57.7%
\[\sqrt{-\log \left(1 - u1\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Applied egg-rr90.4%
\[\leadsto \sqrt{-\color{blue}{\left(\log \left(1 - u1 \cdot u1\right) + -1 \cdot \mathsf{log1p}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Simplified98.3%
\[\leadsto \sqrt{-\color{blue}{\left(\mathsf{log1p}\left(u1 \cdot \left(-u1\right)\right) - \mathsf{log1p}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Proof
[Start]90.4 | \[ \sqrt{-\left(\log \left(1 - u1 \cdot u1\right) + -1 \cdot \mathsf{log1p}\left(u1\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
mul-1-neg [=>]90.4 | \[ \sqrt{-\left(\log \left(1 - u1 \cdot u1\right) + \color{blue}{\left(-\mathsf{log1p}\left(u1\right)\right)}\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
sub-neg [<=]90.4 | \[ \sqrt{-\color{blue}{\left(\log \left(1 - u1 \cdot u1\right) - \mathsf{log1p}\left(u1\right)\right)}} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
sub-neg [=>]90.4 | \[ \sqrt{-\left(\log \color{blue}{\left(1 + \left(-u1 \cdot u1\right)\right)} - \mathsf{log1p}\left(u1\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
log1p-def [=>]98.3 | \[ \sqrt{-\left(\color{blue}{\mathsf{log1p}\left(-u1 \cdot u1\right)} - \mathsf{log1p}\left(u1\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
distribute-rgt-neg-in [=>]98.3 | \[ \sqrt{-\left(\mathsf{log1p}\left(\color{blue}{u1 \cdot \left(-u1\right)}\right) - \mathsf{log1p}\left(u1\right)\right)} \cdot \sin \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
Taylor expanded in u2 around inf 54.7%
\[\leadsto \color{blue}{\sin \left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}}
\]
Simplified98.3%
\[\leadsto \color{blue}{\sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(u1 \cdot \left(-u1\right)\right)}}
\]
Proof
[Start]54.7 | \[ \sin \left(2 \cdot \left(u2 \cdot \pi\right)\right) \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}
\] |
|---|
associate-*r* [=>]54.7 | \[ \sin \color{blue}{\left(\left(2 \cdot u2\right) \cdot \pi\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}
\] |
|---|
*-commutative [=>]54.7 | \[ \sin \color{blue}{\left(\pi \cdot \left(2 \cdot u2\right)\right)} \cdot \sqrt{\log \left(1 + u1\right) - \log \left(1 + -1 \cdot {u1}^{2}\right)}
\] |
|---|
log1p-def [=>]90.4 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\color{blue}{\mathsf{log1p}\left(u1\right)} - \log \left(1 + -1 \cdot {u1}^{2}\right)}
\] |
|---|
log1p-def [=>]98.3 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \color{blue}{\mathsf{log1p}\left(-1 \cdot {u1}^{2}\right)}}
\] |
|---|
*-commutative [=>]98.3 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(\color{blue}{{u1}^{2} \cdot -1}\right)}
\] |
|---|
unpow2 [=>]98.3 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(\color{blue}{\left(u1 \cdot u1\right)} \cdot -1\right)}
\] |
|---|
associate-*l* [=>]98.3 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(\color{blue}{u1 \cdot \left(u1 \cdot -1\right)}\right)}
\] |
|---|
*-commutative [<=]98.3 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(u1 \cdot \color{blue}{\left(-1 \cdot u1\right)}\right)}
\] |
|---|
mul-1-neg [=>]98.3 | \[ \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(u1 \cdot \color{blue}{\left(-u1\right)}\right)}
\] |
|---|
Final simplification98.3%
\[\leadsto \sin \left(\pi \cdot \left(2 \cdot u2\right)\right) \cdot \sqrt{\mathsf{log1p}\left(u1\right) - \mathsf{log1p}\left(u1 \cdot \left(-u1\right)\right)}
\]