Initial program 26.1
\[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}
\]
Simplified8.2
\[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, C - A\right)}{B}\right)}{\pi}}
\]
Proof
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (hypot.f64 B (-.f64 C A))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 C A) (-.f64 C A)))))) B)) (PI.f64))): 96 points increase in error, 7 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 C A) (-.f64 C A))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= sqr-neg_binary64 (*.f64 (neg.f64 (-.f64 C A)) (neg.f64 (-.f64 C A))))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 C A))) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 C) A)) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 C)) A) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 A (neg.f64 C))) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 A C)) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 C A))))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 C) A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 C)) A))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= +-commutative_binary64 (+.f64 A (neg.f64 C))))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= sub-neg_binary64 (-.f64 A C)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.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)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.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)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.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)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.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))))))) (PI.f64))): 0 points increase in error, 0 points decrease in error
Initial program 52.6
\[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}
\]
Simplified51.1
\[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{\left(C - A\right) - \mathsf{hypot}\left(B, C - A\right)}{B}\right)}{\pi}}
\]
Proof
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (hypot.f64 B (-.f64 C A))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (Rewrite<= hypot-def_binary64 (sqrt.f64 (+.f64 (*.f64 B B) (*.f64 (-.f64 C A) (-.f64 C A)))))) B)) (PI.f64))): 96 points increase in error, 7 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (Rewrite<= unpow2_binary64 (pow.f64 B 2)) (*.f64 (-.f64 C A) (-.f64 C A))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (Rewrite<= sqr-neg_binary64 (*.f64 (neg.f64 (-.f64 C A)) (neg.f64 (-.f64 C A))))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 C A))) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 C) A)) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 C)) A) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 A (neg.f64 C))) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 A C)) (neg.f64 (-.f64 C A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 C A))))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 C) A)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 C)) A))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= +-commutative_binary64 (+.f64 A (neg.f64 C))))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (sqrt.f64 (+.f64 (pow.f64 B 2) (*.f64 (-.f64 A C) (Rewrite<= sub-neg_binary64 (-.f64 A C)))))) B)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.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)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.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)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.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)) (PI.f64))): 0 points increase in error, 0 points decrease in error
(*.f64 180 (/.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))))))) (PI.f64))): 0 points increase in error, 0 points decrease in error
Taylor expanded in C around 0 55.1
\[\leadsto \color{blue}{180 \cdot \frac{\tan^{-1} \left(\frac{C - \left(A + \mathsf{hypot}\left(B, C - A\right)\right)}{B}\right)}{\pi}}
\]
Simplified55.1
\[\leadsto \color{blue}{\frac{180}{\pi} \cdot \tan^{-1} \left(\frac{C - \left(A + \mathsf{hypot}\left(B, C - A\right)\right)}{B}\right)}
\]
Proof
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (-.f64 C (+.f64 A (hypot.f64 B (-.f64 C A)))) B))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (Rewrite=> associate--r+_binary64 (-.f64 (-.f64 C A) (hypot.f64 B (-.f64 C A)))) B))): 7 points increase in error, 24 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (-.f64 (Rewrite=> sub-neg_binary64 (+.f64 C (neg.f64 A))) (hypot.f64 B (-.f64 C A))) B))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (-.f64 (+.f64 C (Rewrite<= mul-1-neg_binary64 (*.f64 -1 A))) (hypot.f64 B (-.f64 C A))) B))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (-.f64 (+.f64 C (*.f64 -1 A)) (hypot.f64 B (Rewrite=> sub-neg_binary64 (+.f64 C (neg.f64 A))))) B))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 180 (PI.f64)) (atan.f64 (/.f64 (-.f64 (+.f64 C (*.f64 -1 A)) (hypot.f64 B (+.f64 C (Rewrite<= mul-1-neg_binary64 (*.f64 -1 A))))) B))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 180 (/.f64 (PI.f64) (atan.f64 (/.f64 (-.f64 (+.f64 C (*.f64 -1 A)) (hypot.f64 B (+.f64 C (*.f64 -1 A)))) B))))): 4 points increase in error, 2 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 180 (atan.f64 (/.f64 (-.f64 (+.f64 C (*.f64 -1 A)) (hypot.f64 B (+.f64 C (*.f64 -1 A)))) B))) (PI.f64))): 3 points increase in error, 3 points decrease in error
(/.f64 (*.f64 180 (atan.f64 (/.f64 (-.f64 (+.f64 C (Rewrite=> mul-1-neg_binary64 (neg.f64 A))) (hypot.f64 B (+.f64 C (*.f64 -1 A)))) B))) (PI.f64)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 180 (atan.f64 (/.f64 (-.f64 (Rewrite<= sub-neg_binary64 (-.f64 C A)) (hypot.f64 B (+.f64 C (*.f64 -1 A)))) B))) (PI.f64)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 180 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (hypot.f64 B (+.f64 C (Rewrite=> mul-1-neg_binary64 (neg.f64 A))))) B))) (PI.f64)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 180 (atan.f64 (/.f64 (-.f64 (-.f64 C A) (hypot.f64 B (Rewrite<= sub-neg_binary64 (-.f64 C A)))) B))) (PI.f64)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 180 (atan.f64 (/.f64 (Rewrite<= associate--r+_binary64 (-.f64 C (+.f64 A (hypot.f64 B (-.f64 C A))))) B))) (PI.f64)): 24 points increase in error, 7 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 180 (/.f64 (atan.f64 (/.f64 (-.f64 C (+.f64 A (hypot.f64 B (-.f64 C A)))) B)) (PI.f64)))): 4 points increase in error, 6 points decrease in error
Taylor expanded in B around 0 1.9
\[\leadsto \frac{180}{\pi} \cdot \tan^{-1} \color{blue}{\left(-0.5 \cdot \frac{B}{C - A}\right)}
\]
Simplified1.9
\[\leadsto \frac{180}{\pi} \cdot \tan^{-1} \color{blue}{\left(\frac{B \cdot -0.5}{C - A}\right)}
\]
Proof
(/.f64 (*.f64 B -1/2) (-.f64 C A)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 B (-.f64 C A)) -1/2)): 2 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 -1/2 (/.f64 B (-.f64 C A)))): 0 points increase in error, 0 points decrease in error