\((\left(a - 0.5\right) * \left(\log t\right) + \left(\log \left(x + y\right)\right))_* + \left(\log z - t\right)\)
- Started with
\[\left(\left(\log \left(x + y\right) + \log z\right) - t\right) + \left(a - 0.5\right) \cdot \log t\]
0.2
- Applied simplify to get
\[\color{red}{\left(\left(\log \left(x + y\right) + \log z\right) - t\right) + \left(a - 0.5\right) \cdot \log t} \leadsto \color{blue}{\log \left(x + y\right) + \left((\left(a - 0.5\right) * \left(\log t\right) + \left(\log z\right))_* - t\right)}\]
0.3
- Using strategy
rm 0.3
- Applied fma-udef to get
\[\log \left(x + y\right) + \left(\color{red}{(\left(a - 0.5\right) * \left(\log t\right) + \left(\log z\right))_*} - t\right) \leadsto \log \left(x + y\right) + \left(\color{blue}{\left(\left(a - 0.5\right) \cdot \log t + \log z\right)} - t\right)\]
0.3
- Applied associate--l+ to get
\[\log \left(x + y\right) + \color{red}{\left(\left(\left(a - 0.5\right) \cdot \log t + \log z\right) - t\right)} \leadsto \log \left(x + y\right) + \color{blue}{\left(\left(a - 0.5\right) \cdot \log t + \left(\log z - t\right)\right)}\]
0.3
- Applied associate-+r+ to get
\[\color{red}{\log \left(x + y\right) + \left(\left(a - 0.5\right) \cdot \log t + \left(\log z - t\right)\right)} \leadsto \color{blue}{\left(\log \left(x + y\right) + \left(a - 0.5\right) \cdot \log t\right) + \left(\log z - t\right)}\]
0.3
- Applied simplify to get
\[\color{red}{\left(\log \left(x + y\right) + \left(a - 0.5\right) \cdot \log t\right)} + \left(\log z - t\right) \leadsto \color{blue}{(\left(a - 0.5\right) * \left(\log t\right) + \left(\log \left(x + y\right)\right))_*} + \left(\log z - t\right)\]
0.3
- Removed slow pow expressions