Simplified25.3
\[\leadsto \color{blue}{\frac{F}{\sin B} \cdot {\left(\mathsf{fma}\left(x, 2, \mathsf{fma}\left(F, F, 2\right)\right)\right)}^{-0.5} - \frac{x}{\tan B}}
\]
Proof
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (pow.f64 (fma.f64 x 2 (fma.f64 F F 2)) -1/2)) (/.f64 x (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (pow.f64 (fma.f64 x 2 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 F F) 2))) -1/2)) (/.f64 x (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (pow.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 x 2) (+.f64 (*.f64 F F) 2))) -1/2)) (/.f64 x (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (pow.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 x)) (+.f64 (*.f64 F F) 2)) -1/2)) (/.f64 x (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (pow.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x))) -1/2)) (/.f64 x (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (pow.f64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x)) (Rewrite<= metadata-eval (neg.f64 1/2)))) (/.f64 x (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (pow.f64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x)) (neg.f64 (Rewrite<= metadata-eval (/.f64 1 2))))) (/.f64 x (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (pow.f64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x)) (neg.f64 (/.f64 1 2))))))) (/.f64 x (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (neg.f64 (neg.f64 (pow.f64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x)) (neg.f64 (/.f64 1 2)))))) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 x 1)) (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (neg.f64 (neg.f64 (pow.f64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x)) (neg.f64 (/.f64 1 2)))))) (Rewrite<= associate-*r/_binary64 (*.f64 x (/.f64 1 (tan.f64 B))))): 31 points increase in error, 10 points decrease in error
(Rewrite=> fma-neg_binary64 (fma.f64 (/.f64 F (sin.f64 B)) (neg.f64 (neg.f64 (pow.f64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x)) (neg.f64 (/.f64 1 2))))) (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))))): 1 points increase in error, 2 points decrease in error
(fma.f64 (/.f64 F (sin.f64 B)) (Rewrite=> remove-double-neg_binary64 (pow.f64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x)) (neg.f64 (/.f64 1 2)))) (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 F (sin.f64 B)) (pow.f64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x)) (neg.f64 (/.f64 1 2)))) (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))))): 2 points increase in error, 1 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (*.f64 (/.f64 F (sin.f64 B)) (pow.f64 (+.f64 (+.f64 (*.f64 F F) 2) (*.f64 2 x)) (neg.f64 (/.f64 1 2)))))): 0 points increase in error, 0 points decrease in error