Initial program 26.8
\[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\pi}
\]
Simplified12.5
\[\leadsto \color{blue}{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, A - C\right)}{B}\right) \cdot \frac{180}{\pi}}
\]
Proof
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (hypot.f64 B (-.f64 A C))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 A C) (-.f64 A C)))))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 9 points decrease in error
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 A C) (-.f64 A C))))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 A C) 2))))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) B)) (/.f64 180 (PI.f64))): 10 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (/.f64 180 (PI.f64))): 0 points increase in error, 10 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (atan.f64 (*.f64 (/.f64 1 B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) 180) (PI.f64))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (atan.f64 (*.f64 (/.f64 1 B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) (PI.f64)) 180)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 180 (/.f64 (atan.f64 (*.f64 (/.f64 1 B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) (PI.f64)))): 0 points increase in error, 0 points decrease in error
Initial program 52.2
\[180 \cdot \frac{\tan^{-1} \left(\frac{1}{B} \cdot \left(\left(C - A\right) - \sqrt{{\left(A - C\right)}^{2} + {B}^{2}}\right)\right)}{\pi}
\]
Simplified28.5
\[\leadsto \color{blue}{\frac{180}{\pi} \cdot \tan^{-1} \left(\frac{C - \left(A + \mathsf{hypot}\left(B, A - C\right)\right)}{B}\right)}
\]
Proof
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (hypot.f64 B (-.f64 A C))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 A C) (-.f64 A C)))))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 9 points decrease in error
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 A C) (-.f64 A C))))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= unpow2_binary64 (pow.f64 (-.f64 A C) 2))))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))) B)) (/.f64 180 (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) B)) (/.f64 180 (PI.f64))): 10 points increase in error, 0 points decrease in error
(*.f64 (atan.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2))))))) (/.f64 180 (PI.f64))): 0 points increase in error, 10 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (atan.f64 (*.f64 (/.f64 1 B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) 180) (PI.f64))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (atan.f64 (*.f64 (/.f64 1 B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) (PI.f64)) 180)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 180 (/.f64 (atan.f64 (*.f64 (/.f64 1 B) (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 (-.f64 A C) 2) (pow.f64 B 2)))))) (PI.f64)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in C around inf 35.6
\[\leadsto \frac{180}{\pi} \cdot \tan^{-1} \left(\frac{\color{blue}{-0.5 \cdot \frac{\left({B}^{2} + {A}^{2}\right) - {\left(-1 \cdot A\right)}^{2}}{C} + -1 \cdot \left(A + -1 \cdot A\right)}}{B}\right)
\]
Simplified35.6
\[\leadsto \frac{180}{\pi} \cdot \tan^{-1} \left(\frac{\color{blue}{\mathsf{fma}\left(-0.5, \frac{A \cdot A + \left(B \cdot B - {\left(-A\right)}^{2}\right)}{C}, A \cdot 0\right)}}{B}\right)
\]
Proof
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (+.f64 (*.f64 A A) (-.f64 (*.f64 B B) (pow.f64 (neg.f64 A) 2))) C) (*.f64 A 0)) B))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 A 2)) (-.f64 (*.f64 B B) (pow.f64 (neg.f64 A) 2))) C) (*.f64 A 0)) B))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 A 2) (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (pow.f64 (neg.f64 A) 2))) C) (*.f64 A 0)) B))): 0 points increase in error, 14 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (+.f64 (pow.f64 A 2) (-.f64 (pow.f64 B 2) (pow.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 A)) 2))) C) (*.f64 A 0)) B))): 0 points increase in error, 14 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (pow.f64 A 2) (pow.f64 B 2)) (pow.f64 (*.f64 -1 A) 2))) C) (*.f64 A 0)) B))): 14 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 B 2) (pow.f64 A 2))) (pow.f64 (*.f64 -1 A) 2)) C) (*.f64 A 0)) B))): 0 points increase in error, 14 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (-.f64 (+.f64 (pow.f64 B 2) (pow.f64 A 2)) (pow.f64 (*.f64 -1 A) 2)) C) (*.f64 A (Rewrite<= metadata-eval (+.f64 -1 1)))) B))): 14 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (-.f64 (+.f64 (pow.f64 B 2) (pow.f64 A 2)) (pow.f64 (*.f64 -1 A) 2)) C) (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 -1 1) A))) B))): 0 points increase in error, 14 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (-.f64 (+.f64 (pow.f64 B 2) (pow.f64 A 2)) (pow.f64 (*.f64 -1 A) 2)) C) (*.f64 (Rewrite=> metadata-eval 0) A)) B))): 14 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (-.f64 (+.f64 (pow.f64 B 2) (pow.f64 A 2)) (pow.f64 (*.f64 -1 A) 2)) C) (*.f64 (Rewrite<= metadata-eval (*.f64 -1 0)) A)) B))): 0 points increase in error, 14 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (-.f64 (+.f64 (pow.f64 B 2) (pow.f64 A 2)) (pow.f64 (*.f64 -1 A) 2)) C) (*.f64 (*.f64 -1 (Rewrite<= metadata-eval (+.f64 -1 1))) A)) B))): 0 points increase in error, 14 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (-.f64 (+.f64 (pow.f64 B 2) (pow.f64 A 2)) (pow.f64 (*.f64 -1 A) 2)) C) (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 (+.f64 -1 1) A)))) B))): 14 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (fma.f64 -1/2 (/.f64 (-.f64 (+.f64 (pow.f64 B 2) (pow.f64 A 2)) (pow.f64 (*.f64 -1 A) 2)) C) (*.f64 -1 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 A (*.f64 -1 A))))) B))): 0 points increase in error, 14 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/2 (/.f64 (-.f64 (+.f64 (pow.f64 B 2) (pow.f64 A 2)) (pow.f64 (*.f64 -1 A) 2)) C)) (*.f64 -1 (+.f64 A (*.f64 -1 A))))) B))): 14 points increase in error, 0 points decrease in error
Taylor expanded in A around 0 16.5
\[\leadsto \frac{180}{\pi} \cdot \tan^{-1} \color{blue}{\left(-0.5 \cdot \frac{B}{C}\right)}
\]
Simplified16.5
\[\leadsto \frac{180}{\pi} \cdot \tan^{-1} \color{blue}{\left(\frac{B \cdot -0.5}{C}\right)}
\]
Proof
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (*.f64 B -1/2) C))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1/2 B)) C))): 0 points increase in error, 3 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1/2 (/.f64 B C))))): 3 points increase in error, 0 points decrease in error