Initial program 13.8
\[\sqrt{-\log \left(1 - u1\right)} \cdot \cos \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 \cos \left(\left(2 \cdot \pi\right) \cdot u2\right)
\]
Simplified0.9
\[\leadsto \sqrt{-\color{blue}{\left(\log \left(1 - {u1}^{3}\right) - \mathsf{log1p}\left(\mathsf{fma}\left(u1, u1, u1\right)\right)\right)}} \cdot \cos \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 \cos \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
log1p-def [=>]0.9 | \[ \sqrt{-\left(\log \left(1 - {u1}^{3}\right) - \color{blue}{\mathsf{log1p}\left(\mathsf{fma}\left(u1, u1, u1\right)\right)}\right)} \cdot \cos \left(\left(2 \cdot \pi\right) \cdot u2\right)
\] |
|---|
Taylor expanded in u2 around inf 14.8
\[\leadsto \color{blue}{\sqrt{\log \left({u1}^{2} + \left(1 + u1\right)\right) - \log \left(1 - {u1}^{3}\right)} \cdot \cos \left(2 \cdot \left(u2 \cdot \pi\right)\right)}
\]
Simplified14.8
\[\leadsto \color{blue}{\cos \left(\left(2 \cdot u2\right) \cdot \pi\right) \cdot \sqrt{\log \left(u1 \cdot u1 + \left(u1 + 1\right)\right) - \log \left(1 - {u1}^{3}\right)}}
\]
Proof
[Start]14.8 | \[ \sqrt{\log \left({u1}^{2} + \left(1 + u1\right)\right) - \log \left(1 - {u1}^{3}\right)} \cdot \cos \left(2 \cdot \left(u2 \cdot \pi\right)\right)
\] |
|---|
*-commutative [=>]14.8 | \[ \color{blue}{\cos \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 | \[ \cos \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)}
\] |
|---|
unpow2 [=>]14.8 | \[ \cos \left(\left(2 \cdot u2\right) \cdot \pi\right) \cdot \sqrt{\log \left(\color{blue}{u1 \cdot u1} + \left(1 + u1\right)\right) - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
+-commutative [=>]14.8 | \[ \cos \left(\left(2 \cdot u2\right) \cdot \pi\right) \cdot \sqrt{\log \left(u1 \cdot u1 + \color{blue}{\left(u1 + 1\right)}\right) - \log \left(1 - {u1}^{3}\right)}
\] |
|---|
Applied egg-rr14.5
\[\leadsto \color{blue}{\sqrt[3]{{\cos \left(2 \cdot \left(u2 \cdot \pi\right)\right)}^{3} \cdot {\log \left(\frac{1}{1 - u1}\right)}^{1.5}}}
\]
Simplified0.3
\[\leadsto \color{blue}{\sqrt[3]{{\cos \left(u2 \cdot \left(2 \cdot \pi\right)\right)}^{3} \cdot {\left(-\mathsf{log1p}\left(-u1\right)\right)}^{1.5}}}
\]
Proof
[Start]14.5 | \[ \sqrt[3]{{\cos \left(2 \cdot \left(u2 \cdot \pi\right)\right)}^{3} \cdot {\log \left(\frac{1}{1 - u1}\right)}^{1.5}}
\] |
|---|
associate-*r* [=>]14.5 | \[ \sqrt[3]{{\cos \color{blue}{\left(\left(2 \cdot u2\right) \cdot \pi\right)}}^{3} \cdot {\log \left(\frac{1}{1 - u1}\right)}^{1.5}}
\] |
|---|
*-commutative [=>]14.5 | \[ \sqrt[3]{{\cos \left(\color{blue}{\left(u2 \cdot 2\right)} \cdot \pi\right)}^{3} \cdot {\log \left(\frac{1}{1 - u1}\right)}^{1.5}}
\] |
|---|
associate-*l* [=>]14.5 | \[ \sqrt[3]{{\cos \color{blue}{\left(u2 \cdot \left(2 \cdot \pi\right)\right)}}^{3} \cdot {\log \left(\frac{1}{1 - u1}\right)}^{1.5}}
\] |
|---|
log-rec [=>]13.8 | \[ \sqrt[3]{{\cos \left(u2 \cdot \left(2 \cdot \pi\right)\right)}^{3} \cdot {\color{blue}{\left(-\log \left(1 - u1\right)\right)}}^{1.5}}
\] |
|---|
sub-neg [=>]13.8 | \[ \sqrt[3]{{\cos \left(u2 \cdot \left(2 \cdot \pi\right)\right)}^{3} \cdot {\left(-\log \color{blue}{\left(1 + \left(-u1\right)\right)}\right)}^{1.5}}
\] |
|---|
log1p-def [=>]0.3 | \[ \sqrt[3]{{\cos \left(u2 \cdot \left(2 \cdot \pi\right)\right)}^{3} \cdot {\left(-\color{blue}{\mathsf{log1p}\left(-u1\right)}\right)}^{1.5}}
\] |
|---|
Final simplification0.3
\[\leadsto \sqrt[3]{{\cos \left(u2 \cdot \left(2 \cdot \pi\right)\right)}^{3} \cdot {\left(-\mathsf{log1p}\left(-u1\right)\right)}^{1.5}}
\]