Initial program 85.9%
\[\left(\left(x \cdot 3\right) \cdot x\right) \cdot y
\]
Step-by-step derivation
*-commutative85.9%
\[\leadsto \left(\color{blue}{\left(3 \cdot x\right)} \cdot x\right) \cdot y
\]
associate-*l*85.9%
\[\leadsto \color{blue}{\left(3 \cdot \left(x \cdot x\right)\right)} \cdot y
\]
Simplified85.9%
\[\leadsto \color{blue}{\left(3 \cdot \left(x \cdot x\right)\right) \cdot y}
\]
Step-by-step derivation
associate-*r*85.9%
\[\leadsto \color{blue}{\left(\left(3 \cdot x\right) \cdot x\right)} \cdot y
\]
*-commutative85.9%
\[\leadsto \left(\color{blue}{\left(x \cdot 3\right)} \cdot x\right) \cdot y
\]
associate-*r*99.7%
\[\leadsto \color{blue}{\left(x \cdot 3\right) \cdot \left(x \cdot y\right)}
\]
expm1-log1p-u73.0%
\[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\left(x \cdot 3\right) \cdot \left(x \cdot y\right)\right)\right)}
\]
expm1-udef52.8%
\[\leadsto \color{blue}{e^{\mathsf{log1p}\left(\left(x \cdot 3\right) \cdot \left(x \cdot y\right)\right)} - 1}
\]
log1p-udef52.8%
\[\leadsto e^{\color{blue}{\log \left(1 + \left(x \cdot 3\right) \cdot \left(x \cdot y\right)\right)}} - 1
\]
add-exp-log79.5%
\[\leadsto \color{blue}{\left(1 + \left(x \cdot 3\right) \cdot \left(x \cdot y\right)\right)} - 1
\]
*-commutative79.5%
\[\leadsto \left(1 + \color{blue}{\left(3 \cdot x\right)} \cdot \left(x \cdot y\right)\right) - 1
\]
associate-*l*79.5%
\[\leadsto \left(1 + \color{blue}{3 \cdot \left(x \cdot \left(x \cdot y\right)\right)}\right) - 1
\]
Applied egg-rr79.5%
\[\leadsto \color{blue}{\left(1 + 3 \cdot \left(x \cdot \left(x \cdot y\right)\right)\right) - 1}
\]
Step-by-step derivation
add-exp-log52.7%
\[\leadsto \color{blue}{e^{\log \left(\left(1 + 3 \cdot \left(x \cdot \left(x \cdot y\right)\right)\right) - 1\right)}}
\]
associate--l+52.7%
\[\leadsto e^{\log \color{blue}{\left(1 + \left(3 \cdot \left(x \cdot \left(x \cdot y\right)\right) - 1\right)\right)}}
\]
log1p-def52.7%
\[\leadsto e^{\color{blue}{\mathsf{log1p}\left(3 \cdot \left(x \cdot \left(x \cdot y\right)\right) - 1\right)}}
\]
add-exp-log51.4%
\[\leadsto e^{\mathsf{log1p}\left(\color{blue}{e^{\log \left(3 \cdot \left(x \cdot \left(x \cdot y\right)\right)\right)}} - 1\right)}
\]
expm1-def51.4%
\[\leadsto e^{\mathsf{log1p}\left(\color{blue}{\mathsf{expm1}\left(\log \left(3 \cdot \left(x \cdot \left(x \cdot y\right)\right)\right)\right)}\right)}
\]
log1p-expm1-u61.4%
\[\leadsto e^{\color{blue}{\log \left(3 \cdot \left(x \cdot \left(x \cdot y\right)\right)\right)}}
\]
*-commutative61.4%
\[\leadsto e^{\log \color{blue}{\left(\left(x \cdot \left(x \cdot y\right)\right) \cdot 3\right)}}
\]
associate-*r*54.8%
\[\leadsto e^{\log \left(\color{blue}{\left(\left(x \cdot x\right) \cdot y\right)} \cdot 3\right)}
\]
associate-*r*54.8%
\[\leadsto e^{\log \color{blue}{\left(\left(x \cdot x\right) \cdot \left(y \cdot 3\right)\right)}}
\]
*-commutative54.8%
\[\leadsto e^{\log \left(\left(x \cdot x\right) \cdot \color{blue}{\left(3 \cdot y\right)}\right)}
\]
add-exp-log85.9%
\[\leadsto \color{blue}{\left(x \cdot x\right) \cdot \left(3 \cdot y\right)}
\]
*-commutative85.9%
\[\leadsto \color{blue}{\left(3 \cdot y\right) \cdot \left(x \cdot x\right)}
\]
associate-*l*85.9%
\[\leadsto \color{blue}{3 \cdot \left(y \cdot \left(x \cdot x\right)\right)}
\]
associate-*l*99.6%
\[\leadsto 3 \cdot \color{blue}{\left(\left(y \cdot x\right) \cdot x\right)}
\]
*-commutative99.6%
\[\leadsto 3 \cdot \left(\color{blue}{\left(x \cdot y\right)} \cdot x\right)
\]
associate-*r*99.7%
\[\leadsto \color{blue}{\left(3 \cdot \left(x \cdot y\right)\right) \cdot x}
\]
Applied egg-rr99.7%
\[\leadsto \color{blue}{\left(3 \cdot \left(x \cdot y\right)\right) \cdot x}
\]
Final simplification99.7%
\[\leadsto x \cdot \left(3 \cdot \left(x \cdot y\right)\right)
\]