Initial program 14.8
\[r \cdot \frac{\sin b}{\cos \left(a + b\right)}
\]
Simplified14.8
\[\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}{\cos b \cdot \cos a - \sin b \cdot \sin a}}
\]
Applied egg-rr0.3
\[\leadsto r \cdot \frac{\sin b}{\cos b \cdot \cos a - \color{blue}{\mathsf{log1p}\left(\mathsf{expm1}\left(\sin b \cdot \sin a\right)\right)}}
\]
Taylor expanded in b around inf 0.3
\[\leadsto r \cdot \color{blue}{\frac{\sin b}{\cos a \cdot \cos b - \sin a \cdot \sin b}}
\]
Simplified0.3
\[\leadsto r \cdot \color{blue}{\frac{\sin b}{\mathsf{fma}\left(\sin a, -\sin b, \cos a \cdot \cos b\right)}}
\]
Proof
(/.f64 (sin.f64 b) (fma.f64 (sin.f64 a) (neg.f64 (sin.f64 b)) (*.f64 (cos.f64 a) (cos.f64 b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (sin.f64 b) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (sin.f64 a) (neg.f64 (sin.f64 b))) (*.f64 (cos.f64 a) (cos.f64 b))))): 7 points increase in error, 10 points decrease in error
(/.f64 (sin.f64 b) (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (sin.f64 a) (sin.f64 b)))) (*.f64 (cos.f64 a) (cos.f64 b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (sin.f64 b) (+.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 (sin.f64 a)) (sin.f64 b))) (*.f64 (cos.f64 a) (cos.f64 b)))): 0 points increase in error, 0 points decrease in error
(/.f64 (sin.f64 b) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (cos.f64 a) (cos.f64 b)) (*.f64 (neg.f64 (sin.f64 a)) (sin.f64 b))))): 0 points increase in error, 0 points decrease in error
(/.f64 (sin.f64 b) (Rewrite<= cancel-sign-sub-inv_binary64 (-.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
Final simplification0.3
\[\leadsto r \cdot \frac{\sin b}{\mathsf{fma}\left(\sin a, -\sin b, \cos a \cdot \cos b\right)}
\]