Initial program 15.1
\[\frac{r \cdot \sin b}{\cos \left(a + b\right)}
\]
Simplified15.1
\[\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{r}{\cos a \cdot \cos b - \sin b \cdot \sin a} \cdot \sin b}
\]
Proof
(*.f64 (/.f64 r (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (sin.f64 b) (sin.f64 a)))) (sin.f64 b)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 r (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 a) (sin.f64 b))))) (sin.f64 b)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 r (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (neg.f64 (*.f64 (sin.f64 a) (sin.f64 b)))))) (sin.f64 b)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 r (+.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b)))))) (sin.f64 b)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 r (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b))) (*.f64 (cos.f64 a) (cos.f64 b))))) (sin.f64 b)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 r (/.f64 (+.f64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b))) (*.f64 (cos.f64 a) (cos.f64 b))) (sin.f64 b)))): 49 points increase in error, 31 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 r (sin.f64 b)) (+.f64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b))) (*.f64 (cos.f64 a) (cos.f64 b))))): 25 points increase in error, 46 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 b) r)) (+.f64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b))) (*.f64 (cos.f64 a) (cos.f64 b)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in r around 0 0.3
\[\leadsto \color{blue}{\frac{\sin b \cdot r}{\cos a \cdot \cos b - \sin a \cdot \sin 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 (*.f64 (cos.f64 a) (cos.f64 b)) (Rewrite<= *-commutative_binary64 (*.f64 (sin.f64 a) (sin.f64 b))))) r): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (sin.f64 b) r) (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (sin.f64 a) (sin.f64 b))))): 37 points increase in error, 25 points decrease in error
Final simplification0.3
\[\leadsto \frac{\sin b}{\cos a \cdot \cos b - \sin b \cdot \sin a} \cdot r
\]