Initial program 6.8
\[\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re - \left(x.re \cdot x.im + x.im \cdot x.re\right) \cdot x.im\]
- Using strategy
rm Applied prod-diff6.8
\[\leadsto \color{blue}{(\left(x.re \cdot x.re - x.im \cdot x.im\right) \cdot x.re + \left(-x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)\right))_* + (\left(-x.im\right) \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right) + \left(x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)\right))_*}\]
Simplified0.1
\[\leadsto \color{blue}{(\left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \left(-x.im\right) + \left((\left(x.re \cdot x.im\right) \cdot \left(-x.im\right) + \left({x.re}^{3}\right))_*\right))_*} + (\left(-x.im\right) \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right) + \left(x.im \cdot \left(x.re \cdot x.im + x.im \cdot x.re\right)\right))_*\]
Simplified0.1
\[\leadsto (\left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \left(-x.im\right) + \left((\left(x.re \cdot x.im\right) \cdot \left(-x.im\right) + \left({x.re}^{3}\right))_*\right))_* + \color{blue}{0}\]
Final simplification0.1
\[\leadsto (\left(x.re \cdot \left(x.im + x.im\right)\right) \cdot \left(-x.im\right) + \left((\left(x.re \cdot x.im\right) \cdot \left(-x.im\right) + \left({x.re}^{3}\right))_*\right))_*\]