Initial program 0.2
\[\left(-x \cdot \frac{1}{\tan B}\right) + \frac{1}{\sin B}
\]
Simplified0.2
\[\leadsto \color{blue}{\frac{1}{\sin B} - \frac{x}{\tan B}}
\]
Proof
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 x (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 (sin.f64 B)) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 x 1)) (tan.f64 B))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 (sin.f64 B)) (Rewrite<= associate-*r/_binary64 (*.f64 x (/.f64 1 (tan.f64 B))))): 14 points increase in error, 4 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 1 (sin.f64 B)) (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (*.f64 x (/.f64 1 (tan.f64 B)))) (/.f64 1 (sin.f64 B)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr1.2
\[\leadsto \color{blue}{{\left(\sqrt[3]{\frac{1}{\sin B} - \frac{x}{\tan B}}\right)}^{3}}
\]
Applied egg-rr0.2
\[\leadsto \color{blue}{\frac{\frac{\tan B - \sin B \cdot x}{\sin B}}{\tan B}}
\]
Applied egg-rr0.2
\[\leadsto \frac{\color{blue}{\frac{\tan B}{\sin B} + \left(-\frac{\sin B}{\frac{\sin B}{x}}\right)}}{\tan B}
\]
Simplified0.2
\[\leadsto \frac{\color{blue}{\frac{\tan B}{\sin B} - x}}{\tan B}
\]
Proof
(-.f64 (/.f64 (tan.f64 B) (sin.f64 B)) x): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (tan.f64 B) (sin.f64 B)) (Rewrite<= *-lft-identity_binary64 (*.f64 1 x))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (tan.f64 B) (sin.f64 B)) (*.f64 (Rewrite<= *-inverses_binary64 (/.f64 (sin.f64 B) (sin.f64 B))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (tan.f64 B) (sin.f64 B)) (Rewrite<= associate-/r/_binary64 (/.f64 (sin.f64 B) (/.f64 (sin.f64 B) x)))): 7 points increase in error, 5 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 (tan.f64 B) (sin.f64 B)) (neg.f64 (/.f64 (sin.f64 B) (/.f64 (sin.f64 B) x))))): 0 points increase in error, 0 points decrease in error
Final simplification0.2
\[\leadsto \frac{\frac{\tan B}{\sin B} - x}{\tan B}
\]