Initial program 1.7
\[\frac{\left(\frac{\left(-b_2\right)}{\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(a \cdot c\right)\right)}\right)}\right)}{a}\]
Simplified1.7
\[\leadsto \color{blue}{\frac{\left(\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right) - b_2\right)}{a}}\]
- Using strategy
rm Applied p16-flip--2.9
\[\leadsto \frac{\color{blue}{\left(\frac{\left(\left(\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right) \cdot \left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)\right) - \left(b_2 \cdot b_2\right)\right)}{\left(\frac{\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)}{b_2}\right)}\right)}}{a}\]
- Using strategy
rm Applied p16-*-un-lft-identity2.9
\[\leadsto \frac{\left(\frac{\left(\left(\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right) \cdot \left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)\right) - \color{blue}{\left(\left(1.0\right) \cdot \left(b_2 \cdot b_2\right)\right)}\right)}{\left(\frac{\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)}{b_2}\right)}\right)}{a}\]
Applied p16-*-un-lft-identity2.9
\[\leadsto \frac{\left(\frac{\left(\left(\color{blue}{\left(\left(1.0\right) \cdot \left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)\right)} \cdot \left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)\right) - \left(\left(1.0\right) \cdot \left(b_2 \cdot b_2\right)\right)\right)}{\left(\frac{\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)}{b_2}\right)}\right)}{a}\]
Applied associate-*l*2.9
\[\leadsto \frac{\left(\frac{\left(\color{blue}{\left(\left(1.0\right) \cdot \left(\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right) \cdot \left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)\right)\right)} - \left(\left(1.0\right) \cdot \left(b_2 \cdot b_2\right)\right)\right)}{\left(\frac{\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)}{b_2}\right)}\right)}{a}\]
Applied distribute-lft-out--2.9
\[\leadsto \frac{\left(\frac{\color{blue}{\left(\left(1.0\right) \cdot \left(\left(\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right) \cdot \left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)\right) - \left(b_2 \cdot b_2\right)\right)\right)}}{\left(\frac{\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)}{b_2}\right)}\right)}{a}\]
Applied associate-/l*3.2
\[\leadsto \frac{\color{blue}{\left(\frac{\left(1.0\right)}{\left(\frac{\left(\frac{\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)}{b_2}\right)}{\left(\left(\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right) \cdot \left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(c \cdot a\right)\right)}\right)\right) - \left(b_2 \cdot b_2\right)\right)}\right)}\right)}}{a}\]
Simplified1.8
\[\leadsto \frac{\left(\frac{\left(1.0\right)}{\color{blue}{\left(\frac{\left(1.0\right)}{\left(\left(\sqrt{\left(\left(b_2 \cdot b_2\right) - \left(a \cdot c\right)\right)}\right) - b_2\right)}\right)}}\right)}{a}\]
Final simplification1.8
\[\leadsto \frac{\frac{1.0}{\frac{1.0}{\sqrt{b_2 \cdot b_2 - a \cdot c} - b_2}}}{a}\]