Initial program 4.7
\[x + \left(y \cdot z\right) \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\]
- Using strategy
rm Applied associate-*l*2.2
\[\leadsto x + \color{blue}{y \cdot \left(z \cdot \left(\tanh \left(\frac{t}{y}\right) - \tanh \left(\frac{x}{y}\right)\right)\right)}\]
- Using strategy
rm Applied sub-neg2.2
\[\leadsto x + y \cdot \left(z \cdot \color{blue}{\left(\tanh \left(\frac{t}{y}\right) + \left(-\tanh \left(\frac{x}{y}\right)\right)\right)}\right)\]
Applied distribute-lft-in2.2
\[\leadsto x + y \cdot \color{blue}{\left(z \cdot \tanh \left(\frac{t}{y}\right) + z \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)\right)}\]
Applied distribute-lft-in2.3
\[\leadsto x + \color{blue}{\left(y \cdot \left(z \cdot \tanh \left(\frac{t}{y}\right)\right) + y \cdot \left(z \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)\right)\right)}\]
Simplified2.3
\[\leadsto x + \left(\color{blue}{y \cdot \left(\tanh \left(\frac{t}{y}\right) \cdot z\right)} + y \cdot \left(z \cdot \left(-\tanh \left(\frac{x}{y}\right)\right)\right)\right)\]
Simplified2.3
\[\leadsto x + \left(y \cdot \left(\tanh \left(\frac{t}{y}\right) \cdot z\right) + \color{blue}{y \cdot \left(\left(-\tanh \left(\frac{x}{y}\right)\right) \cdot z\right)}\right)\]
Final simplification2.3
\[\leadsto x + \left(y \cdot \left(\tanh \left(\frac{t}{y}\right) \cdot z\right) + y \cdot \left(\left(-\tanh \left(\frac{x}{y}\right)\right) \cdot z\right)\right)\]
