(FPCore (A B C F)
:precision binary64
(/
(-
(sqrt
(*
(* 2.0 (* (- (pow B 2.0) (* (* 4.0 A) C)) F))
(+ (+ A C) (sqrt (+ (pow (- A C) 2.0) (pow B 2.0)))))))
(- (pow B 2.0) (* (* 4.0 A) C))))
↓
(FPCore (A B C F)
:precision binary64
(let* ((t_0 (hypot B (- A C)))
(t_1 (fma -4.0 (* A C) (* B B)))
(t_2 (fma B B (* C (* A -4.0)))))
(if (<= A -1.08e+63)
(/
(- (sqrt (* 2.0 (* t_2 (* F (fma 2.0 C (/ (* -0.5 (* B B)) A)))))))
t_2)
(if (<= A 7.5e-268)
(* (/ (sqrt (* 2.0 (+ C (+ A t_0)))) t_1) (* (sqrt t_1) (- (sqrt F))))
(/ (sqrt (* F t_1)) (/ (- t_1) (sqrt (* 2.0 (+ A (+ C t_0))))))))))
\[\leadsto \frac{-\color{blue}{\sqrt{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right) \cdot F} \cdot \sqrt{2 \cdot \left(\mathsf{hypot}\left(B, A - C\right) + \left(A + C\right)\right)}}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
Applied egg-rr43.1
\[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right) \cdot F}}{1} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}}
\]
Simplified43.1
\[\leadsto \color{blue}{\sqrt{F \cdot \mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)}}
\]
Proof
[Start]43.1
\[ \frac{\sqrt{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right) \cdot F}}{1} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
/-rgt-identity [=>]43.1
\[ \color{blue}{\sqrt{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right) \cdot F}} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
*-commutative [=>]43.1
\[ \sqrt{\color{blue}{F \cdot \mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
*-commutative [=>]43.1
\[ \sqrt{F \cdot \mathsf{fma}\left(-4, \color{blue}{C \cdot A}, B \cdot B\right)} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
*-commutative [=>]43.1
\[ \sqrt{F \cdot \mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, \color{blue}{C \cdot A}, B \cdot B\right)}
\]
Applied egg-rr37.7
\[\leadsto \color{blue}{\left(\sqrt{\mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)} \cdot \sqrt{F}\right)} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)}
\]
\[\leadsto \frac{-\color{blue}{\sqrt{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right) \cdot F} \cdot \sqrt{2 \cdot \left(\mathsf{hypot}\left(B, A - C\right) + \left(A + C\right)\right)}}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
Applied egg-rr38.1
\[\leadsto \color{blue}{\frac{\sqrt{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right) \cdot F}}{1} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}}
\]
Simplified38.1
\[\leadsto \color{blue}{\sqrt{F \cdot \mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)}}
\]
Proof
[Start]38.1
\[ \frac{\sqrt{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right) \cdot F}}{1} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
/-rgt-identity [=>]38.1
\[ \color{blue}{\sqrt{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right) \cdot F}} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
*-commutative [=>]38.1
\[ \sqrt{\color{blue}{F \cdot \mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
*-commutative [=>]38.1
\[ \sqrt{F \cdot \mathsf{fma}\left(-4, \color{blue}{C \cdot A}, B \cdot B\right)} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}
\]
*-commutative [=>]38.1
\[ \sqrt{F \cdot \mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)} \cdot \frac{-\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, \color{blue}{C \cdot A}, B \cdot B\right)}
\]
Applied egg-rr37.3
\[\leadsto \color{blue}{\frac{\sqrt{F \cdot \mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)} \cdot \sqrt{2 \cdot \left(A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{-\mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)}}
\]
Simplified37.3
\[\leadsto \color{blue}{\frac{\sqrt{F \cdot \mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}}{\frac{-\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}{\sqrt{2 \cdot \left(A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}}}
\]
Proof
[Start]37.3
\[ \frac{\sqrt{F \cdot \mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)} \cdot \sqrt{2 \cdot \left(A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{-\mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)}
\]
associate-/l* [=>]37.3
\[ \color{blue}{\frac{\sqrt{F \cdot \mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)}}{\frac{-\mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)}{\sqrt{2 \cdot \left(A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}}}
\]
*-commutative [=>]37.3
\[ \frac{\sqrt{F \cdot \mathsf{fma}\left(-4, \color{blue}{A \cdot C}, B \cdot B\right)}}{\frac{-\mathsf{fma}\left(-4, C \cdot A, B \cdot B\right)}{\sqrt{2 \cdot \left(A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}}
\]
*-commutative [=>]37.3
\[ \frac{\sqrt{F \cdot \mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}}{\frac{-\mathsf{fma}\left(-4, \color{blue}{A \cdot C}, B \cdot B\right)}{\sqrt{2 \cdot \left(A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}}
\]
Recombined 3 regimes into one program.
Final simplification39.0
\[\leadsto \begin{array}{l}
\mathbf{if}\;A \leq -1.08 \cdot 10^{+63}:\\
\;\;\;\;\frac{-\sqrt{2 \cdot \left(\mathsf{fma}\left(B, B, C \cdot \left(A \cdot -4\right)\right) \cdot \left(F \cdot \mathsf{fma}\left(2, C, \frac{-0.5 \cdot \left(B \cdot B\right)}{A}\right)\right)\right)}}{\mathsf{fma}\left(B, B, C \cdot \left(A \cdot -4\right)\right)}\\
\mathbf{elif}\;A \leq 7.5 \cdot 10^{-268}:\\
\;\;\;\;\frac{\sqrt{2 \cdot \left(C + \left(A + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)} \cdot \left(\sqrt{\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)} \cdot \left(-\sqrt{F}\right)\right)\\
\mathbf{else}:\\
\;\;\;\;\frac{\sqrt{F \cdot \mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}}{\frac{-\mathsf{fma}\left(-4, A \cdot C, B \cdot B\right)}{\sqrt{2 \cdot \left(A + \left(C + \mathsf{hypot}\left(B, A - C\right)\right)\right)}}}\\
\end{array}
\]
herbie shell --seed 2023038
(FPCore (A B C F)
:name "ABCF->ab-angle a"
:precision binary64
(/ (- (sqrt (* (* 2.0 (* (- (pow B 2.0) (* (* 4.0 A) C)) F)) (+ (+ A C) (sqrt (+ (pow (- A C) 2.0) (pow B 2.0))))))) (- (pow B 2.0) (* (* 4.0 A) C))))