Initial program 53.6
\[\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}
\]
Simplified51.0
\[\leadsto \color{blue}{\frac{-\sqrt{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right) \cdot \left(\left(A + \left(C - \mathsf{hypot}\left(B, A - C\right)\right)\right) \cdot \left(2 \cdot F\right)\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (*.f64 A (*.f64 C -4))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (*.f64 A (*.f64 C (Rewrite<= metadata-eval (neg.f64 4))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 A C))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 B B) (*.f64 (*.f64 4 A) C))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 C 0)) (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 10 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 A C) (-.f64 A C))))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 10 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 A C) (-.f64 A C)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 A C) 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 A (+.f64 C 0)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A (Rewrite=> +-rgt-identity_binary64 C)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (Rewrite<= *-commutative_binary64 (*.f64 F 2)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 F 2) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.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 C -4)))): 0 points increase in error, 23 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 C (Rewrite<= metadata-eval (neg.f64 4)))))): 27 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 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4))))): 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))))))) (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4))))): 0 points increase in error, 27 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<= *-commutative_binary64 (*.f64 4 (*.f64 A C)))))): 18 points increase in error, 9 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 4 A) C))))): 9 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
Applied egg-rr63.1
\[\leadsto \color{blue}{\frac{\mathsf{hypot}\left(B, \sqrt{A \cdot \left(C \cdot -4\right)}\right)}{1} \cdot \frac{\sqrt{\left(\left(A + C\right) - \mathsf{hypot}\left(B, A - C\right)\right) \cdot \left(2 \cdot F\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}}
\]
Simplified63.1
\[\leadsto \color{blue}{\frac{\sqrt{\left(C + \left(A - \mathsf{hypot}\left(B, A - C\right)\right)\right) \cdot \left(2 \cdot F\right)}}{\frac{\mathsf{fma}\left(B, B, \left(A \cdot C\right) \cdot -4\right)}{\mathsf{hypot}\left(B, \sqrt{\left(A \cdot C\right) \cdot -4}\right)}}}
\]
Proof
(/.f64 (sqrt.f64 (*.f64 (+.f64 C (-.f64 A (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 (*.f64 A C) -4)) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 C A) (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 (*.f64 A C) -4)) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 A C)) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 (*.f64 A C) -4)) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 9 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (/.f64 (fma.f64 B B (Rewrite<= associate-*r*_binary64 (*.f64 A (*.f64 C -4)))) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 9 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 A (*.f64 C -4))) (hypot.f64 B (sqrt.f64 (Rewrite<= associate-*r*_binary64 (*.f64 A (*.f64 C -4))))))): 9 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4))))) (fma.f64 B B (*.f64 A (*.f64 C -4))))): 0 points increase in error, 9 points decrease in error
(/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) 1)) (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F)))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) 1) (/.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (fma.f64 B B (*.f64 A (*.f64 C -4)))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in B around inf 36.7
\[\leadsto \frac{\sqrt{\left(C + \left(A - \mathsf{hypot}\left(B, A - C\right)\right)\right) \cdot \left(2 \cdot F\right)}}{\color{blue}{B}}
\]
Initial program 50.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}
\]
Simplified49.5
\[\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(A + \left(C - \sqrt{B \cdot B + {\left(A - C\right)}^{2}}\right)\right)\right)}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (*.f64 A (*.f64 C -4))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (*.f64 A (*.f64 C (Rewrite<= metadata-eval (neg.f64 4))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 A C))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 B B) (*.f64 (*.f64 4 A) C))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 C 0)) (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 10 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 A C) (-.f64 A C))))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 10 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 A C) (-.f64 A C)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 A C) 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 A (+.f64 C 0)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A (Rewrite=> +-rgt-identity_binary64 C)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (Rewrite<= *-commutative_binary64 (*.f64 F 2)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 F 2) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.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 C -4)))): 0 points increase in error, 23 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 C (Rewrite<= metadata-eval (neg.f64 4)))))): 27 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 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4))))): 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))))))) (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4))))): 0 points increase in error, 27 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<= *-commutative_binary64 (*.f64 4 (*.f64 A C)))))): 18 points increase in error, 9 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 4 A) C))))): 9 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
Taylor expanded in B around 0 55.3
\[\leadsto \frac{-\sqrt{2 \cdot \left(\color{blue}{\left(-4 \cdot \left(A \cdot \left(C \cdot F\right)\right)\right)} \cdot \left(A + \left(C - \sqrt{B \cdot B + {\left(A - C\right)}^{2}}\right)\right)\right)}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Simplified54.6
\[\leadsto \frac{-\sqrt{2 \cdot \left(\color{blue}{\left(-4 \cdot \left(\left(A \cdot C\right) \cdot F\right)\right)} \cdot \left(A + \left(C - \sqrt{B \cdot B + {\left(A - C\right)}^{2}}\right)\right)\right)}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 (*.f64 -4 (*.f64 (*.f64 A C) F)) (+.f64 A (-.f64 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 -4 (Rewrite<= associate-*r*_binary64 (*.f64 A (*.f64 C F)))) (+.f64 A (-.f64 C (sqrt.f64 (+.f64 (*.f64 B B) (pow.f64 (-.f64 A C) 2))))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 2 points increase in error, 0 points decrease in error
Taylor expanded in A around inf 51.2
\[\leadsto \frac{-\sqrt{2 \cdot \color{blue}{\left(-4 \cdot \left(A \cdot \left(C \cdot \left(\left(C - -1 \cdot C\right) \cdot F\right)\right)\right)\right)}}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Simplified49.0
\[\leadsto \frac{-\sqrt{2 \cdot \color{blue}{\left(-4 \cdot \left(\left(A \cdot C\right) \cdot \left(F \cdot \left(C + C\right)\right)\right)\right)}}}{B \cdot B - 4 \cdot \left(A \cdot C\right)}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 -4 (*.f64 (*.f64 A C) (*.f64 F (+.f64 C C))))))) (-.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 -4 (*.f64 (*.f64 A C) (*.f64 F (+.f64 C (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 C)))))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 6 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 -4 (*.f64 (*.f64 A C) (*.f64 F (+.f64 C (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 C)))))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 6 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 -4 (*.f64 (*.f64 A C) (*.f64 F (Rewrite<= sub-neg_binary64 (-.f64 C (*.f64 -1 C))))))))) (-.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 -4 (*.f64 (*.f64 A C) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 C (*.f64 -1 C)) F))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 0 points increase in error, 6 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 2 (*.f64 -4 (Rewrite<= associate-*r*_binary64 (*.f64 A (*.f64 C (*.f64 (-.f64 C (*.f64 -1 C)) F)))))))) (-.f64 (*.f64 B B) (*.f64 4 (*.f64 A C)))): 6 points increase in error, 0 points decrease in error
Initial program 53.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}
\]
Simplified48.5
\[\leadsto \color{blue}{\frac{-\sqrt{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right) \cdot \left(\left(A + \left(C - \mathsf{hypot}\left(B, A - C\right)\right)\right) \cdot \left(2 \cdot F\right)\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (*.f64 A (*.f64 C -4))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (*.f64 A (*.f64 C (Rewrite<= metadata-eval (neg.f64 4))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 A C))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 B B) (*.f64 (*.f64 4 A) C))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 C 0)) (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 10 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 A C) (-.f64 A C))))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 10 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 A C) (-.f64 A C)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 A C) 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 A (+.f64 C 0)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A (Rewrite=> +-rgt-identity_binary64 C)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (Rewrite<= *-commutative_binary64 (*.f64 F 2)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 F 2) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.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 C -4)))): 0 points increase in error, 23 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 C (Rewrite<= metadata-eval (neg.f64 4)))))): 27 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 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4))))): 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))))))) (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4))))): 0 points increase in error, 27 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<= *-commutative_binary64 (*.f64 4 (*.f64 A C)))))): 18 points increase in error, 9 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 4 A) C))))): 9 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
Taylor expanded in A around -inf 50.4
\[\leadsto \frac{-\sqrt{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right) \cdot \left(\color{blue}{\left(2 \cdot A + 0.5 \cdot \frac{{B}^{2}}{A}\right)} \cdot \left(2 \cdot F\right)\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Simplified50.4
\[\leadsto \frac{-\sqrt{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right) \cdot \left(\color{blue}{\mathsf{fma}\left(2, A, 0.5 \cdot \frac{B \cdot B}{A}\right)} \cdot \left(2 \cdot F\right)\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Proof
(/.f64 (sqrt.f64 (*.f64 (+.f64 C (-.f64 A (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 (*.f64 A C) -4)) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 C A) (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 (*.f64 A C) -4)) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 A C)) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 (*.f64 A C) -4)) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 9 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (/.f64 (fma.f64 B B (Rewrite<= associate-*r*_binary64 (*.f64 A (*.f64 C -4)))) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 9 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 A (*.f64 C -4))) (hypot.f64 B (sqrt.f64 (Rewrite<= associate-*r*_binary64 (*.f64 A (*.f64 C -4))))))): 9 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4))))) (fma.f64 B B (*.f64 A (*.f64 C -4))))): 0 points increase in error, 9 points decrease in error
(/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) 1)) (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F)))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) 1) (/.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (fma.f64 B B (*.f64 A (*.f64 C -4)))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr56.0
\[\leadsto \frac{-\color{blue}{\sqrt{2 \cdot \left(F \cdot \mathsf{fma}\left(2, A, 0.5 \cdot \left(\frac{B}{A} \cdot B\right)\right)\right)} \cdot \mathsf{hypot}\left(B, \sqrt{A \cdot \left(C \cdot -4\right)}\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Simplified56.0
\[\leadsto \frac{-\color{blue}{\mathsf{hypot}\left(B, \sqrt{C \cdot \left(-4 \cdot A\right)}\right) \cdot \sqrt{\left(B \cdot \frac{B}{A}\right) \cdot F + F \cdot \left(A \cdot 4\right)}}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Proof
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 C (*.f64 -4 A)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 B (/.f64 B A)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 C -4) A)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 B (/.f64 B A)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 A (*.f64 C -4))))) (sqrt.f64 (+.f64 (*.f64 (*.f64 B (/.f64 B A)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 24 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 B A) B)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 24 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (*.f64 (/.f64 B A) B) 1)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 24 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 (*.f64 (/.f64 B A) B) (Rewrite<= metadata-eval (*.f64 1/2 2))) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 24 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 (/.f64 B A) B) 1/2) 2)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 24 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/2 (*.f64 (/.f64 B A) B))) 2) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 1/2 (*.f64 (/.f64 B A) B)) (*.f64 2 F))) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B)))) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (*.f64 A (Rewrite<= metadata-eval (*.f64 2 2)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 24 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A 2) 2))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 24 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 A)) 2)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (Rewrite=> associate-*l*_binary64 (*.f64 2 (*.f64 A 2)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (*.f64 2 (Rewrite<= *-commutative_binary64 (*.f64 2 A)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 F 2) (*.f64 2 A))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 F)) (*.f64 2 A)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 (*.f64 2 F) (Rewrite=> *-commutative_binary64 (*.f64 A 2))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 A 2)) (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (Rewrite<= *-commutative_binary64 (*.f64 2 A))) (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (Rewrite=> distribute-lft-out_binary64 (*.f64 (*.f64 2 F) (+.f64 (*.f64 2 A) (*.f64 1/2 (*.f64 (/.f64 B A) B)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (*.f64 (*.f64 2 F) (Rewrite<= fma-udef_binary64 (fma.f64 2 A (*.f64 1/2 (*.f64 (/.f64 B A) B)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 F (fma.f64 2 A (*.f64 1/2 (*.f64 (/.f64 B A) B))))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 (sqrt.f64 (*.f64 2 (*.f64 F (fma.f64 2 A (*.f64 1/2 (*.f64 (/.f64 B A) B)))))) (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in B around 0 54.4
\[\leadsto \frac{-\mathsf{hypot}\left(B, \sqrt{C \cdot \left(-4 \cdot A\right)}\right) \cdot \color{blue}{\left(2 \cdot \sqrt{A \cdot F}\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Simplified54.4
\[\leadsto \frac{-\mathsf{hypot}\left(B, \sqrt{C \cdot \left(-4 \cdot A\right)}\right) \cdot \color{blue}{\left(2 \cdot \sqrt{F \cdot A}\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Proof
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 C (*.f64 -4 A)))) (*.f64 2 (sqrt.f64 (*.f64 F A))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 C (*.f64 -4 A)))) (*.f64 2 (sqrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 A F)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
Initial program 51.8
\[\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}
\]
Simplified46.0
\[\leadsto \color{blue}{\frac{-\sqrt{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right) \cdot \left(\left(A + \left(C - \mathsf{hypot}\left(B, A - C\right)\right)\right) \cdot \left(2 \cdot F\right)\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}}
\]
Proof
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (*.f64 A (*.f64 C -4))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (*.f64 A (*.f64 C (Rewrite<= metadata-eval (neg.f64 4))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 A C))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 B B) (*.f64 (*.f64 4 A) C))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 C 0)) (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 10 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 A C) (-.f64 A C))))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 10 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 A C) (-.f64 A C)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 A C) 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 A (+.f64 C 0)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A (Rewrite=> +-rgt-identity_binary64 C)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (Rewrite<= *-commutative_binary64 (*.f64 F 2)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 F 2) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.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 C -4)))): 0 points increase in error, 23 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 C (Rewrite<= metadata-eval (neg.f64 4)))))): 27 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 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4))))): 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))))))) (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4))))): 0 points increase in error, 27 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<= *-commutative_binary64 (*.f64 4 (*.f64 A C)))))): 18 points increase in error, 9 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 4 A) C))))): 9 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
Taylor expanded in A around -inf 50.3
\[\leadsto \frac{-\sqrt{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right) \cdot \left(\color{blue}{\left(2 \cdot A + 0.5 \cdot \frac{{B}^{2}}{A}\right)} \cdot \left(2 \cdot F\right)\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Simplified50.3
\[\leadsto \frac{-\sqrt{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right) \cdot \left(\color{blue}{\mathsf{fma}\left(2, A, 0.5 \cdot \frac{B \cdot B}{A}\right)} \cdot \left(2 \cdot F\right)\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Proof
(/.f64 (sqrt.f64 (*.f64 (+.f64 C (-.f64 A (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 (*.f64 A C) -4)) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 C A) (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 (*.f64 A C) -4)) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 0 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 A C)) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 (*.f64 A C) -4)) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 9 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (/.f64 (fma.f64 B B (Rewrite<= associate-*r*_binary64 (*.f64 A (*.f64 C -4)))) (hypot.f64 B (sqrt.f64 (*.f64 (*.f64 A C) -4))))): 0 points increase in error, 9 points decrease in error
(/.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (/.f64 (fma.f64 B B (*.f64 A (*.f64 C -4))) (hypot.f64 B (sqrt.f64 (Rewrite<= associate-*r*_binary64 (*.f64 A (*.f64 C -4))))))): 9 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4))))) (fma.f64 B B (*.f64 A (*.f64 C -4))))): 0 points increase in error, 9 points decrease in error
(/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) 1)) (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F)))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) 1) (/.f64 (sqrt.f64 (*.f64 (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))) (*.f64 2 F))) (fma.f64 B B (*.f64 A (*.f64 C -4)))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in A around inf 49.7
\[\leadsto \frac{-\sqrt{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right) \cdot \color{blue}{\left(4 \cdot \left(A \cdot F\right)\right)}}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Simplified49.7
\[\leadsto \frac{-\sqrt{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right) \cdot \color{blue}{\left(\left(4 \cdot A\right) \cdot F\right)}}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}
\]
Proof
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 C (*.f64 -4 A)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 B (/.f64 B A)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 C -4) A)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 B (/.f64 B A)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (Rewrite<= *-commutative_binary64 (*.f64 A (*.f64 C -4))))) (sqrt.f64 (+.f64 (*.f64 (*.f64 B (/.f64 B A)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 24 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 B A) B)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 24 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (*.f64 (/.f64 B A) B) 1)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 24 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 (*.f64 (/.f64 B A) B) (Rewrite<= metadata-eval (*.f64 1/2 2))) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 24 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (*.f64 (/.f64 B A) B) 1/2) 2)) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 24 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 1/2 (*.f64 (/.f64 B A) B))) 2) F) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 1/2 (*.f64 (/.f64 B A) B)) (*.f64 2 F))) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B)))) (*.f64 F (*.f64 A 4)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (*.f64 A (Rewrite<= metadata-eval (*.f64 2 2)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 24 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A 2) 2))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 24 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 A)) 2)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (Rewrite=> associate-*l*_binary64 (*.f64 2 (*.f64 A 2)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 F (*.f64 2 (Rewrite<= *-commutative_binary64 (*.f64 2 A)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 F 2) (*.f64 2 A))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 F)) (*.f64 2 A)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))) (*.f64 (*.f64 2 F) (Rewrite=> *-commutative_binary64 (*.f64 A 2))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (*.f64 2 F) (*.f64 A 2)) (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (+.f64 (*.f64 (*.f64 2 F) (Rewrite<= *-commutative_binary64 (*.f64 2 A))) (*.f64 (*.f64 2 F) (*.f64 1/2 (*.f64 (/.f64 B A) B))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (Rewrite=> distribute-lft-out_binary64 (*.f64 (*.f64 2 F) (+.f64 (*.f64 2 A) (*.f64 1/2 (*.f64 (/.f64 B A) B)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (*.f64 (*.f64 2 F) (Rewrite<= fma-udef_binary64 (fma.f64 2 A (*.f64 1/2 (*.f64 (/.f64 B A) B)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (*.f64 (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4)))) (sqrt.f64 (Rewrite<= associate-*r*_binary64 (*.f64 2 (*.f64 F (fma.f64 2 A (*.f64 1/2 (*.f64 (/.f64 B A) B))))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 (sqrt.f64 (*.f64 2 (*.f64 F (fma.f64 2 A (*.f64 1/2 (*.f64 (/.f64 B A) B)))))) (hypot.f64 B (sqrt.f64 (*.f64 A (*.f64 C -4))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
Initial program 52.4
\[\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}
\]
Simplified49.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 (fma.f64 B B (*.f64 A (*.f64 C -4))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (*.f64 A (*.f64 C (Rewrite<= metadata-eval (neg.f64 4))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (*.f64 A C))))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 18 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (fma.f64 B B (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C)))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 B B) (*.f64 (*.f64 4 A) C))) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 9 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 C (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (Rewrite<= +-rgt-identity_binary64 (+.f64 C 0)) (hypot.f64 B (-.f64 A C)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 10 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 A C) (-.f64 A C))))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 10 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 A C) (-.f64 A C)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 A C) 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (+.f64 A (-.f64 (+.f64 C 0) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (Rewrite=> associate-+r-_binary64 (-.f64 (+.f64 A (+.f64 C 0)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A (Rewrite=> +-rgt-identity_binary64 C)) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (*.f64 2 F))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))) (Rewrite<= *-commutative_binary64 (*.f64 F 2)))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 27 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 F 2) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 27 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) (*.f64 F 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 9 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 B 2) (*.f64 (*.f64 4 A) C)) F) 2)) (-.f64 (+.f64 A C) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))): 0 points increase in error, 18 points decrease in error
(/.f64 (neg.f64 (sqrt.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.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 C -4)))): 0 points increase in error, 23 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 C (Rewrite<= metadata-eval (neg.f64 4)))))): 27 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 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 A C) (neg.f64 4))))): 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))))))) (fma.f64 B B (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (*.f64 A C) 4))))): 0 points increase in error, 27 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<= *-commutative_binary64 (*.f64 4 (*.f64 A C)))))): 18 points increase in error, 9 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 4 A) C))))): 9 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
Applied egg-rr46.4
\[\leadsto \frac{-\color{blue}{\sqrt{2 \cdot \mathsf{fma}\left(B, B, A \cdot \left(-4 \cdot C\right)\right)} \cdot \sqrt{F \cdot \left(A + \left(C - \mathsf{hypot}\left(B, A - C\right)\right)\right)}}}{\mathsf{fma}\left(B, B, A \cdot \left(-4 \cdot C\right)\right)}
\]
Simplified46.4
\[\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(B, B, A \cdot \left(C \cdot -4\right)\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 B B (*.f64 A (*.f64 C -4))))))) (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 B B (*.f64 A (Rewrite<= *-commutative_binary64 (*.f64 -4 C)))))))) (fma.f64 B B (*.f64 A (*.f64 -4 C)))): 0 points increase in error, 3 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)))): 0 points increase in error, 3 points decrease in error
Applied egg-rr46.7
\[\leadsto \color{blue}{\sqrt{F \cdot \left(\left(A + C\right) - \mathsf{hypot}\left(B, A - C\right)\right)} \cdot \left(\left(-\sqrt{2 \cdot \mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}\right) \cdot \frac{1}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}\right)}
\]
Simplified46.7
\[\leadsto \color{blue}{\sqrt{F \cdot \left(\left(A + C\right) - \mathsf{hypot}\left(B, A - C\right)\right)} \cdot \left(-\frac{\sqrt{2 \cdot \mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}}{\mathsf{fma}\left(B, B, A \cdot \left(C \cdot -4\right)\right)}\right)}
\]
Proof
(*.f64 (sqrt.f64 (*.f64 F (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))))) (neg.f64 (/.f64 (sqrt.f64 (*.f64 2 (fma.f64 B B (*.f64 A (*.f64 C -4))))) (fma.f64 B B (*.f64 A (*.f64 C -4)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (sqrt.f64 (*.f64 F (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))))) (neg.f64 (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (sqrt.f64 (*.f64 2 (fma.f64 B B (*.f64 A (*.f64 C -4))))) 1)) (fma.f64 B B (*.f64 A (*.f64 C -4)))))): 0 points increase in error, 4 points decrease in error
(*.f64 (sqrt.f64 (*.f64 F (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))))) (neg.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (sqrt.f64 (*.f64 2 (fma.f64 B B (*.f64 A (*.f64 C -4))))) (/.f64 1 (fma.f64 B B (*.f64 A (*.f64 C -4)))))))): 0 points increase in error, 4 points decrease in error
(*.f64 (sqrt.f64 (*.f64 F (-.f64 (+.f64 A C) (hypot.f64 B (-.f64 A C))))) (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 (sqrt.f64 (*.f64 2 (fma.f64 B B (*.f64 A (*.f64 C -4)))))) (/.f64 1 (fma.f64 B B (*.f64 A (*.f64 C -4))))))): 4 points increase in error, 0 points decrease in error
Taylor expanded in B around inf 35.9
\[\leadsto \sqrt{F \cdot \left(\left(A + C\right) - \mathsf{hypot}\left(B, A - C\right)\right)} \cdot \left(-\color{blue}{\frac{\sqrt{2}}{B}}\right)
\]