Initial program 53.3
\[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right)
\]
Simplified57.9
\[\leadsto \color{blue}{\frac{\frac{c0}{2}}{w} \cdot \mathsf{fma}\left(d \cdot d, \frac{c0}{w \cdot \left(h \cdot \left(D \cdot D\right)\right)}, \sqrt{\mathsf{fma}\left(\frac{c0}{w \cdot h}, \frac{c0}{w \cdot h} \cdot {\left(\frac{d}{D}\right)}^{4}, M \cdot \left(-M\right)\right)}\right)}
\]
Proof
(*.f64 (/.f64 (/.f64 c0 2) w) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 w (*.f64 h (*.f64 D D)))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) 4)) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 c0 (*.f64 2 w))) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 w (*.f64 h (*.f64 D D)))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) 4)) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) 4)) (*.f64 M (neg.f64 M)))))): 1 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) (Rewrite<= metadata-eval (+.f64 3 1)))) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (Rewrite<= pow-plus_binary64 (*.f64 (pow.f64 (/.f64 d D) 3) (/.f64 d D)))) (*.f64 M (neg.f64 M)))))): 1 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (Rewrite=> unpow3_binary64 (*.f64 (*.f64 (/.f64 d D) (/.f64 d D)) (/.f64 d D))) (/.f64 d D))) (*.f64 M (neg.f64 M)))))): 1 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 d d) (*.f64 D D))) (/.f64 d D)) (/.f64 d D))) (*.f64 M (neg.f64 M)))))): 3 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (Rewrite<= associate-*r*_binary64 (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (*.f64 (/.f64 d D) (/.f64 d D))))) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M (neg.f64 M)))))): 1 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (/.f64 (*.f64 d d) (*.f64 D D)))) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 M M))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 c0 (*.f64 w h))) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M M))))): 2 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M M))))): 0 points increase in error, 7 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D)))) (*.f64 M M))))): 4 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))))) (*.f64 M M))))): 1 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M)))))): 0 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (*.f64 d d))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))): 0 points increase in error, 2 points decrease in error
Taylor expanded in c0 around inf 56.0
\[\leadsto \color{blue}{\frac{{d}^{2} \cdot {c0}^{2}}{{D}^{2} \cdot \left({w}^{2} \cdot h\right)}}
\]
Simplified51.4
\[\leadsto \color{blue}{\left(\frac{d}{D \cdot D} \cdot d\right) \cdot \frac{c0 \cdot c0}{w \cdot \left(w \cdot h\right)}}
\]
Proof
(*.f64 (*.f64 (/.f64 d (*.f64 D D)) d) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (/.f64 d (Rewrite<= unpow2_binary64 (pow.f64 D 2))) d) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/r/_binary64 (/.f64 d (/.f64 (pow.f64 D 2) d))) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 1 points increase in error, 3 points decrease in error
(*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 d d) (pow.f64 D 2))) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 10 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) (pow.f64 D 2)) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (pow.f64 d 2) (pow.f64 D 2)) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c0 2)) (*.f64 w (*.f64 w h)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (pow.f64 d 2) (pow.f64 D 2)) (/.f64 (pow.f64 c0 2) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 w w) h)))): 2 points increase in error, 1 points decrease in error
(*.f64 (/.f64 (pow.f64 d 2) (pow.f64 D 2)) (/.f64 (pow.f64 c0 2) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 w 2)) h))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 (pow.f64 d 2) (pow.f64 c0 2)) (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)))): 5 points increase in error, 9 points decrease in error
Taylor expanded in d around 0 56.0
\[\leadsto \color{blue}{\frac{{d}^{2} \cdot {c0}^{2}}{{D}^{2} \cdot \left({w}^{2} \cdot h\right)}}
\]
Simplified35.7
\[\leadsto \color{blue}{d \cdot \left(\frac{d}{D \cdot w} \cdot \frac{c0}{\left(w \cdot h\right) \cdot \frac{D}{c0}}\right)}
\]
Proof
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (/.f64 c0 (*.f64 (*.f64 w h) (/.f64 D c0))))): 0 points increase in error, 0 points decrease in error
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (/.f64 c0 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 h w)) (/.f64 D c0))))): 0 points increase in error, 0 points decrease in error
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 c0 (/.f64 D c0)) (*.f64 h w))))): 23 points increase in error, 15 points decrease in error
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c0 c0) D)) (*.f64 h w)))): 15 points increase in error, 11 points decrease in error
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (/.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c0 2)) D) (*.f64 h w)))): 0 points increase in error, 0 points decrease in error
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (Rewrite=> associate-/l/_binary64 (/.f64 (pow.f64 c0 2) (*.f64 (*.f64 h w) D))))): 18 points increase in error, 9 points decrease in error
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (/.f64 (pow.f64 c0 2) (Rewrite<= *-commutative_binary64 (*.f64 D (*.f64 h w)))))): 0 points increase in error, 0 points decrease in error
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (/.f64 (pow.f64 c0 2) (*.f64 D (Rewrite=> *-commutative_binary64 (*.f64 w h)))))): 0 points increase in error, 0 points decrease in error
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (/.f64 (pow.f64 c0 2) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 D w) h))))): 5 points increase in error, 15 points decrease in error
(*.f64 d (*.f64 (/.f64 d (*.f64 D w)) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (pow.f64 c0 2) h) (*.f64 D w))))): 14 points increase in error, 25 points decrease in error
(*.f64 d (Rewrite<= associate-/r/_binary64 (/.f64 d (/.f64 (*.f64 D w) (/.f64 (/.f64 (pow.f64 c0 2) h) (*.f64 D w)))))): 16 points increase in error, 22 points decrease in error
(*.f64 d (/.f64 d (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D w) (*.f64 D w)) (/.f64 (pow.f64 c0 2) h))))): 30 points increase in error, 5 points decrease in error
(*.f64 d (/.f64 d (/.f64 (Rewrite<= unswap-sqr_binary64 (*.f64 (*.f64 D D) (*.f64 w w))) (/.f64 (pow.f64 c0 2) h)))): 33 points increase in error, 5 points decrease in error
(*.f64 d (/.f64 d (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 w w)) (/.f64 (pow.f64 c0 2) h)))): 0 points increase in error, 0 points decrease in error
(*.f64 d (/.f64 d (/.f64 (*.f64 (pow.f64 D 2) (Rewrite<= unpow2_binary64 (pow.f64 w 2))) (/.f64 (pow.f64 c0 2) h)))): 0 points increase in error, 0 points decrease in error
(*.f64 d (/.f64 d (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 (pow.f64 D 2) (pow.f64 w 2)) h) (pow.f64 c0 2))))): 5 points increase in error, 9 points decrease in error
(*.f64 d (/.f64 d (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h))) (pow.f64 c0 2)))): 9 points increase in error, 4 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 d (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)) (pow.f64 c0 2))) d)): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 d d) (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)) (pow.f64 c0 2)))): 37 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)) (pow.f64 c0 2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 d 2) (pow.f64 c0 2)) (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)))): 5 points increase in error, 1 points decrease in error
Taylor expanded in d around 0 56.0
\[\leadsto \color{blue}{\frac{{d}^{2} \cdot {c0}^{2}}{{D}^{2} \cdot \left({w}^{2} \cdot h\right)}}
\]
Simplified33.8
\[\leadsto \color{blue}{d \cdot \left(\frac{d}{D} \cdot \frac{c0}{D \cdot \frac{w}{\frac{\frac{c0}{w}}{h}}}\right)}
\]
Proof
(*.f64 d (*.f64 (/.f64 d D) (/.f64 c0 (*.f64 D (/.f64 w (/.f64 (/.f64 c0 w) h)))))): 0 points increase in error, 0 points decrease in error
(*.f64 d (*.f64 (/.f64 d D) (/.f64 c0 (*.f64 D (/.f64 w (Rewrite<= associate-/r*_binary64 (/.f64 c0 (*.f64 w h)))))))): 5 points increase in error, 11 points decrease in error
(*.f64 d (*.f64 (/.f64 d D) (/.f64 c0 (*.f64 D (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 w (*.f64 w h)) c0)))))): 18 points increase in error, 11 points decrease in error
(*.f64 d (*.f64 (/.f64 d D) (/.f64 c0 (*.f64 D (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 w w) h)) c0))))): 8 points increase in error, 8 points decrease in error
(*.f64 d (*.f64 (/.f64 d D) (/.f64 c0 (*.f64 D (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 w 2)) h) c0))))): 0 points increase in error, 0 points decrease in error
(*.f64 d (*.f64 (/.f64 d D) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 c0 (/.f64 (*.f64 (pow.f64 w 2) h) c0)) D)))): 14 points increase in error, 4 points decrease in error
(*.f64 d (*.f64 (/.f64 d D) (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 c0 c0) (*.f64 (pow.f64 w 2) h))) D))): 15 points increase in error, 5 points decrease in error
(*.f64 d (*.f64 (/.f64 d D) (/.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c0 2)) (*.f64 (pow.f64 w 2) h)) D))): 0 points increase in error, 0 points decrease in error
(*.f64 d (Rewrite<= times-frac_binary64 (/.f64 (*.f64 d (/.f64 (pow.f64 c0 2) (*.f64 (pow.f64 w 2) h))) (*.f64 D D)))): 28 points increase in error, 13 points decrease in error
(*.f64 d (/.f64 (*.f64 d (/.f64 (pow.f64 c0 2) (*.f64 (pow.f64 w 2) h))) (Rewrite<= unpow2_binary64 (pow.f64 D 2)))): 0 points increase in error, 0 points decrease in error
(*.f64 d (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 d (pow.f64 D 2)) (/.f64 (pow.f64 c0 2) (*.f64 (pow.f64 w 2) h))))): 25 points increase in error, 4 points decrease in error
(*.f64 d (Rewrite<= times-frac_binary64 (/.f64 (*.f64 d (pow.f64 c0 2)) (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h))))): 9 points increase in error, 25 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (*.f64 d (pow.f64 c0 2)) (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h))) d)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite=> associate-/l*_binary64 (/.f64 d (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)) (pow.f64 c0 2)))) d): 2 points increase in error, 14 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 d (/.f64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)) (pow.f64 c0 2)) d))): 3 points increase in error, 2 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 d d) (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)) (pow.f64 c0 2)))): 35 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)) (pow.f64 c0 2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 d 2) (pow.f64 c0 2)) (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)))): 5 points increase in error, 1 points decrease in error
Initial program 27.6
\[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right)
\]
Taylor expanded in c0 around -inf 34.0
\[\leadsto \color{blue}{-0.5 \cdot \frac{\left(\frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)} + -1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)}\right) \cdot {c0}^{2}}{w} + 0.25 \cdot \frac{{D}^{2} \cdot \left({M}^{2} \cdot h\right)}{{d}^{2}}}
\]
Simplified25.5
\[\leadsto \color{blue}{\mathsf{fma}\left(0.25, \frac{D}{\frac{d \cdot d}{D}} \cdot \left(\left(h \cdot M\right) \cdot M\right), 0\right)}
\]
Proof
(fma.f64 1/4 (*.f64 (/.f64 D (/.f64 (*.f64 d d) D)) (*.f64 (*.f64 h M) M)) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (*.f64 (/.f64 D (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) D)) (*.f64 (*.f64 h M) M)) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 D D) (pow.f64 d 2))) (*.f64 (*.f64 h M) M)) 0): 28 points increase in error, 2 points decrease in error
(fma.f64 1/4 (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (pow.f64 d 2)) (*.f64 (*.f64 h M) M)) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (*.f64 (/.f64 (pow.f64 D 2) (pow.f64 d 2)) (Rewrite<= associate-*r*_binary64 (*.f64 h (*.f64 M M)))) 0): 16 points increase in error, 3 points decrease in error
(fma.f64 1/4 (*.f64 (/.f64 (pow.f64 D 2) (pow.f64 d 2)) (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 D 2) (/.f64 (pow.f64 d 2) (*.f64 h (pow.f64 M 2))))) 0): 7 points increase in error, 7 points decrease in error
(fma.f64 1/4 (/.f64 (pow.f64 D 2) (/.f64 (pow.f64 d 2) (Rewrite=> *-commutative_binary64 (*.f64 (pow.f64 M 2) h)))) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))) 0): 3 points increase in error, 6 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= div0_binary64 (/.f64 0 (/.f64 w (pow.f64 c0 2))))): 48 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (Rewrite<= metadata-eval (*.f64 -1/2 0)) (/.f64 w (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (*.f64 -1/2 (Rewrite<= mul0-lft_binary64 (*.f64 0 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))))) (/.f64 w (pow.f64 c0 2)))): 93 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (*.f64 -1/2 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (/.f64 w (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (*.f64 -1/2 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))))) (/.f64 w (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= associate-*r/_binary64 (*.f64 -1/2 (/.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (/.f64 w (pow.f64 c0 2)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 1 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))) (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr18.8
\[\leadsto \mathsf{fma}\left(0.25, \color{blue}{0 + h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}}, 0\right)
\]
Applied egg-rr18.9
\[\leadsto \mathsf{fma}\left(0.25, 0 + h \cdot \color{blue}{\left(\left(\left(M \cdot \frac{D}{d}\right) \cdot \frac{D}{d}\right) \cdot M\right)}, 0\right)
\]
Initial program 51.6
\[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right)
\]
Simplified56.6
\[\leadsto \color{blue}{\frac{\frac{c0}{2}}{w} \cdot \mathsf{fma}\left(d \cdot d, \frac{c0}{w \cdot \left(h \cdot \left(D \cdot D\right)\right)}, \sqrt{\mathsf{fma}\left(\frac{c0}{w \cdot h}, \frac{c0}{w \cdot h} \cdot {\left(\frac{d}{D}\right)}^{4}, M \cdot \left(-M\right)\right)}\right)}
\]
Proof
(*.f64 (/.f64 (/.f64 c0 2) w) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 w (*.f64 h (*.f64 D D)))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) 4)) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 c0 (*.f64 2 w))) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 w (*.f64 h (*.f64 D D)))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) 4)) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) 4)) (*.f64 M (neg.f64 M)))))): 1 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (pow.f64 (/.f64 d D) (Rewrite<= metadata-eval (+.f64 3 1)))) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (Rewrite<= pow-plus_binary64 (*.f64 (pow.f64 (/.f64 d D) 3) (/.f64 d D)))) (*.f64 M (neg.f64 M)))))): 1 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (Rewrite=> unpow3_binary64 (*.f64 (*.f64 (/.f64 d D) (/.f64 d D)) (/.f64 d D))) (/.f64 d D))) (*.f64 M (neg.f64 M)))))): 1 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 d d) (*.f64 D D))) (/.f64 d D)) (/.f64 d D))) (*.f64 M (neg.f64 M)))))): 3 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (Rewrite<= associate-*r*_binary64 (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (*.f64 (/.f64 d D) (/.f64 d D))))) (*.f64 M (neg.f64 M)))))): 0 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M (neg.f64 M)))))): 1 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (/.f64 (*.f64 d d) (*.f64 D D)))) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 M M))))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 c0 (*.f64 w h)) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 c0 (*.f64 w h))) (*.f64 (/.f64 (*.f64 d d) (*.f64 D D)) (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M M))))): 2 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (Rewrite<= swap-sqr_binary64 (*.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))))) (*.f64 M M))))): 0 points increase in error, 7 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D)))) (*.f64 M M))))): 4 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (fma.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))))) (*.f64 M M))))): 1 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (*.f64 d d) (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M)))))): 0 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 c0 (*.f64 (*.f64 w h) (*.f64 D D))) (*.f64 d d))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (-.f64 (*.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (*.f64 M M))))): 0 points increase in error, 2 points decrease in error
Taylor expanded in c0 around inf 54.2
\[\leadsto \color{blue}{\frac{{d}^{2} \cdot {c0}^{2}}{{D}^{2} \cdot \left({w}^{2} \cdot h\right)}}
\]
Simplified52.5
\[\leadsto \color{blue}{\left(\frac{d}{D \cdot D} \cdot d\right) \cdot \frac{c0 \cdot c0}{w \cdot \left(w \cdot h\right)}}
\]
Proof
(*.f64 (*.f64 (/.f64 d (*.f64 D D)) d) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (/.f64 d (Rewrite<= unpow2_binary64 (pow.f64 D 2))) d) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/r/_binary64 (/.f64 d (/.f64 (pow.f64 D 2) d))) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 1 points increase in error, 3 points decrease in error
(*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 d d) (pow.f64 D 2))) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 10 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) (pow.f64 D 2)) (/.f64 (*.f64 c0 c0) (*.f64 w (*.f64 w h)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (pow.f64 d 2) (pow.f64 D 2)) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 c0 2)) (*.f64 w (*.f64 w h)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (pow.f64 d 2) (pow.f64 D 2)) (/.f64 (pow.f64 c0 2) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 w w) h)))): 2 points increase in error, 1 points decrease in error
(*.f64 (/.f64 (pow.f64 d 2) (pow.f64 D 2)) (/.f64 (pow.f64 c0 2) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 w 2)) h))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 (pow.f64 d 2) (pow.f64 c0 2)) (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 w 2) h)))): 5 points increase in error, 9 points decrease in error
Applied egg-rr19.6
\[\leadsto \color{blue}{{\left(\frac{d}{D} \cdot \frac{c0}{w \cdot \sqrt{h}}\right)}^{2}}
\]
Initial program 64.0
\[\frac{c0}{2 \cdot w} \cdot \left(\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} + \sqrt{\frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} \cdot \frac{c0 \cdot \left(d \cdot d\right)}{\left(w \cdot h\right) \cdot \left(D \cdot D\right)} - M \cdot M}\right)
\]
Taylor expanded in c0 around -inf 63.5
\[\leadsto \color{blue}{-0.5 \cdot \frac{\left(\frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)} + -1 \cdot \frac{{d}^{2}}{{D}^{2} \cdot \left(w \cdot h\right)}\right) \cdot {c0}^{2}}{w} + 0.25 \cdot \frac{{D}^{2} \cdot \left({M}^{2} \cdot h\right)}{{d}^{2}}}
\]
Simplified28.5
\[\leadsto \color{blue}{\mathsf{fma}\left(0.25, \frac{D}{\frac{d \cdot d}{D}} \cdot \left(\left(h \cdot M\right) \cdot M\right), 0\right)}
\]
Proof
(fma.f64 1/4 (*.f64 (/.f64 D (/.f64 (*.f64 d d) D)) (*.f64 (*.f64 h M) M)) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (*.f64 (/.f64 D (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) D)) (*.f64 (*.f64 h M) M)) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 D D) (pow.f64 d 2))) (*.f64 (*.f64 h M) M)) 0): 28 points increase in error, 2 points decrease in error
(fma.f64 1/4 (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (pow.f64 d 2)) (*.f64 (*.f64 h M) M)) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (*.f64 (/.f64 (pow.f64 D 2) (pow.f64 d 2)) (Rewrite<= associate-*r*_binary64 (*.f64 h (*.f64 M M)))) 0): 16 points increase in error, 3 points decrease in error
(fma.f64 1/4 (*.f64 (/.f64 (pow.f64 D 2) (pow.f64 d 2)) (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 D 2) (/.f64 (pow.f64 d 2) (*.f64 h (pow.f64 M 2))))) 0): 7 points increase in error, 7 points decrease in error
(fma.f64 1/4 (/.f64 (pow.f64 D 2) (/.f64 (pow.f64 d 2) (Rewrite=> *-commutative_binary64 (*.f64 (pow.f64 M 2) h)))) 0): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))) 0): 3 points increase in error, 6 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= div0_binary64 (/.f64 0 (/.f64 w (pow.f64 c0 2))))): 48 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (Rewrite<= metadata-eval (*.f64 -1/2 0)) (/.f64 w (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (*.f64 -1/2 (Rewrite<= mul0-lft_binary64 (*.f64 0 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h)))))) (/.f64 w (pow.f64 c0 2)))): 93 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (*.f64 -1/2 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (/.f64 w (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (/.f64 (*.f64 -1/2 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))))) (/.f64 w (pow.f64 c0 2)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (Rewrite<= associate-*r/_binary64 (*.f64 -1/2 (/.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (/.f64 w (pow.f64 c0 2)))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2)) (*.f64 -1/2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 1 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))) (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1/2 (/.f64 (*.f64 (+.f64 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))) (*.f64 -1 (/.f64 (pow.f64 d 2) (*.f64 (pow.f64 D 2) (*.f64 w h))))) (pow.f64 c0 2)) w)) (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (pow.f64 d 2))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr14.8
\[\leadsto \mathsf{fma}\left(0.25, \color{blue}{0 + h \cdot {\left(M \cdot \frac{D}{d}\right)}^{2}}, 0\right)
\]
Applied egg-rr14.9
\[\leadsto \mathsf{fma}\left(0.25, 0 + h \cdot {\color{blue}{\left(\frac{M \cdot D}{d}\right)}}^{2}, 0\right)
\]