Initial program 14.9
\[\frac{r \cdot \sin b}{\cos \left(a + b\right)}
\]
Simplified14.9
\[\leadsto \color{blue}{\frac{r \cdot \sin b}{\cos \left(b + a\right)}}
\]
Proof
(/.f64 (*.f64 r (sin.f64 b)) (cos.f64 (+.f64 b a))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 r (sin.f64 b)) (cos.f64 (Rewrite<= +-commutative_binary64 (+.f64 a b)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.3
\[\leadsto \frac{r \cdot \sin b}{\color{blue}{\mathsf{fma}\left(\cos b, \cos a, \left(-\sin b\right) \cdot \sin a\right)}}
\]
Taylor expanded in r around 0 0.3
\[\leadsto \color{blue}{\frac{\sin b \cdot r}{-1 \cdot \left(\sin a \cdot \sin b\right) + \cos a \cdot \cos b}}
\]
Simplified0.3
\[\leadsto \color{blue}{\frac{\sin b}{\cos a \cdot \cos b - \sin b \cdot \sin a} \cdot r}
\]
Proof
(*.f64 (/.f64 (sin.f64 b) (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (sin.f64 b) (sin.f64 a)))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (cos.f64 b) (cos.f64 a))) (*.f64 (sin.f64 b) (sin.f64 a)))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (-.f64 (*.f64 (cos.f64 b) (cos.f64 a)) (Rewrite=> *-commutative_binary64 (*.f64 (sin.f64 a) (sin.f64 b))))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 (*.f64 (cos.f64 b) (cos.f64 a)) (*.f64 (neg.f64 (sin.f64 a)) (sin.f64 b))))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (neg.f64 (sin.f64 a)) (sin.f64 b)) (*.f64 (cos.f64 b) (cos.f64 a))))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (+.f64 (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 (sin.f64 a) (sin.f64 b)))) (*.f64 (cos.f64 b) (cos.f64 a)))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (+.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b)))) (*.f64 (cos.f64 b) (cos.f64 a)))) r): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (sin.f64 b) (+.f64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b))) (Rewrite=> *-commutative_binary64 (*.f64 (cos.f64 a) (cos.f64 b))))) r): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 (sin.f64 b) (/.f64 (+.f64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b))) (*.f64 (cos.f64 a) (cos.f64 b))) r))): 51 points increase in error, 40 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (sin.f64 b) r) (+.f64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b))) (*.f64 (cos.f64 a) (cos.f64 b))))): 38 points increase in error, 44 points decrease in error
Applied egg-rr0.3
\[\leadsto \frac{\sin b}{\color{blue}{\mathsf{fma}\left(\cos b, \cos a, \sin a \cdot \left(-\sin b\right)\right)}} \cdot r
\]
Final simplification0.3
\[\leadsto \frac{\sin b}{\mathsf{fma}\left(\cos b, \cos a, \sin a \cdot \left(-\sin b\right)\right)} \cdot r
\]