Simplified0.3
\[\leadsto \color{blue}{\frac{2}{r \cdot r} + \left(-1.5 - \frac{w}{\frac{\frac{1 - v}{\mathsf{fma}\left(v, -0.25, 0.375\right)}}{r}} \cdot \left(r \cdot w\right)\right)}
\]
Proof
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 -3/2 (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (fma.f64 v -1/4 3/8)) r)) (*.f64 r w)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (Rewrite<= metadata-eval (+.f64 -9/2 3)) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (fma.f64 v -1/4 3/8)) r)) (*.f64 r w)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (Rewrite<= metadata-eval (neg.f64 9/2)) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (fma.f64 v -1/4 3/8)) r)) (*.f64 r w)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (fma.f64 v (Rewrite<= metadata-eval (*.f64 1/8 -2)) 3/8)) r)) (*.f64 r w)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (fma.f64 v (*.f64 1/8 (Rewrite<= metadata-eval (neg.f64 2))) 3/8)) r)) (*.f64 r w)))): 19 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (fma.f64 v (*.f64 1/8 (neg.f64 2)) (Rewrite<= metadata-eval (*.f64 1/8 3)))) r)) (*.f64 r w)))): 0 points increase in error, 19 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 v (*.f64 1/8 (neg.f64 2))) (*.f64 1/8 3)))) r)) (*.f64 r w)))): 19 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 1/8 (neg.f64 2)) v)) (*.f64 1/8 3))) r)) (*.f64 r w)))): 0 points increase in error, 19 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 1/8 (*.f64 (neg.f64 2) v))) (*.f64 1/8 3))) r)) (*.f64 r w)))): 16 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (+.f64 (*.f64 1/8 (Rewrite<= distribute-lft-neg-in_binary64 (neg.f64 (*.f64 2 v)))) (*.f64 1/8 3))) r)) (*.f64 r w)))): 16 points increase in error, 16 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 1/8 3) (*.f64 1/8 (neg.f64 (*.f64 2 v)))))) r)) (*.f64 r w)))): 0 points increase in error, 32 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (Rewrite<= distribute-lft-in_binary64 (*.f64 1/8 (+.f64 3 (neg.f64 (*.f64 2 v)))))) r)) (*.f64 r w)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (*.f64 1/8 (Rewrite<= sub-neg_binary64 (-.f64 3 (*.f64 2 v))))) r)) (*.f64 r w)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (Rewrite<= associate-/r*_binary64 (/.f64 (-.f64 1 v) (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) r)))) (*.f64 r w)))): 31 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (*.f64 (/.f64 w (/.f64 (-.f64 1 v) (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) r))) (Rewrite<= *-commutative_binary64 (*.f64 w r))))): 1 points increase in error, 30 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (Rewrite<= associate-/r/_binary64 (/.f64 w (/.f64 (/.f64 (-.f64 1 v) (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) r)) (*.f64 w r)))))): 0 points increase in error, 16 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 w (*.f64 w r)) (/.f64 (-.f64 1 v) (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) r)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 w w) r)) (/.f64 (-.f64 1 v) (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) r))))): 14 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 (*.f64 w w) r) (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) r)) (-.f64 1 v))))): 0 points increase in error, 14 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) r) (*.f64 (*.f64 w w) r))) (-.f64 1 v)))): 29 points increase in error, 0 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 r (*.f64 (*.f64 w w) r)))) (-.f64 1 v)))): 2 points increase in error, 29 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (-.f64 (+.f64 (neg.f64 9/2) 3) (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 (*.f64 w w) r) r))) (-.f64 1 v)))): 0 points increase in error, 16 points decrease in error
(+.f64 (/.f64 2 (*.f64 r r)) (Rewrite=> sub-neg_binary64 (+.f64 (+.f64 (neg.f64 9/2) 3) (neg.f64 (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v)))))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 (/.f64 2 (*.f64 r r)) (+.f64 (neg.f64 9/2) 3)) (neg.f64 (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v))))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 (neg.f64 9/2) 3) (/.f64 2 (*.f64 r r)))) (neg.f64 (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v)))): 14 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-+r+_binary64 (+.f64 (neg.f64 9/2) (+.f64 3 (/.f64 2 (*.f64 r r))))) (neg.f64 (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v)))): 3 points increase in error, 1 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 3 (/.f64 2 (*.f64 r r))) (neg.f64 9/2))) (neg.f64 (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v)))): 0 points increase in error, 16 points decrease in error
(+.f64 (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 3 (/.f64 2 (*.f64 r r))) 9/2)) (neg.f64 (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v))) (-.f64 (+.f64 3 (/.f64 2 (*.f64 r r))) 9/2))): 7 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (neg.f64 (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v))) (+.f64 3 (/.f64 2 (*.f64 r r)))) 9/2)): 0 points increase in error, 7 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 3 (/.f64 2 (*.f64 r r))) (neg.f64 (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v))))) 9/2): 7 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= sub-neg_binary64 (-.f64 (+.f64 3 (/.f64 2 (*.f64 r r))) (/.f64 (*.f64 (*.f64 1/8 (-.f64 3 (*.f64 2 v))) (*.f64 (*.f64 (*.f64 w w) r) r)) (-.f64 1 v)))) 9/2): 0 points increase in error, 7 points decrease in error