Initial program 30.2
\[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{F}{\sin B} \cdot {\left(\left(F \cdot F + 2\right) + 2 \cdot x\right)}^{\left(-\frac{1}{2}\right)}
\]
Simplified30.2
\[\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, 11 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))): 3 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))): 11 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, 11 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (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))): 11 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 (/.f64 1 2)))) (Rewrite<= associate-*r/_binary64 (*.f64 x (/.f64 1 (tan.f64 B))))): 0 points increase in error, 11 points decrease in error
(Rewrite<= unsub-neg_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)))))): 0 points increase in error, 3 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)))))): 11 points increase in error, 0 points decrease in error
Taylor expanded in F around -inf 0.1
\[\leadsto \color{blue}{\frac{-1}{\sin B}} - \frac{x}{\tan B}
\]
Initial program 0.8
\[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{F}{\sin B} \cdot {\left(\left(F \cdot F + 2\right) + 2 \cdot x\right)}^{\left(-\frac{1}{2}\right)}
\]
Simplified0.7
\[\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, 11 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))): 3 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))): 11 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, 11 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (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))): 11 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 (/.f64 1 2)))) (Rewrite<= associate-*r/_binary64 (*.f64 x (/.f64 1 (tan.f64 B))))): 0 points increase in error, 11 points decrease in error
(Rewrite<= unsub-neg_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)))))): 0 points increase in error, 3 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)))))): 11 points increase in error, 0 points decrease in error
Applied egg-rr0.3
\[\leadsto \color{blue}{\frac{F \cdot {\left(\mathsf{fma}\left(x, 2, \mathsf{fma}\left(F, F, 2\right)\right)\right)}^{-0.5}}{\sin B}} - \frac{x}{\tan B}
\]
Initial program 25.1
\[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{F}{\sin B} \cdot {\left(\left(F \cdot F + 2\right) + 2 \cdot x\right)}^{\left(-\frac{1}{2}\right)}
\]
Simplified25.0
\[\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, 11 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))): 3 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))): 11 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, 11 points decrease in error
(-.f64 (*.f64 (/.f64 F (sin.f64 B)) (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))): 11 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 (/.f64 1 2)))) (Rewrite<= associate-*r/_binary64 (*.f64 x (/.f64 1 (tan.f64 B))))): 0 points increase in error, 11 points decrease in error
(Rewrite<= unsub-neg_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)))))): 0 points increase in error, 3 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)))))): 11 points increase in error, 0 points decrease in error
Taylor expanded in F around -inf 38.6
\[\leadsto \color{blue}{\frac{-1}{\sin B}} - \frac{x}{\tan B}
\]
Applied egg-rr42.3
\[\leadsto \color{blue}{\frac{-1 \cdot \frac{\tan B}{x} - \sin B}{\sin B \cdot \frac{\tan B}{x}}}
\]
Simplified38.7
\[\leadsto \color{blue}{\frac{\frac{-\tan B}{x \cdot \sin B} + -1}{\frac{\tan B}{x}}}
\]
Proof
(/.f64 (+.f64 (/.f64 (neg.f64 (tan.f64 B)) (*.f64 x (sin.f64 B))) -1) (/.f64 (tan.f64 B) x)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (/.f64 (neg.f64 (tan.f64 B)) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 B) x))) -1) (/.f64 (tan.f64 B) x)): 0 points increase in error, 9 points decrease in error
(/.f64 (+.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (neg.f64 (tan.f64 B)) x) (sin.f64 B))) -1) (/.f64 (tan.f64 B) x)): 10 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (/.f64 (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (tan.f64 B))) x) (sin.f64 B)) -1) (/.f64 (tan.f64 B) x)): 8 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (/.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (tan.f64 B) x))) (sin.f64 B)) -1) (/.f64 (tan.f64 B) x)): 0 points increase in error, 10 points decrease in error
(/.f64 (+.f64 (/.f64 (*.f64 -1 (/.f64 (tan.f64 B) x)) (sin.f64 B)) (Rewrite<= metadata-eval (neg.f64 1))) (/.f64 (tan.f64 B) x)): 10 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 (*.f64 -1 (/.f64 (tan.f64 B) x)) (sin.f64 B)) 1)) (/.f64 (tan.f64 B) x)): 1 points increase in error, 9 points decrease in error
(/.f64 (-.f64 (/.f64 (*.f64 -1 (/.f64 (tan.f64 B) x)) (sin.f64 B)) (Rewrite<= *-inverses_binary64 (/.f64 (sin.f64 B) (sin.f64 B)))) (/.f64 (tan.f64 B) x)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (*.f64 -1 (/.f64 (tan.f64 B) x)) (sin.f64 B)) (sin.f64 B))) (/.f64 (tan.f64 B) x)): 9 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (-.f64 (*.f64 -1 (/.f64 (tan.f64 B) x)) (sin.f64 B)) (*.f64 (sin.f64 B) (/.f64 (tan.f64 B) x)))): 9 points increase in error, 1 points decrease in error
Applied egg-rr0.4
\[\leadsto \color{blue}{\frac{x}{\tan B} \cdot \frac{\frac{\tan B}{x}}{\sin B} + \frac{x}{\tan B} \cdot -1}
\]
Simplified0.2
\[\leadsto \color{blue}{\frac{\left(-x\right) + \frac{\tan B}{\sin B}}{\tan B}}
\]
Proof
(/.f64 (+.f64 (neg.f64 x) (/.f64 (tan.f64 B) (sin.f64 B))) (tan.f64 B)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 x)) (/.f64 (tan.f64 B) (sin.f64 B))) (tan.f64 B)): 0 points increase in error, 15 points decrease in error
(/.f64 (+.f64 (*.f64 -1 x) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (tan.f64 B) (sin.f64 B))))) (tan.f64 B)): 15 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (*.f64 -1 x) (*.f64 (Rewrite<= rgt-mult-inverse_binary64 (*.f64 x (/.f64 1 x))) (/.f64 (tan.f64 B) (sin.f64 B)))) (tan.f64 B)): 0 points increase in error, 15 points decrease in error
(/.f64 (+.f64 (*.f64 -1 x) (Rewrite<= associate-*r*_binary64 (*.f64 x (*.f64 (/.f64 1 x) (/.f64 (tan.f64 B) (sin.f64 B)))))) (tan.f64 B)): 0 points increase in error, 15 points decrease in error
(/.f64 (+.f64 (*.f64 -1 x) (*.f64 x (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (/.f64 1 x) (tan.f64 B)) (sin.f64 B))))) (tan.f64 B)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (*.f64 -1 x) (*.f64 x (/.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 (tan.f64 B)) x)) (sin.f64 B)))) (tan.f64 B)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (*.f64 -1 x) (*.f64 x (/.f64 (Rewrite<= associate-*r/_binary64 (*.f64 1 (/.f64 (tan.f64 B) x))) (sin.f64 B)))) (tan.f64 B)): 15 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (*.f64 -1 x) (*.f64 x (Rewrite<= associate-*r/_binary64 (*.f64 1 (/.f64 (/.f64 (tan.f64 B) x) (sin.f64 B)))))) (tan.f64 B)): 0 points increase in error, 15 points decrease in error
(/.f64 (+.f64 (*.f64 -1 x) (*.f64 x (Rewrite=> *-lft-identity_binary64 (/.f64 (/.f64 (tan.f64 B) x) (sin.f64 B))))) (tan.f64 B)): 15 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (*.f64 -1 x) (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (/.f64 (tan.f64 B) x) (sin.f64 B)) x))) (tan.f64 B)): 0 points increase in error, 15 points decrease in error
(/.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 x (+.f64 -1 (/.f64 (/.f64 (tan.f64 B) x) (sin.f64 B))))) (tan.f64 B)): 15 points increase in error, 0 points decrease in error
(/.f64 (*.f64 x (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (/.f64 (tan.f64 B) x) (sin.f64 B)) -1))) (tan.f64 B)): 0 points increase in error, 15 points decrease in error
(Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 x (tan.f64 B)) (+.f64 (/.f64 (/.f64 (tan.f64 B) x) (sin.f64 B)) -1))): 0 points increase in error, 15 points decrease in error
(Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 (/.f64 x (tan.f64 B)) (/.f64 (/.f64 (tan.f64 B) x) (sin.f64 B))) (*.f64 (/.f64 x (tan.f64 B)) -1))): 15 points increase in error, 0 points decrease in error