Initial program 0.1
\[\left(\frac{m \cdot \left(1 - m\right)}{v} - 1\right) \cdot \left(1 - m\right)\]
Initial simplification0.1
\[\leadsto (\left(1 - m\right) \cdot \left(\frac{m}{v}\right) + -1)_* \cdot \left(1 - m\right)\]
- Using strategy
rm Applied sub-neg0.1
\[\leadsto (\left(1 - m\right) \cdot \left(\frac{m}{v}\right) + -1)_* \cdot \color{blue}{\left(1 + \left(-m\right)\right)}\]
Applied distribute-rgt-in0.1
\[\leadsto \color{blue}{1 \cdot (\left(1 - m\right) \cdot \left(\frac{m}{v}\right) + -1)_* + \left(-m\right) \cdot (\left(1 - m\right) \cdot \left(\frac{m}{v}\right) + -1)_*}\]
Simplified0.1
\[\leadsto 1 \cdot (\left(1 - m\right) \cdot \left(\frac{m}{v}\right) + -1)_* + \color{blue}{(\left(\frac{m}{v}\right) \cdot \left(m \cdot \left(-1 + m\right)\right) + m)_*}\]
- Using strategy
rm Applied *-un-lft-identity0.1
\[\leadsto 1 \cdot (\left(1 - m\right) \cdot \left(\frac{m}{v}\right) + -1)_* + \color{blue}{1 \cdot (\left(\frac{m}{v}\right) \cdot \left(m \cdot \left(-1 + m\right)\right) + m)_*}\]
Applied distribute-lft-out0.1
\[\leadsto \color{blue}{1 \cdot \left((\left(1 - m\right) \cdot \left(\frac{m}{v}\right) + -1)_* + (\left(\frac{m}{v}\right) \cdot \left(m \cdot \left(-1 + m\right)\right) + m)_*\right)}\]
Simplified0.1
\[\leadsto 1 \cdot \color{blue}{(\left((\left(\frac{m}{v}\right) \cdot \left(m + -1\right) + 1)_*\right) \cdot m + \left((\left(\frac{m}{v}\right) \cdot \left(1 - m\right) + -1)_*\right))_*}\]
Final simplification0.1
\[\leadsto (\left((\left(\frac{m}{v}\right) \cdot \left(m + -1\right) + 1)_*\right) \cdot m + \left((\left(\frac{m}{v}\right) \cdot \left(1 - m\right) + -1)_*\right))_*\]