- Started with
\[(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)\]
12.7
- Using strategy
rm 12.7
- Applied associate--r+ to get
\[\color{red}{(x * y + z)_* - \left(1 + \left(x \cdot y + z\right)\right)} \leadsto \color{blue}{\left((x * y + z)_* - 1\right) - \left(x \cdot y + z\right)}\]
9.9
- Using strategy
rm 9.9
- Applied associate--r+ to get
\[\color{red}{\left((x * y + z)_* - 1\right) - \left(x \cdot y + z\right)} \leadsto \color{blue}{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right) - z}\]
10.3
- Using strategy
rm 10.3
- Applied flip3-- to get
\[\color{red}{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right) - z} \leadsto \color{blue}{\frac{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^{3} - {z}^{3}}{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^2 + \left({z}^2 + \left(\left((x * y + z)_* - 1\right) - x \cdot y\right) \cdot z\right)}}\]
10.5
- Applied simplify to get
\[\frac{\color{red}{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^{3} - {z}^{3}}}{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^2 + \left({z}^2 + \left(\left((x * y + z)_* - 1\right) - x \cdot y\right) \cdot z\right)} \leadsto \frac{\color{blue}{{\left(\left((x * y + z)_* - 1\right) - y \cdot x\right)}^3 - {z}^3}}{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^2 + \left({z}^2 + \left(\left((x * y + z)_* - 1\right) - x \cdot y\right) \cdot z\right)}\]
10.4
- Applied taylor to get
\[\frac{{\left(\left((x * y + z)_* - 1\right) - y \cdot x\right)}^3 - {z}^3}{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^2 + \left({z}^2 + \left(\left((x * y + z)_* - 1\right) - x \cdot y\right) \cdot z\right)} \leadsto \frac{{\left(\left((x * y + z)_* - 1\right) - y \cdot x\right)}^3 - {z}^3}{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^2 + \left({z}^2 + \left((x * y + z)_* - \left(y \cdot x + 1\right)\right) \cdot z\right)}\]
10.3
- Taylor expanded around 0 to get
\[\frac{{\left(\left((x * y + z)_* - 1\right) - y \cdot x\right)}^3 - {z}^3}{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^2 + \left({z}^2 + \color{red}{\left((x * y + z)_* - \left(y \cdot x + 1\right)\right)} \cdot z\right)} \leadsto \frac{{\left(\left((x * y + z)_* - 1\right) - y \cdot x\right)}^3 - {z}^3}{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^2 + \left({z}^2 + \color{blue}{\left((x * y + z)_* - \left(y \cdot x + 1\right)\right)} \cdot z\right)}\]
10.3
- Applied simplify to get
\[\frac{{\left(\left((x * y + z)_* - 1\right) - y \cdot x\right)}^3 - {z}^3}{{\left(\left((x * y + z)_* - 1\right) - x \cdot y\right)}^2 + \left({z}^2 + \left((x * y + z)_* - \left(y \cdot x + 1\right)\right) \cdot z\right)} \leadsto \frac{{\left(\left((x * y + z)_* - y \cdot x\right) - 1\right)}^3 - {z}^3}{z \cdot \left(\left((x * y + z)_* - 1\right) - \left(y \cdot x - z\right)\right) + {\left(\left((x * y + z)_* - y \cdot x\right) - 1\right)}^2}\]
5.1
- Applied final simplification