Initial program 15.1
\[r \cdot \frac{\sin b}{\cos \left(a + b\right)}
\]
Simplified15.1
\[\leadsto \color{blue}{r \cdot \frac{\sin b}{\cos \left(b + a\right)}}
\]
Proof
(*.f64 r (/.f64 (sin.f64 b) (cos.f64 (+.f64 b a)))): 0 points increase in error, 0 points decrease in error
(*.f64 r (/.f64 (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 r \cdot \frac{\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 \cdot r}{\cos a \cdot \cos b - \sin a \cdot \sin b}}
\]
Proof
(/.f64 (*.f64 (sin.f64 b) r) (-.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (sin.f64 a) (sin.f64 b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (sin.f64 b) r) (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (neg.f64 (*.f64 (sin.f64 a) (sin.f64 b)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (sin.f64 b) r) (+.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (sin.f64 a) (sin.f64 b)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (sin.f64 b) r) (Rewrite<= +-commutative_binary64 (+.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
Applied egg-rr0.3
\[\leadsto \frac{\sin b \cdot r}{\color{blue}{\mathsf{fma}\left(\cos b, \cos a, \sin b \cdot \left(-\sin a\right)\right)}}
\]
Final simplification0.3
\[\leadsto \frac{\sin b \cdot r}{\mathsf{fma}\left(\cos b, \cos a, \sin b \cdot \left(-\sin a\right)\right)}
\]