Initial program 0.1
\[\left(\left(x \cdot \log y - y\right) - z\right) + \log t\]
- Using strategy
rm Applied flip3-+45.4
\[\leadsto \color{blue}{\frac{{\left(\left(x \cdot \log y - y\right) - z\right)}^{3} + {\left(\log t\right)}^{3}}{\left(\left(x \cdot \log y - y\right) - z\right) \cdot \left(\left(x \cdot \log y - y\right) - z\right) + \left(\log t \cdot \log t - \left(\left(x \cdot \log y - y\right) - z\right) \cdot \log t\right)}}\]
Simplified45.4
\[\leadsto \frac{{\left(\left(x \cdot \log y - y\right) - z\right)}^{3} + {\left(\log t\right)}^{3}}{\color{blue}{\mathsf{fma}\left(\left(x \cdot \log y - z\right) - y, \left(\left(x \cdot \log y - y\right) - z\right) - \log t, \log t \cdot \log t\right)}}\]
- Using strategy
rm Applied clear-num45.4
\[\leadsto \color{blue}{\frac{1}{\frac{\mathsf{fma}\left(\left(x \cdot \log y - z\right) - y, \left(\left(x \cdot \log y - y\right) - z\right) - \log t, \log t \cdot \log t\right)}{{\left(\left(x \cdot \log y - y\right) - z\right)}^{3} + {\left(\log t\right)}^{3}}}}\]
- Using strategy
rm Applied sum-cubes45.4
\[\leadsto \frac{1}{\frac{\mathsf{fma}\left(\left(x \cdot \log y - z\right) - y, \left(\left(x \cdot \log y - y\right) - z\right) - \log t, \log t \cdot \log t\right)}{\color{blue}{\left(\left(\left(x \cdot \log y - y\right) - z\right) \cdot \left(\left(x \cdot \log y - y\right) - z\right) + \left(\log t \cdot \log t - \left(\left(x \cdot \log y - y\right) - z\right) \cdot \log t\right)\right) \cdot \left(\left(\left(x \cdot \log y - y\right) - z\right) + \log t\right)}}}\]
Applied associate-/r*37.2
\[\leadsto \frac{1}{\color{blue}{\frac{\frac{\mathsf{fma}\left(\left(x \cdot \log y - z\right) - y, \left(\left(x \cdot \log y - y\right) - z\right) - \log t, \log t \cdot \log t\right)}{\left(\left(x \cdot \log y - y\right) - z\right) \cdot \left(\left(x \cdot \log y - y\right) - z\right) + \left(\log t \cdot \log t - \left(\left(x \cdot \log y - y\right) - z\right) \cdot \log t\right)}}{\left(\left(x \cdot \log y - y\right) - z\right) + \log t}}}\]
Simplified0.2
\[\leadsto \frac{1}{\frac{\color{blue}{1}}{\left(\left(x \cdot \log y - y\right) - z\right) + \log t}}\]
- Using strategy
rm Applied div-inv0.2
\[\leadsto \color{blue}{1 \cdot \frac{1}{\frac{1}{\left(\left(x \cdot \log y - y\right) - z\right) + \log t}}}\]
Simplified0.1
\[\leadsto 1 \cdot \color{blue}{\left(\mathsf{fma}\left(x, \log y, \log t\right) - \left(y + z\right)\right)}\]
Final simplification0.1
\[\leadsto \mathsf{fma}\left(x, \log y, \log t\right) - \left(y + z\right)\]