Simplified33.3
\[\leadsto \color{blue}{\frac{-\sqrt{2 \cdot \left(\mathsf{fma}\left(B, B, A \cdot \left(-4 \cdot C\right)\right) \cdot \left(F \cdot \left(C - \left(\mathsf{hypot}\left(B, A - C\right) - A\right)\right)\right)\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(-4 \cdot C\right)\right)}}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (fma.f64 B B (*.f64 A (*.f64 -4 C))) (*.f64 F (-.f64 C (-.f64 (hypot.f64 B (-.f64 A C)) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (fma.f64 B B (*.f64 A (*.f64 (Rewrite<= metadata-eval (neg.f64 4)) C))) (*.f64 F (-.f64 C (-.f64 (hypot.f64 B (-.f64 A C)) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 12 points increase in error, 14 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (fma.f64 B B (*.f64 A (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 4 C))))) (*.f64 F (-.f64 C (-.f64 (hypot.f64 B (-.f64 A C)) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 14 points increase in error, 8 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 A (*.f64 4 C))))) (*.f64 F (-.f64 C (-.f64 (hypot.f64 B (-.f64 A C)) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A 4) C)))) (*.f64 F (-.f64 C (-.f64 (hypot.f64 B (-.f64 A C)) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 8 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (fma.f64 B B (neg.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 A)) C))) (*.f64 F (-.f64 C (-.f64 (hypot.f64 B (-.f64 A C)) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 B B) (*.f64 (*.f64 4 A) C))) (*.f64 F (-.f64 C (-.f64 (hypot.f64 B (-.f64 A C)) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 34 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) (*.f64 F (-.f64 C (-.f64 (hypot.f64 B (-.f64 A C)) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 34 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F (-.f64 C (-.f64 (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 A C) (-.f64 A C))))) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 34 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F (-.f64 C (-.f64 (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 A C) (-.f64 A C)))) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 34 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F (-.f64 C (-.f64 (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 A C) 2)))) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 34 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F (-.f64 C (-.f64 (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 34 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 C (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) A))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 19 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F (Rewrite<= +-commutative_binary64 (+.f64 A (-.f64 C (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 34 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 34 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (Rewrite<= associate-*l*_binary64 (*.f64 (*.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))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 34 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 (Rewrite=> +-commutative_binary64 (+.f64 C A)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (fma.f64 B B (*.f64 A (*.f64 -4 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) (Rewrite=> associate--l+_binary64 (+.f64 C (-.f64 A (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 34 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) C) (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (-.f64 A (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 34 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 C (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F))) (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (-.f64 A (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 34 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 2 (*.f64 C (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F))) (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (-.f64 A (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 34 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (+.f64 (*.f64 2 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) C))) (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (-.f64 A (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 26 points increase in error, 8 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) C)) (*.f64 2 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) (-.f64 A (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (+.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) C) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (-.f64 A (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (+.f64 C (-.f64 A (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 8 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (*.f64 2 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F)) (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 34 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 (Rewrite<= +-commutative_binary64 (+.f64 A C)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 34 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))))))) (fma.f64 B B (*.f64 A (*.f64 (Rewrite<= metadata-eval (neg.f64 4)) C)))): 34 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))))))) (fma.f64 B B (*.f64 A (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 4 C)))))): 0 points increase in error, 34 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))))))) (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 A (*.f64 4 C)))))): 34 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))))))) (fma.f64 B B (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A 4) C))))): 8 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))))))) (fma.f64 B B (neg.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.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))))))) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 B B) (*.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
Simplified22.9
\[\leadsto \frac{-\color{blue}{\sqrt{F \cdot \left(A + \left(C - \mathsf{hypot}\left(B, A - C\right)\right)\right)} \cdot \sqrt{2 \cdot \mathsf{fma}\left(A, C \cdot -4, B \cdot B\right)}}}{\mathsf{fma}\left(B, B, A \cdot \left(-4 \cdot C\right)\right)}
\]
Proof
(/.f64 (neg.f64 (*.f64 (sqrt.f64 (*.f64 F (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))))) (sqrt.f64 (*.f64 2 (fma.f64 A (*.f64 C -4) (*.f64 B B)))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (sqrt.f64 (*.f64 F (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))))) (sqrt.f64 (*.f64 2 (fma.f64 A (Rewrite<= *-commutative_binary64 (*.f64 -4 C)) (*.f64 B B)))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (sqrt.f64 (*.f64 F (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))))) (sqrt.f64 (*.f64 2 (fma.f64 A (*.f64 -4 C) (Rewrite<= unpow2_binary64 (pow.f64 B 2))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 8 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (sqrt.f64 (*.f64 F (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))))) (sqrt.f64 (*.f64 2 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 A (*.f64 -4 C)) (pow.f64 B 2))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (sqrt.f64 (*.f64 F (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))))) (sqrt.f64 (*.f64 2 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 B 2) (*.f64 A (*.f64 -4 C)))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (sqrt.f64 (*.f64 F (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))))) (sqrt.f64 (*.f64 2 (+.f64 (Rewrite=> unpow2_binary64 (*.f64 B B)) (*.f64 A (*.f64 -4 C))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (sqrt.f64 (*.f64 F (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))))) (sqrt.f64 (*.f64 2 (Rewrite=> fma-def_binary64 (fma.f64 B B (*.f64 A (*.f64 -4 C)))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 8 points decrease in error
(/.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sqrt.f64 (*.f64 2 (fma.f64 B B (*.f64 A (*.f64 -4 C))))) (sqrt.f64 (*.f64 F (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C))))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 8 points increase in error, 0 points decrease in error