Simplified44.2
\[\leadsto \color{blue}{\mathsf{fma}\left(\frac{{\left(a \cdot \cos \left(\frac{angle}{180} \cdot \pi\right)\right)}^{2} + {\left(b \cdot \sin \left(\frac{angle}{180} \cdot \pi\right)\right)}^{2}}{y-scale \cdot y-scale}, \frac{{\left(a \cdot \sin \left(\frac{angle}{180} \cdot \pi\right)\right)}^{2} + {\left(b \cdot \cos \left(\frac{angle}{180} \cdot \pi\right)\right)}^{2}}{x-scale \cdot x-scale} \cdot -4, \frac{b \cdot b - a \cdot a}{\frac{\frac{x-scale \cdot y-scale}{\cos \left(\frac{angle}{180} \cdot \pi\right)}}{2 \cdot \sin \left(\frac{angle}{180} \cdot \pi\right)}} \cdot \frac{b \cdot b - a \cdot a}{\frac{\frac{x-scale \cdot y-scale}{\cos \left(\frac{angle}{180} \cdot \pi\right)}}{2 \cdot \sin \left(\frac{angle}{180} \cdot \pi\right)}}\right)}
\]
Proof
(fma.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) (*.f64 y-scale y-scale)) (*.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) (*.f64 x-scale x-scale)) -4) (*.f64 (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale)) (*.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) (*.f64 x-scale x-scale)) -4) (*.f64 (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 1 points increase in error, 17 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (*.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale)) -4) (*.f64 (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 6 points increase in error, 22 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (*.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale) (Rewrite<= metadata-eval (neg.f64 4))) (*.f64 (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale) 4))) (*.f64 (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale)))) (*.f64 (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 b 2)) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (-.f64 (pow.f64 b 2) (Rewrite<= unpow2_binary64 (pow.f64 a 2))) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)) (/.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 y-scale x-scale)) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)) (/.f64 (Rewrite<= associate-*r/_binary64 (*.f64 y-scale (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 2 points increase in error, 3 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64))))) (*.f64 y-scale (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64))))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 5 points increase in error, 7 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)) 2) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64))))) (*.f64 y-scale (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2)))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 y-scale (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64))))) y-scale)) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 5 points increase in error, 9 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale)) y-scale) (/.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 1 points increase in error, 2 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (-.f64 (Rewrite<= unpow2_binary64 (pow.f64 b 2)) (*.f64 a a)) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (-.f64 (pow.f64 b 2) (Rewrite<= unpow2_binary64 (pow.f64 a 2))) (/.f64 (/.f64 (*.f64 x-scale y-scale) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)) (/.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 y-scale x-scale)) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)) (/.f64 (Rewrite<= associate-*r/_binary64 (*.f64 y-scale (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 3 points increase in error, 2 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)) (*.f64 2 (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64))))) (*.f64 y-scale (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64))))))))): 7 points increase in error, 5 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (-.f64 (pow.f64 b 2) (pow.f64 a 2)) 2) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64))))) (*.f64 y-scale (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2)))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (*.f64 y-scale (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (/.f64 x-scale (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64))))) y-scale)))): 7 points increase in error, 16 points decrease in error
(fma.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale)) y-scale))): 1 points increase in error, 3 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale) (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale)))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale)))): 10 points increase in error, 16 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale))) (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale)) (*.f64 (neg.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale))) (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale) (/.f64 (/.f64 (*.f64 (*.f64 (*.f64 2 (-.f64 (pow.f64 b 2) (pow.f64 a 2))) (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) x-scale) y-scale)) (*.f64 (*.f64 4 (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) x-scale) x-scale)) (/.f64 (/.f64 (+.f64 (pow.f64 (*.f64 a (cos.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2) (pow.f64 (*.f64 b (sin.f64 (*.f64 (/.f64 angle 180) (PI.f64)))) 2)) y-scale) y-scale)))): 0 points increase in error, 0 points decrease in error
Simplified5.5
\[\leadsto \color{blue}{-4 \cdot \left(\left(\frac{b}{x-scale} \cdot \frac{a}{y-scale}\right) \cdot \left(\frac{b}{x-scale} \cdot \frac{a}{y-scale}\right)\right)}
\]
Proof
(*.f64 -4 (*.f64 (*.f64 (/.f64 b x-scale) (/.f64 a y-scale)) (*.f64 (/.f64 b x-scale) (/.f64 a y-scale)))): 0 points increase in error, 0 points decrease in error
(*.f64 -4 (Rewrite<= unswap-sqr_binary64 (*.f64 (*.f64 (/.f64 b x-scale) (/.f64 b x-scale)) (*.f64 (/.f64 a y-scale) (/.f64 a y-scale))))): 73 points increase in error, 25 points decrease in error
(*.f64 -4 (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 b b) (*.f64 x-scale x-scale))) (*.f64 (/.f64 a y-scale) (/.f64 a y-scale)))): 60 points increase in error, 6 points decrease in error
(*.f64 -4 (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 b 2)) (*.f64 x-scale x-scale)) (*.f64 (/.f64 a y-scale) (/.f64 a y-scale)))): 0 points increase in error, 0 points decrease in error
(*.f64 -4 (*.f64 (/.f64 (pow.f64 b 2) (Rewrite<= unpow2_binary64 (pow.f64 x-scale 2))) (*.f64 (/.f64 a y-scale) (/.f64 a y-scale)))): 0 points increase in error, 0 points decrease in error
(*.f64 -4 (*.f64 (/.f64 (pow.f64 b 2) (pow.f64 x-scale 2)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 a a) (*.f64 y-scale y-scale))))): 38 points increase in error, 1 points decrease in error
(*.f64 -4 (*.f64 (/.f64 (pow.f64 b 2) (pow.f64 x-scale 2)) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 a 2)) (*.f64 y-scale y-scale)))): 0 points increase in error, 0 points decrease in error
(*.f64 -4 (*.f64 (/.f64 (pow.f64 b 2) (pow.f64 x-scale 2)) (/.f64 (pow.f64 a 2) (Rewrite<= unpow2_binary64 (pow.f64 y-scale 2))))): 0 points increase in error, 0 points decrease in error
(*.f64 -4 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 a 2) (pow.f64 y-scale 2)) (/.f64 (pow.f64 b 2) (pow.f64 x-scale 2))))): 0 points increase in error, 0 points decrease in error
(*.f64 -4 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (pow.f64 a 2) (pow.f64 b 2)) (*.f64 (pow.f64 y-scale 2) (pow.f64 x-scale 2))))): 11 points increase in error, 8 points decrease in error
Simplified6.1
\[\leadsto -4 \cdot \color{blue}{{\left(a \cdot \frac{\frac{b}{x-scale}}{y-scale}\right)}^{2}}
\]
Proof
(pow.f64 (*.f64 a (/.f64 (/.f64 b x-scale) y-scale)) 2): 0 points increase in error, 0 points decrease in error
(pow.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (/.f64 b x-scale) y-scale) a)) 2): 0 points increase in error, 0 points decrease in error
(pow.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (/.f64 b x-scale) a) y-scale)) 2): 30 points increase in error, 24 points decrease in error
(pow.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 b x-scale) (/.f64 a y-scale))) 2): 30 points increase in error, 32 points decrease in error
(Rewrite=> unpow2_binary64 (*.f64 (*.f64 (/.f64 b x-scale) (/.f64 a y-scale)) (*.f64 (/.f64 b x-scale) (/.f64 a y-scale)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> swap-sqr_binary64 (*.f64 (*.f64 (/.f64 b x-scale) (/.f64 b x-scale)) (*.f64 (/.f64 a y-scale) (/.f64 a y-scale)))): 70 points increase in error, 30 points decrease in error
(*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 b b) (*.f64 x-scale x-scale))) (*.f64 (/.f64 a y-scale) (/.f64 a y-scale))): 51 points increase in error, 16 points decrease in error
(*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 b 2)) (*.f64 x-scale x-scale)) (*.f64 (/.f64 a y-scale) (/.f64 a y-scale))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (pow.f64 b 2) (Rewrite<= unpow2_binary64 (pow.f64 x-scale 2))) (*.f64 (/.f64 a y-scale) (/.f64 a y-scale))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (pow.f64 b 2) (pow.f64 x-scale 2)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 a a) (*.f64 y-scale y-scale)))): 32 points increase in error, 7 points decrease in error
(*.f64 (/.f64 (pow.f64 b 2) (pow.f64 x-scale 2)) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 a 2)) (*.f64 y-scale y-scale))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (pow.f64 b 2) (pow.f64 x-scale 2)) (/.f64 (pow.f64 a 2) (Rewrite<= unpow2_binary64 (pow.f64 y-scale 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 (pow.f64 b 2) (pow.f64 a 2)) (*.f64 (pow.f64 x-scale 2) (pow.f64 y-scale 2)))): 13 points increase in error, 7 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 a 2) (pow.f64 b 2))) (*.f64 (pow.f64 x-scale 2) (pow.f64 y-scale 2))): 0 points increase in error, 0 points decrease in error