Simplified0.5
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(\sqrt{2}, \left(\cos x - \cos y\right) \cdot \left(\left(\sin x - \frac{\sin y}{16}\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right), 2\right)}{3 + \mathsf{fma}\left(\cos y, \frac{3 - \sqrt{5}}{0.6666666666666666}, \frac{\cos x \cdot \left(\sqrt{5} + -1\right)}{0.6666666666666666}\right)}}
\]
Proof
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (cos.f64 x) (cos.f64 y)) (*.f64 (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16)) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)))) 2) (+.f64 3 (fma.f64 (cos.f64 y) (/.f64 (-.f64 3 (sqrt.f64 5)) 2/3) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) -1)) 2/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16)) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (+.f64 3 (fma.f64 (cos.f64 y) (/.f64 (-.f64 3 (sqrt.f64 5)) 2/3) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) -1)) 2/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (sqrt.f64 2) (*.f64 (*.f64 (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16)) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2)) (+.f64 3 (fma.f64 (cos.f64 y) (/.f64 (-.f64 3 (sqrt.f64 5)) 2/3) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) -1)) 2/3)))): 2 points increase in error, 5 points decrease in error
(/.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16)) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (+.f64 3 (fma.f64 (cos.f64 y) (/.f64 (-.f64 3 (sqrt.f64 5)) 2/3) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) -1)) 2/3)))): 2 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (*.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)))) (-.f64 (cos.f64 x) (cos.f64 y))) 2) (+.f64 3 (fma.f64 (cos.f64 y) (/.f64 (-.f64 3 (sqrt.f64 5)) 2/3) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) -1)) 2/3)))): 0 points increase in error, 2 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y))))) (+.f64 3 (fma.f64 (cos.f64 y) (/.f64 (-.f64 3 (sqrt.f64 5)) 2/3) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) -1)) 2/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (/.f64 (-.f64 3 (sqrt.f64 5)) (Rewrite<= metadata-eval (/.f64 2 3))) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) -1)) 2/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 3 (sqrt.f64 5)) 3) 2)) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) -1)) 2/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3)) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) -1)) 2/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3) (/.f64 (*.f64 (cos.f64 x) (+.f64 (sqrt.f64 5) (Rewrite<= metadata-eval (neg.f64 1)))) 2/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3) (/.f64 (*.f64 (cos.f64 x) (Rewrite<= sub-neg_binary64 (-.f64 (sqrt.f64 5) 1))) 2/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (sqrt.f64 5) 1) (cos.f64 x))) 2/3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3) (/.f64 (*.f64 (-.f64 (sqrt.f64 5) 1) (cos.f64 x)) (Rewrite<= metadata-eval (/.f64 2 3)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 (-.f64 (sqrt.f64 5) 1) (cos.f64 x)) 3) 2))))): 5 points increase in error, 11 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (*.f64 (-.f64 (sqrt.f64 5) 1) (cos.f64 x)) 2) 3))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3) (*.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x))) 3)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (fma.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3) (Rewrite<= *-commutative_binary64 (*.f64 3 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x))))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3)) (*.f64 3 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x))))))): 2 points increase in error, 4 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (cos.f64 y) (/.f64 (-.f64 3 (sqrt.f64 5)) 2)) 3)) (*.f64 3 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x)))))): 4 points increase in error, 4 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y))) 3) (*.f64 3 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (+.f64 (*.f64 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y)) 3) (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x)) 3))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (Rewrite<= distribute-rgt-in_binary64 (*.f64 3 (+.f64 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y)) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x))))))): 9 points increase in error, 11 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 3 (*.f64 3 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x)) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y))))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (+.f64 (Rewrite<= metadata-eval (*.f64 3 1)) (*.f64 3 (+.f64 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x)) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (Rewrite<= distribute-lft-in_binary64 (*.f64 3 (+.f64 1 (+.f64 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x)) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y))))))): 21 points increase in error, 20 points decrease in error
(/.f64 (+.f64 2 (*.f64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) (*.f64 3 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 1 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x))) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y)))))): 9 points increase in error, 8 points decrease in error
Simplified0.4
\[\leadsto \frac{\mathsf{fma}\left(\sqrt{2}, \left(\cos x - \cos y\right) \cdot \left(\left(\sin x - \frac{\sin y}{16}\right) \cdot \left(\sin y - \frac{\sin x}{16}\right)\right), 2\right)}{3 + \color{blue}{\mathsf{fma}\left(\cos x, 1.5 \cdot \left(\sqrt{5} + -1\right), \cos y \cdot \frac{6}{\sqrt{5} + 3}\right)}}
\]
Proof
(fma.f64 (cos.f64 x) (*.f64 3/2 (+.f64 (sqrt.f64 5) -1)) (*.f64 (cos.f64 y) (/.f64 6 (+.f64 (sqrt.f64 5) 3)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 x) (*.f64 3/2 (+.f64 (sqrt.f64 5) (Rewrite<= metadata-eval (neg.f64 1)))) (*.f64 (cos.f64 y) (/.f64 6 (+.f64 (sqrt.f64 5) 3)))): 0 points increase in error, 0 points decrease in error
(fma.f64 (cos.f64 x) (*.f64 3/2 (Rewrite<= sub-neg_binary64 (-.f64 (sqrt.f64 5) 1))) (*.f64 (cos.f64 y) (/.f64 6 (+.f64 (sqrt.f64 5) 3)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> fma-udef_binary64 (+.f64 (*.f64 (cos.f64 x) (*.f64 3/2 (-.f64 (sqrt.f64 5) 1))) (*.f64 (cos.f64 y) (/.f64 6 (+.f64 (sqrt.f64 5) 3))))): 17 points increase in error, 23 points decrease in error
(+.f64 (*.f64 (cos.f64 x) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (sqrt.f64 5) 1) 3/2))) (*.f64 (cos.f64 y) (/.f64 6 (+.f64 (sqrt.f64 5) 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (cos.f64 x) (*.f64 (Rewrite=> sub-neg_binary64 (+.f64 (sqrt.f64 5) (neg.f64 1))) 3/2)) (*.f64 (cos.f64 y) (/.f64 6 (+.f64 (sqrt.f64 5) 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (cos.f64 x) (*.f64 (+.f64 (sqrt.f64 5) (Rewrite=> metadata-eval -1)) 3/2)) (*.f64 (cos.f64 y) (/.f64 6 (+.f64 (sqrt.f64 5) 3)))): 0 points increase in error, 0 points decrease in error