Simplified0.4
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(\sqrt{2}, \left(\sin y + -0.0625 \cdot \sin x\right) \cdot \left(\left(\sin x + -0.0625 \cdot \sin y\right) \cdot \left(\cos x - \cos y\right)\right), 2\right)}{\mathsf{fma}\left(\cos x, \frac{\sqrt{5} + -1}{0.6666666666666666}, \mathsf{fma}\left(\cos y, 4.5 - \frac{\sqrt{5}}{0.6666666666666666}, 3\right)\right)}}
\]
Proof
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (+.f64 (sin.f64 y) (*.f64 -1/16 (sin.f64 x))) (*.f64 (+.f64 (sin.f64 x) (*.f64 -1/16 (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (+.f64 (sin.f64 y) (*.f64 (Rewrite<= metadata-eval (/.f64 -1 16)) (sin.f64 x))) (*.f64 (+.f64 (sin.f64 x) (*.f64 -1/16 (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (+.f64 (sin.f64 y) (*.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) 16) (sin.f64 x))) (*.f64 (+.f64 (sin.f64 x) (*.f64 -1/16 (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (+.f64 (sin.f64 y) (Rewrite<= associate-/r/_binary64 (/.f64 (neg.f64 1) (/.f64 16 (sin.f64 x))))) (*.f64 (+.f64 (sin.f64 x) (*.f64 -1/16 (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 1 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (+.f64 (sin.f64 y) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (neg.f64 1) (sin.f64 x)) 16))) (*.f64 (+.f64 (sin.f64 x) (*.f64 -1/16 (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 1 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (+.f64 (sin.f64 y) (/.f64 (*.f64 (Rewrite=> metadata-eval -1) (sin.f64 x)) 16)) (*.f64 (+.f64 (sin.f64 x) (*.f64 -1/16 (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (+.f64 (sin.f64 y) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (sin.f64 x))) 16)) (*.f64 (+.f64 (sin.f64 x) (*.f64 -1/16 (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (+.f64 (sin.f64 y) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (sin.f64 x) 16)))) (*.f64 (+.f64 (sin.f64 x) (*.f64 -1/16 (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16))) (*.f64 (+.f64 (sin.f64 x) (*.f64 -1/16 (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (*.f64 (+.f64 (sin.f64 x) (*.f64 (Rewrite<= metadata-eval (/.f64 -1 16)) (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (*.f64 (+.f64 (sin.f64 x) (*.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) 16) (sin.f64 y))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (*.f64 (+.f64 (sin.f64 x) (Rewrite<= associate-/r/_binary64 (/.f64 (neg.f64 1) (/.f64 16 (sin.f64 y))))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (*.f64 (+.f64 (sin.f64 x) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (neg.f64 1) (sin.f64 y)) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (*.f64 (+.f64 (sin.f64 x) (/.f64 (*.f64 (Rewrite=> metadata-eval -1) (sin.f64 y)) 16)) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (*.f64 (+.f64 (sin.f64 x) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (sin.f64 y))) 16)) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (*.f64 (+.f64 (sin.f64 x) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 (sin.f64 y) 16)))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (-.f64 (cos.f64 x) (cos.f64 y)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (cos.f64 x) (cos.f64 y)) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (-.f64 (cos.f64 x) (cos.f64 y))) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 4 points increase in error, 1 points decrease in error
(/.f64 (fma.f64 (sqrt.f64 2) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16)) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (-.f64 (cos.f64 x) (cos.f64 y))))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (sqrt.f64 2) (*.f64 (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16)) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (-.f64 (cos.f64 x) (cos.f64 y))))) 2)) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 3 points increase in error, 3 points decrease in error
(/.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (sqrt.f64 2) (-.f64 (sin.f64 x) (/.f64 (sin.f64 y) 16))) (*.f64 (-.f64 (sin.f64 y) (/.f64 (sin.f64 x) 16)) (-.f64 (cos.f64 x) (cos.f64 y))))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 0 points increase in error, 8 points decrease in error
(/.f64 (+.f64 (Rewrite<= associate-*l*_binary64 (*.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)))) 2) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 3))): 3 points increase in error, 3 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))))) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) -1) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 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)))) (fma.f64 (cos.f64 x) (/.f64 (+.f64 (sqrt.f64 5) (Rewrite<= metadata-eval (neg.f64 1))) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 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)))) (fma.f64 (cos.f64 x) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (sqrt.f64 5) 1)) 2/3) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 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)))) (fma.f64 (cos.f64 x) (/.f64 (-.f64 (sqrt.f64 5) 1) (Rewrite<= metadata-eval (/.f64 2 3))) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 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)))) (fma.f64 (cos.f64 x) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 (sqrt.f64 5) 1) 3) 2)) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 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)))) (fma.f64 (cos.f64 x) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3)) (fma.f64 (cos.f64 y) (-.f64 9/2 (/.f64 (sqrt.f64 5) 2/3)) 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (fma.f64 (cos.f64 y) (-.f64 (Rewrite<= metadata-eval (/.f64 3 2/3)) (/.f64 (sqrt.f64 5) 2/3)) 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (fma.f64 (cos.f64 y) (-.f64 (/.f64 3 (Rewrite<= metadata-eval (/.f64 2 3))) (/.f64 (sqrt.f64 5) 2/3)) 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (fma.f64 (cos.f64 y) (-.f64 (/.f64 3 (/.f64 2 3)) (/.f64 (sqrt.f64 5) (Rewrite<= metadata-eval (/.f64 2 3)))) 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (fma.f64 (cos.f64 y) (Rewrite<= div-sub_binary64 (/.f64 (-.f64 3 (sqrt.f64 5)) (/.f64 2 3))) 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (fma.f64 (cos.f64 y) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 3 (sqrt.f64 5)) 3) 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (fma.f64 (cos.f64 y) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3)) 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (cos.f64 y) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) 3)) 3)))): 4 points increase in error, 2 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (cos.f64 y) (/.f64 (-.f64 3 (sqrt.f64 5)) 2)) 3)) 3))): 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y))) 3) 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (Rewrite=> distribute-lft1-in_binary64 (*.f64 (+.f64 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y)) 1) 3)))): 18 points increase in error, 13 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)))) (fma.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3) (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y)))) 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)))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (cos.f64 x) (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) 3)) (*.f64 (+.f64 1 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y))) 3)))): 9 points increase in error, 8 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<= associate-*l*_binary64 (*.f64 (*.f64 (cos.f64 x) (/.f64 (-.f64 (sqrt.f64 5) 1) 2)) 3)) (*.f64 (+.f64 1 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y))) 3))): 7 points increase in error, 7 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 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x))) 3) (*.f64 (+.f64 1 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y))) 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)))) (Rewrite<= distribute-rgt-in_binary64 (*.f64 3 (+.f64 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x)) (+.f64 1 (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y))))))): 17 points increase in error, 21 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 (*.f64 (/.f64 (-.f64 (sqrt.f64 5) 1) 2) (cos.f64 x)) 1) (*.f64 (/.f64 (-.f64 3 (sqrt.f64 5)) 2) (cos.f64 y)))))): 9 points increase in error, 7 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<= +-commutative_binary64 (+.f64 1 (*.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