Initial program 28.3
\[\frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
\]
Simplified28.3
\[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)} - b}{a \cdot 2}}
\]
Proof
[Start]28.3 | \[ \frac{\left(-b\right) + \sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c}}{2 \cdot a}
\] |
|---|
+-commutative [=>]28.3 | \[ \frac{\color{blue}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} + \left(-b\right)}}{2 \cdot a}
\] |
|---|
unsub-neg [=>]28.3 | \[ \frac{\color{blue}{\sqrt{b \cdot b - \left(4 \cdot a\right) \cdot c} - b}}{2 \cdot a}
\] |
|---|
fma-neg [=>]28.3 | \[ \frac{\sqrt{\color{blue}{\mathsf{fma}\left(b, b, -\left(4 \cdot a\right) \cdot c\right)}} - b}{2 \cdot a}
\] |
|---|
*-commutative [=>]28.3 | \[ \frac{\sqrt{\mathsf{fma}\left(b, b, -\color{blue}{c \cdot \left(4 \cdot a\right)}\right)} - b}{2 \cdot a}
\] |
|---|
distribute-rgt-neg-in [=>]28.3 | \[ \frac{\sqrt{\mathsf{fma}\left(b, b, \color{blue}{c \cdot \left(-4 \cdot a\right)}\right)} - b}{2 \cdot a}
\] |
|---|
distribute-lft-neg-in [=>]28.3 | \[ \frac{\sqrt{\mathsf{fma}\left(b, b, c \cdot \color{blue}{\left(\left(-4\right) \cdot a\right)}\right)} - b}{2 \cdot a}
\] |
|---|
*-commutative [<=]28.3 | \[ \frac{\sqrt{\mathsf{fma}\left(b, b, c \cdot \color{blue}{\left(a \cdot \left(-4\right)\right)}\right)} - b}{2 \cdot a}
\] |
|---|
metadata-eval [=>]28.3 | \[ \frac{\sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot \color{blue}{-4}\right)\right)} - b}{2 \cdot a}
\] |
|---|
*-commutative [=>]28.3 | \[ \frac{\sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)} - b}{\color{blue}{a \cdot 2}}
\] |
|---|
Applied egg-rr28.8
\[\leadsto \color{blue}{\sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)} \cdot \frac{0.5}{a} - b \cdot \frac{0.5}{a}}
\]
Applied egg-rr27.6
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right) - b \cdot b}{\left(a \cdot 2\right) \cdot \left(b + \sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)}\right)}}
\]
Applied egg-rr27.6
\[\leadsto \color{blue}{\left(-\left(\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right) - b \cdot b\right)\right) \cdot \frac{1}{\left(a \cdot 2\right) \cdot \left(-\left(b + \sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)}\right)\right)}}
\]
Simplified0.3
\[\leadsto \color{blue}{\frac{\frac{0 - -4 \cdot \left(c \cdot a\right)}{a}}{-2 \cdot \left(b + \sqrt{\mathsf{fma}\left(b, b, -4 \cdot \left(c \cdot a\right)\right)}\right)}}
\]
Proof
[Start]27.6 | \[ \left(-\left(\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right) - b \cdot b\right)\right) \cdot \frac{1}{\left(a \cdot 2\right) \cdot \left(-\left(b + \sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)}\right)\right)}
\] |
|---|
associate-*r/ [=>]27.6 | \[ \color{blue}{\frac{\left(-\left(\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right) - b \cdot b\right)\right) \cdot 1}{\left(a \cdot 2\right) \cdot \left(-\left(b + \sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)}\right)\right)}}
\] |
|---|
associate-*l* [=>]27.6 | \[ \frac{\left(-\left(\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right) - b \cdot b\right)\right) \cdot 1}{\color{blue}{a \cdot \left(2 \cdot \left(-\left(b + \sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)}\right)\right)\right)}}
\] |
|---|
associate-/r* [=>]27.6 | \[ \color{blue}{\frac{\frac{\left(-\left(\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right) - b \cdot b\right)\right) \cdot 1}{a}}{2 \cdot \left(-\left(b + \sqrt{\mathsf{fma}\left(b, b, c \cdot \left(a \cdot -4\right)\right)}\right)\right)}}
\] |
|---|
Final simplification0.3
\[\leadsto \frac{\frac{4 \cdot \left(c \cdot a\right)}{a}}{-2 \cdot \left(b + \sqrt{\mathsf{fma}\left(b, b, -4 \cdot \left(c \cdot a\right)\right)}\right)}
\]