Initial program 15.3
\[x \cdot \log \left(\frac{x}{y}\right) - z
\]
Applied egg-rr15.4
\[\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
\]
Simplified15.4
\[\leadsto x \cdot \color{blue}{\left(\log \left(\sqrt[3]{\frac{x}{y}}\right) \cdot 3\right)} - z
\]
Proof
(*.f64 (log.f64 (cbrt.f64 (/.f64 x y))) 3): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 3 (log.f64 (cbrt.f64 (/.f64 x y))))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= metadata-eval (+.f64 2 1)) (log.f64 (cbrt.f64 (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 2 (log.f64 (cbrt.f64 (/.f64 x y)))) (log.f64 (cbrt.f64 (/.f64 x y))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= log-pow_binary64 (log.f64 (pow.f64 (cbrt.f64 (/.f64 x y)) 2))) (log.f64 (cbrt.f64 (/.f64 x y)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr15.4
\[\leadsto \color{blue}{\mathsf{fma}\left(x \cdot 3, \log \left(\sqrt[3]{\frac{x}{y}}\right), -z\right)}
\]
Applied egg-rr0.2
\[\leadsto \mathsf{fma}\left(x \cdot 3, \log \color{blue}{\left(\sqrt[3]{x} \cdot \frac{1}{\sqrt[3]{y}}\right)}, -z\right)
\]
Simplified0.2
\[\leadsto \mathsf{fma}\left(x \cdot 3, \log \color{blue}{\left(\frac{\sqrt[3]{x}}{\sqrt[3]{y}}\right)}, -z\right)
\]
Proof
(/.f64 (cbrt.f64 x) (cbrt.f64 y)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (cbrt.f64 x) 1)) (cbrt.f64 y)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (cbrt.f64 x) (/.f64 1 (cbrt.f64 y)))): 36 points increase in error, 38 points decrease in error
Final simplification0.2
\[\leadsto \mathsf{fma}\left(x \cdot 3, \log \left(\frac{\sqrt[3]{x}}{\sqrt[3]{y}}\right), -z\right)
\]