- Started with
\[\left(\left(\left(e + d\right) + c\right) + b\right) + a\]
0.4
- Using strategy
rm 0.4
- Applied associate-+l+ to get
\[\color{red}{\left(\left(\left(e + d\right) + c\right) + b\right)} + a \leadsto \color{blue}{\left(\left(e + d\right) + \left(c + b\right)\right)} + a\]
0.4
- Using strategy
rm 0.4
- Applied add-log-exp to get
\[\left(\left(e + d\right) + \color{red}{\left(c + b\right)}\right) + a \leadsto \left(\left(e + d\right) + \color{blue}{\log \left(e^{c + b}\right)}\right) + a\]
0.4
- Applied add-log-exp to get
\[\left(\color{red}{\left(e + d\right)} + \log \left(e^{c + b}\right)\right) + a \leadsto \left(\color{blue}{\log \left(e^{e + d}\right)} + \log \left(e^{c + b}\right)\right) + a\]
0.4
- Applied sum-log to get
\[\color{red}{\left(\log \left(e^{e + d}\right) + \log \left(e^{c + b}\right)\right)} + a \leadsto \color{blue}{\log \left(e^{e + d} \cdot e^{c + b}\right)} + a\]
0.4
- Applied simplify to get
\[\log \color{red}{\left(e^{e + d} \cdot e^{c + b}\right)} + a \leadsto \log \color{blue}{\left(e^{\left(d + b\right) + \left(c + e\right)}\right)} + a\]
0.3
- Using strategy
rm 0.3
- Applied exp-sum to get
\[\log \color{red}{\left(e^{\left(d + b\right) + \left(c + e\right)}\right)} + a \leadsto \log \color{blue}{\left(e^{d + b} \cdot e^{c + e}\right)} + a\]
0.3
- Applied log-prod to get
\[\color{red}{\log \left(e^{d + b} \cdot e^{c + e}\right)} + a \leadsto \color{blue}{\left(\log \left(e^{d + b}\right) + \log \left(e^{c + e}\right)\right)} + a\]
0.3
- Applied associate-+l+ to get
\[\color{red}{\left(\log \left(e^{d + b}\right) + \log \left(e^{c + e}\right)\right) + a} \leadsto \color{blue}{\log \left(e^{d + b}\right) + \left(\log \left(e^{c + e}\right) + a\right)}\]
0.3
- Applied simplify to get
\[\log \left(e^{d + b}\right) + \color{red}{\left(\log \left(e^{c + e}\right) + a\right)} \leadsto \log \left(e^{d + b}\right) + \color{blue}{\left(e + \left(c + a\right)\right)}\]
0.2