Simplified53.3
\[\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)))): 0 points increase in error, 27 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)))): 27 points increase in error, 0 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)))): 18 points increase in error, 9 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)))): 0 points increase in error, 27 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)))): 27 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)))): 0 points increase in error, 9 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)))): 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 (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)))): 18 points increase in error, 9 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)))): 9 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, 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 (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)))): 0 points increase in error, 9 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)))): 9 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, 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 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)))): 27 points increase in error, 0 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, 0 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, 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 (*.f64 A (*.f64 C (Rewrite<= metadata-eval (neg.f64 4)))))): 9 points increase in error, 14 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))))): 14 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)))))): 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 (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 4 A) C))))): 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))))))) (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 B B) (*.f64 (*.f64 4 A) C)))): 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))))))) (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (*.f64 4 A) C))): 0 points increase in error, 27 points decrease in error
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))))): 8 points increase in error, 1 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))))): 1 points increase in error, 8 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, 9 points decrease in error