Initial program 75.9%
\[x \cdot \log \left(\frac{x}{y}\right) - z
\]
Applied egg-rr75.8%
\[\leadsto x \cdot \color{blue}{\left(\log \left({\left(\sqrt[3]{\frac{x}{y}}\right)}^{2}\right) + \log \left(\sqrt[3]{\frac{x}{y}}\right)\right)} - z
\]
Proof
[Start]75.9 | \[ x \cdot \log \left(\frac{x}{y}\right) - z
\] |
|---|
add-cube-cbrt [=>]75.9 | \[ x \cdot \log \color{blue}{\left(\left(\sqrt[3]{\frac{x}{y}} \cdot \sqrt[3]{\frac{x}{y}}\right) \cdot \sqrt[3]{\frac{x}{y}}\right)} - z
\] |
|---|
log-prod [=>]75.8 | \[ x \cdot \color{blue}{\left(\log \left(\sqrt[3]{\frac{x}{y}} \cdot \sqrt[3]{\frac{x}{y}}\right) + \log \left(\sqrt[3]{\frac{x}{y}}\right)\right)} - z
\] |
|---|
pow2 [=>]75.8 | \[ x \cdot \left(\log \color{blue}{\left({\left(\sqrt[3]{\frac{x}{y}}\right)}^{2}\right)} + \log \left(\sqrt[3]{\frac{x}{y}}\right)\right) - z
\] |
|---|
Simplified75.8%
\[\leadsto x \cdot \color{blue}{\left(\log \left(\sqrt[3]{\frac{x}{y}}\right) \cdot 3\right)} - z
\]
Proof
[Start]75.8 | \[ x \cdot \left(\log \left({\left(\sqrt[3]{\frac{x}{y}}\right)}^{2}\right) + \log \left(\sqrt[3]{\frac{x}{y}}\right)\right) - z
\] |
|---|
log-pow [=>]75.8 | \[ x \cdot \left(\color{blue}{2 \cdot \log \left(\sqrt[3]{\frac{x}{y}}\right)} + \log \left(\sqrt[3]{\frac{x}{y}}\right)\right) - z
\] |
|---|
*-lft-identity [<=]75.8 | \[ x \cdot \left(2 \cdot \log \left(\sqrt[3]{\frac{x}{y}}\right) + \color{blue}{1 \cdot \log \left(\sqrt[3]{\frac{x}{y}}\right)}\right) - z
\] |
|---|
distribute-rgt-out [=>]75.8 | \[ x \cdot \color{blue}{\left(\log \left(\sqrt[3]{\frac{x}{y}}\right) \cdot \left(2 + 1\right)\right)} - z
\] |
|---|
metadata-eval [=>]75.8 | \[ x \cdot \left(\log \left(\sqrt[3]{\frac{x}{y}}\right) \cdot \color{blue}{3}\right) - z
\] |
|---|
Applied egg-rr75.8%
\[\leadsto \color{blue}{\mathsf{fma}\left(x \cdot \log \left(\sqrt[3]{\frac{x}{y}}\right), 3, -z\right)}
\]
Proof
[Start]75.8 | \[ x \cdot \left(\log \left(\sqrt[3]{\frac{x}{y}}\right) \cdot 3\right) - z
\] |
|---|
associate-*r* [=>]75.8 | \[ \color{blue}{\left(x \cdot \log \left(\sqrt[3]{\frac{x}{y}}\right)\right) \cdot 3} - z
\] |
|---|
fma-neg [=>]75.8 | \[ \color{blue}{\mathsf{fma}\left(x \cdot \log \left(\sqrt[3]{\frac{x}{y}}\right), 3, -z\right)}
\] |
|---|
Applied egg-rr99.7%
\[\leadsto \mathsf{fma}\left(x \cdot \log \color{blue}{\left(\sqrt[3]{x} \cdot \frac{1}{\sqrt[3]{y}}\right)}, 3, -z\right)
\]
Proof
[Start]75.8 | \[ \mathsf{fma}\left(x \cdot \log \left(\sqrt[3]{\frac{x}{y}}\right), 3, -z\right)
\] |
|---|
cbrt-div [=>]99.7 | \[ \mathsf{fma}\left(x \cdot \log \color{blue}{\left(\frac{\sqrt[3]{x}}{\sqrt[3]{y}}\right)}, 3, -z\right)
\] |
|---|
div-inv [=>]99.7 | \[ \mathsf{fma}\left(x \cdot \log \color{blue}{\left(\sqrt[3]{x} \cdot \frac{1}{\sqrt[3]{y}}\right)}, 3, -z\right)
\] |
|---|
Simplified99.7%
\[\leadsto \mathsf{fma}\left(x \cdot \log \color{blue}{\left(\frac{\sqrt[3]{x}}{\sqrt[3]{y}}\right)}, 3, -z\right)
\]
Proof
[Start]99.7 | \[ \mathsf{fma}\left(x \cdot \log \left(\sqrt[3]{x} \cdot \frac{1}{\sqrt[3]{y}}\right), 3, -z\right)
\] |
|---|
associate-*r/ [=>]99.7 | \[ \mathsf{fma}\left(x \cdot \log \color{blue}{\left(\frac{\sqrt[3]{x} \cdot 1}{\sqrt[3]{y}}\right)}, 3, -z\right)
\] |
|---|
*-rgt-identity [=>]99.7 | \[ \mathsf{fma}\left(x \cdot \log \left(\frac{\color{blue}{\sqrt[3]{x}}}{\sqrt[3]{y}}\right), 3, -z\right)
\] |
|---|
Final simplification99.7%
\[\leadsto \mathsf{fma}\left(x \cdot \log \left(\frac{\sqrt[3]{x}}{\sqrt[3]{y}}\right), 3, -z\right)
\]