Initial program 60.9
\[\frac{-\sqrt{\left(2 \cdot \left(\left({B}^{2} - \left(4 \cdot A\right) \cdot C\right) \cdot F\right)\right) \cdot \left(\left(A + C\right) + \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)}}{{B}^{2} - \left(4 \cdot A\right) \cdot C}
\]
Simplified60.9
\[\leadsto \color{blue}{\frac{-\sqrt{2 \cdot \left(\left(\left(B \cdot B - 4 \cdot \left(A \cdot C\right)\right) \cdot F\right) \cdot \left(\left(A + C\right) + \sqrt{B \cdot B + {\left(A - C\right)}^{2}}\right)\right)}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C))) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (*.f64 B B) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C))) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 8 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (-.f64 (*.f64 B B) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C))): 0 points increase in error, 0 points decrease in error
Taylor expanded in A around 0 61.0
\[\leadsto \frac{-\sqrt{2 \cdot \color{blue}{\left(\left(C + \sqrt{{B}^{2} + {C}^{2}}\right) \cdot \left(F \cdot {B}^{2}\right)\right)}}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Simplified61.0
\[\leadsto \frac{-\sqrt{2 \cdot \color{blue}{\left(\left(C + \sqrt{B \cdot B + C \cdot C}\right) \cdot \left(\left(B \cdot B\right) \cdot F\right)\right)}}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 C C)))) (*.f64 (*.f64 B B) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 C C)))) (*.f64 (*.f64 B B) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 5 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 C 2))))) (*.f64 (*.f64 B B) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 5 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 B 2) (pow.f64 C 2)))) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 5 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 B 2) (pow.f64 C 2)))) (Rewrite<= *-commutative_binary64 (*.f64 F (pow.f64 B 2))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 5 points increase in error, 0 points decrease in error
Applied egg-rr62.3
\[\leadsto \color{blue}{e^{\mathsf{log1p}\left(\frac{\sqrt{2 \cdot \left(C + \mathsf{hypot}\left(B, C\right)\right)} \cdot \left(B \cdot \sqrt{F}\right)}{\mathsf{fma}\left(B, B, \left(C \cdot A\right) \cdot -4\right)}\right)} - 1}
\]
Simplified52.1
\[\leadsto \color{blue}{\sqrt{2 \cdot \left(C + \mathsf{hypot}\left(C, B\right)\right)} \cdot \frac{B \cdot \sqrt{F}}{\mathsf{fma}\left(B, B, \left(-4 \cdot C\right) \cdot A\right)}}
\]
Proof
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 C B)))) (/.f64 (*.f64 B (sqrt.f64 F)) (fma.f64 B B (*.f64 (*.f64 -4 C) A)))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 C C) (*.f64 B B))))))) (/.f64 (*.f64 B (sqrt.f64 F)) (fma.f64 B B (*.f64 (*.f64 -4 C) A)))): 19 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 C 2)) (*.f64 B B)))))) (/.f64 (*.f64 B (sqrt.f64 F)) (fma.f64 B B (*.f64 (*.f64 -4 C) A)))): 19 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 C 2) (Rewrite<= unpow2_binary64 (pow.f64 B 2))))))) (/.f64 (*.f64 B (sqrt.f64 F)) (fma.f64 B B (*.f64 (*.f64 -4 C) A)))): 0 points increase in error, 19 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 B 2) (pow.f64 C 2))))))) (/.f64 (*.f64 B (sqrt.f64 F)) (fma.f64 B B (*.f64 (*.f64 -4 C) A)))): 19 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (sqrt.f64 (+.f64 (Rewrite=> unpow2_binary64 (*.f64 B B)) (pow.f64 C 2)))))) (/.f64 (*.f64 B (sqrt.f64 F)) (fma.f64 B B (*.f64 (*.f64 -4 C) A)))): 0 points increase in error, 19 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (sqrt.f64 (+.f64 (*.f64 B B) (Rewrite=> unpow2_binary64 (*.f64 C C))))))) (/.f64 (*.f64 B (sqrt.f64 F)) (fma.f64 B B (*.f64 (*.f64 -4 C) A)))): 18 points increase in error, 1 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (Rewrite=> hypot-def_binary64 (hypot.f64 B C))))) (/.f64 (*.f64 B (sqrt.f64 F)) (fma.f64 B B (*.f64 (*.f64 -4 C) A)))): 6 points increase in error, 13 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (*.f64 B (sqrt.f64 F)) 1)) (fma.f64 B B (*.f64 (*.f64 -4 C) A)))): 0 points increase in error, 13 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (/.f64 (*.f64 (*.f64 B (sqrt.f64 F)) 1) (fma.f64 B B (Rewrite<= associate-*r*_binary64 (*.f64 -4 (*.f64 C A)))))): 13 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (/.f64 (*.f64 (*.f64 B (sqrt.f64 F)) 1) (fma.f64 B B (*.f64 -4 (Rewrite<= *-commutative_binary64 (*.f64 A C)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (/.f64 (*.f64 (*.f64 B (sqrt.f64 F)) 1) (fma.f64 B B (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 19 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (/.f64 (*.f64 (*.f64 B (sqrt.f64 F)) 1) (fma.f64 B B (*.f64 (Rewrite=> *-commutative_binary64 (*.f64 C A)) -4)))): 2 points increase in error, 17 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (Rewrite<= associate-*r/_binary64 (*.f64 (*.f64 B (sqrt.f64 F)) (/.f64 1 (fma.f64 B B (*.f64 (*.f64 C A) -4)))))): 17 points increase in error, 2 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (*.f64 B (sqrt.f64 F))) (/.f64 1 (fma.f64 B B (*.f64 (*.f64 C A) -4))))): 13 points increase in error, 6 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (*.f64 B (sqrt.f64 F))) 1) (fma.f64 B B (*.f64 (*.f64 C A) -4)))): 19 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> *-rgt-identity_binary64 (*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (*.f64 B (sqrt.f64 F)))) (fma.f64 B B (*.f64 (*.f64 C A) -4))): 0 points increase in error, 19 points decrease in error
(Rewrite<= expm1-log1p_binary64 (expm1.f64 (log1p.f64 (/.f64 (*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (*.f64 B (sqrt.f64 F))) (fma.f64 B B (*.f64 (*.f64 C A) -4)))))): 18 points increase in error, 1 points decrease in error
(Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (log1p.f64 (/.f64 (*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 B C)))) (*.f64 B (sqrt.f64 F))) (fma.f64 B B (*.f64 (*.f64 C A) -4))))) 1)): 19 points increase in error, 0 points decrease in error
Taylor expanded in B around inf 23.7
\[\leadsto \sqrt{2 \cdot \left(C + \mathsf{hypot}\left(C, B\right)\right)} \cdot \color{blue}{\left(\sqrt{F} \cdot \frac{1}{B}\right)}
\]
Simplified23.7
\[\leadsto \sqrt{2 \cdot \left(C + \mathsf{hypot}\left(C, B\right)\right)} \cdot \color{blue}{\frac{\sqrt{F}}{B}}
\]
Proof
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 C B)))) (/.f64 (sqrt.f64 F) B)): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 C B)))) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (sqrt.f64 F) 1)) B)): 3 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 (*.f64 2 (+.f64 C (hypot.f64 C B)))) (Rewrite<= associate-*r/_binary64 (*.f64 (sqrt.f64 F) (/.f64 1 B)))): 3 points increase in error, 0 points decrease in error
Initial program 48.0
\[\frac{-\sqrt{\left(2 \cdot \left(\left({B}^{2} - \left(4 \cdot A\right) \cdot C\right) \cdot F\right)\right) \cdot \left(\left(A + C\right) + \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)}}{{B}^{2} - \left(4 \cdot A\right) \cdot C}
\]
Simplified48.0
\[\leadsto \color{blue}{\frac{-\sqrt{2 \cdot \left(\left(\left(B \cdot B - 4 \cdot \left(A \cdot C\right)\right) \cdot F\right) \cdot \left(\left(A + C\right) + \sqrt{B \cdot B + {\left(A - C\right)}^{2}}\right)\right)}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C))) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (*.f64 B B) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C))) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 8 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (-.f64 (*.f64 B B) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C))): 0 points increase in error, 0 points decrease in error
Applied egg-rr37.8
\[\leadsto \frac{-\color{blue}{\sqrt{2 \cdot \left(\mathsf{fma}\left(B, B, \left(A \cdot C\right) \cdot -4\right) \cdot F\right)} \cdot \sqrt{A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)}}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Simplified37.8
\[\leadsto \frac{-\color{blue}{\sqrt{A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)} \cdot \sqrt{\left(2 \cdot \mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)\right) \cdot F}}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 C C)))) (*.f64 (*.f64 B B) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 C C)))) (*.f64 (*.f64 B B) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 5 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 C 2))))) (*.f64 (*.f64 B B) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 5 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 B 2) (pow.f64 C 2)))) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 5 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 B 2) (pow.f64 C 2)))) (Rewrite<= *-commutative_binary64 (*.f64 F (pow.f64 B 2))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 5 points increase in error, 0 points decrease in error
Initial program 52.9
\[\frac{-\sqrt{\left(2 \cdot \left(\left({B}^{2} - \left(4 \cdot A\right) \cdot C\right) \cdot F\right)\right) \cdot \left(\left(A + C\right) + \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)}}{{B}^{2} - \left(4 \cdot A\right) \cdot C}
\]
Simplified47.8
\[\leadsto \color{blue}{\frac{-\sqrt{2 \cdot \left(\mathsf{fma}\left(B, B, C \cdot \left(A \cdot -4\right)\right) \cdot \left(F \cdot \left(A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)\right)\right)\right)}}{\mathsf{fma}\left(B, B, C \cdot \left(A \cdot -4\right)\right)}}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C))) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (*.f64 B B) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C))) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 8 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (-.f64 (*.f64 B B) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C))): 0 points increase in error, 0 points decrease in error
Taylor expanded in A around -inf 49.4
\[\leadsto \frac{-\sqrt{2 \cdot \left(\mathsf{fma}\left(B, B, C \cdot \left(A \cdot -4\right)\right) \cdot \left(F \cdot \color{blue}{\left(2 \cdot C\right)}\right)\right)}}{\mathsf{fma}\left(B, B, C \cdot \left(A \cdot -4\right)\right)}
\]
Initial program 61.0
\[\frac{-\sqrt{\left(2 \cdot \left(\left({B}^{2} - \left(4 \cdot A\right) \cdot C\right) \cdot F\right)\right) \cdot \left(\left(A + C\right) + \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)}}{{B}^{2} - \left(4 \cdot A\right) \cdot C}
\]
Simplified61.0
\[\leadsto \color{blue}{\frac{-\sqrt{2 \cdot \left(\left(\left(B \cdot B - 4 \cdot \left(A \cdot C\right)\right) \cdot F\right) \cdot \left(\left(A + C\right) + \sqrt{B \cdot B + {\left(A - C\right)}^{2}}\right)\right)}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C))) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (*.f64 B B) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C))) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (pow.f64 (-.f64 A C) 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 8 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (+.f64 (+.f64 A C) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (-.f64 (*.f64 B B) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C))): 0 points increase in error, 0 points decrease in error
Taylor expanded in A around 0 57.8
\[\leadsto \frac{-\color{blue}{\sqrt{\left(C + \sqrt{{B}^{2} + {C}^{2}}\right) \cdot F} \cdot \left(\sqrt{2} \cdot B\right)}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Simplified57.8
\[\leadsto \frac{-\color{blue}{\sqrt{F \cdot \left(C + \sqrt{B \cdot B + C \cdot C}\right)} \cdot \left(B \cdot \sqrt{2}\right)}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 C C)))) (*.f64 (*.f64 B B) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 C C)))) (*.f64 (*.f64 B B) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 5 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 C 2))))) (*.f64 (*.f64 B B) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 5 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 B 2) (pow.f64 C 2)))) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) F))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 5 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (+.f64 C (sqrt.f64 (+.f64 (pow.f64 B 2) (pow.f64 C 2)))) (Rewrite<= *-commutative_binary64 (*.f64 F (pow.f64 B 2))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 5 points increase in error, 0 points decrease in error
Taylor expanded in C around 0 32.5
\[\leadsto \color{blue}{-1 \cdot \left(\sqrt{2} \cdot \sqrt{\frac{F}{B}}\right)}
\]
Simplified32.5
\[\leadsto \color{blue}{\sqrt{\frac{F}{B}} \cdot \left(-\sqrt{2}\right)}
\]
Proof
(*.f64 (sqrt.f64 (/.f64 F B)) (neg.f64 (sqrt.f64 2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (sqrt.f64 2)) (sqrt.f64 (/.f64 F B)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (sqrt.f64 2))) (sqrt.f64 (/.f64 F B))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 (sqrt.f64 2) (sqrt.f64 (/.f64 F B))))): 0 points increase in error, 0 points decrease in error