Initial program 60.5%
\[\frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\]
Simplified98.5%
\[\leadsto \color{blue}{\frac{-\mathsf{log1p}\left(-u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}}
\]
Proof
[Start]60.5 | \[ \frac{-\log \left(1 - u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
sub-neg [=>]60.5 | \[ \frac{-\log \color{blue}{\left(1 + \left(-u0\right)\right)}}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
log1p-def [=>]98.5 | \[ \frac{-\color{blue}{\mathsf{log1p}\left(-u0\right)}}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
Applied egg-rr98.4%
\[\leadsto \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{1}{alphax \cdot \left(-alphax\right)} \cdot \left(-cos2phi\right)} + \frac{sin2phi}{alphay \cdot alphay}}
\]
Proof
[Start]98.5 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{cos2phi}{alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
frac-2neg [=>]98.5 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{-cos2phi}{-alphax \cdot alphax}} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
clear-num [=>]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{1}{\frac{-alphax \cdot alphax}{-cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
associate-/r/ [=>]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{1}{-alphax \cdot alphax} \cdot \left(-cos2phi\right)} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
distribute-rgt-neg-in [=>]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{1}{\color{blue}{alphax \cdot \left(-alphax\right)}} \cdot \left(-cos2phi\right) + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
Taylor expanded in alphax around 0 98.4%
\[\leadsto \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{-1}{{alphax}^{2}}} \cdot \left(-cos2phi\right) + \frac{sin2phi}{alphay \cdot alphay}}
\]
Simplified98.4%
\[\leadsto \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{-1}{alphax \cdot alphax}} \cdot \left(-cos2phi\right) + \frac{sin2phi}{alphay \cdot alphay}}
\]
Proof
[Start]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{-1}{{alphax}^{2}} \cdot \left(-cos2phi\right) + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
unpow2 [=>]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{-1}{\color{blue}{alphax \cdot alphax}} \cdot \left(-cos2phi\right) + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
Applied egg-rr98.4%
\[\leadsto \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{1}{\frac{alphax \cdot alphax}{cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}}
\]
Proof
[Start]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{-1}{alphax \cdot alphax} \cdot \left(-cos2phi\right) + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
frac-2neg [=>]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{--1}{-alphax \cdot alphax}} \cdot \left(-cos2phi\right) + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
metadata-eval [=>]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{\color{blue}{1}}{-alphax \cdot alphax} \cdot \left(-cos2phi\right) + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
associate-*l/ [=>]98.5 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{1 \cdot \left(-cos2phi\right)}{-alphax \cdot alphax}} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
*-un-lft-identity [<=]98.5 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{\color{blue}{-cos2phi}}{-alphax \cdot alphax} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
frac-2neg [<=]98.5 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{cos2phi}{alphax \cdot alphax}} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
clear-num [=>]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{1}{\frac{alphax \cdot alphax}{cos2phi}}} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
Simplified98.4%
\[\leadsto \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{1}{alphax \cdot alphax} \cdot cos2phi} + \frac{sin2phi}{alphay \cdot alphay}}
\]
Proof
[Start]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{1}{\frac{alphax \cdot alphax}{cos2phi}} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
associate-/r/ [=>]98.4 | \[ \frac{-\mathsf{log1p}\left(-u0\right)}{\color{blue}{\frac{1}{alphax \cdot alphax} \cdot cos2phi} + \frac{sin2phi}{alphay \cdot alphay}}
\] |
|---|
Final simplification98.4%
\[\leadsto \frac{-\mathsf{log1p}\left(-u0\right)}{\frac{1}{alphax \cdot alphax} \cdot cos2phi + \frac{sin2phi}{alphay \cdot alphay}}
\]