Initial program 62.9
\[\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)
\]
Simplified62.7
\[\leadsto \color{blue}{\frac{c0}{2 \cdot w} \cdot \left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D} + \sqrt{\mathsf{fma}\left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, \frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, -M \cdot M\right)}\right)}
\]
Proof
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (sqrt.f64 (fma.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))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (fma.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))) (neg.f64 (*.f64 M M)))))): 13 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.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))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 4 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.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)))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 7 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.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
Taylor expanded in c0 around -inf 63.3
\[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\left(0.5 \cdot \frac{{D}^{2} \cdot \left(w \cdot \left({M}^{2} \cdot h\right)\right)}{{d}^{2} \cdot c0} + -1 \cdot \left(\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\right)\right)}
\]
Simplified62.2
\[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\mathsf{fma}\left(0.5, \frac{\left(w \cdot \left(h \cdot \left(M \cdot M\right)\right)\right) \cdot \left(D \cdot D\right)}{c0 \cdot \left(d \cdot d\right)}, -c0 \cdot \left(0 \cdot \frac{d \cdot d}{w \cdot \left(D \cdot \left(D \cdot h\right)\right)}\right)\right)}
\]
Proof
(fma.f64 1/2 (/.f64 (*.f64 (*.f64 w (*.f64 h (*.f64 M M))) (*.f64 D D)) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (*.f64 w (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) (*.f64 D D)) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (*.f64 w (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 D D)) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (*.f64 w (*.f64 (pow.f64 M 2) h)))) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 d d) c0))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) c0)) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (*.f64 w (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 D D) h)))))))): 4 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (*.f64 w (Rewrite<= *-commutative_binary64 (*.f64 h (*.f64 D D))))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (*.f64 w h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 w h))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (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))))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (Rewrite<= *-commutative_binary64 (*.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))))) c0)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.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))))) c0)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0))) (*.f64 -1 (*.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))))) c0)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in c0 around 0 39.9
\[\leadsto \color{blue}{0.25 \cdot \frac{{D}^{2} \cdot \left(h \cdot {M}^{2}\right)}{{d}^{2}}}
\]
Simplified32.3
\[\leadsto \color{blue}{\frac{h}{\frac{d}{M}} \cdot \left(\frac{D \cdot D}{\frac{d}{M}} \cdot 0.25\right)}
\]
Proof
(*.f64 (/.f64 h (/.f64 d M)) (*.f64 (/.f64 (*.f64 D D) (/.f64 d M)) 1/4)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 h M) d)) (*.f64 (/.f64 (*.f64 D D) (/.f64 d M)) 1/4)): 16 points increase in error, 11 points decrease in error
(*.f64 (/.f64 (*.f64 h M) d) (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D D) M) d)) 1/4)): 12 points increase in error, 13 points decrease in error
(*.f64 (/.f64 (*.f64 h M) d) (*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 M (*.f64 D D))) d) 1/4)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 (*.f64 h M) d) (/.f64 (*.f64 M (*.f64 D D)) d)) 1/4)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (*.f64 h M) (*.f64 M (*.f64 D D))) (*.f64 d d))) 1/4): 49 points increase in error, 7 points decrease in error
(*.f64 (/.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 (*.f64 h M) M) (*.f64 D D))) (*.f64 d d)) 1/4): 15 points increase in error, 3 points decrease in error
(*.f64 (/.f64 (*.f64 (Rewrite<= associate-*r*_binary64 (*.f64 h (*.f64 M M))) (*.f64 D D)) (*.f64 d d)) 1/4): 15 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (*.f64 h (*.f64 M M)))) (*.f64 d d)) 1/4): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (*.f64 D D) (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) (*.f64 d d)) 1/4): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 h (pow.f64 M 2))) (*.f64 d d)) 1/4): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (Rewrite<= unpow2_binary64 (pow.f64 d 2))) 1/4): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (pow.f64 d 2)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in D around 0 33.1
\[\leadsto \frac{h}{\frac{d}{M}} \cdot \left(\color{blue}{\frac{{D}^{2} \cdot M}{d}} \cdot 0.25\right)
\]
Simplified23.9
\[\leadsto \frac{h}{\frac{d}{M}} \cdot \left(\color{blue}{\left(D \cdot \left(D \cdot \frac{M}{d}\right)\right)} \cdot 0.25\right)
\]
Proof
(*.f64 D (*.f64 D (/.f64 M d))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 D D) (/.f64 M d))): 41 points increase in error, 27 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (*.f64 D D) M) d)): 26 points increase in error, 26 points decrease in error
(/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) M) d): 0 points increase in error, 0 points decrease in error
Applied egg-rr21.9
\[\leadsto \color{blue}{\frac{h}{\frac{\frac{d}{M}}{D \cdot \left(D \cdot \left(\frac{M}{d} \cdot 0.25\right)\right)}}}
\]
Simplified20.0
\[\leadsto \color{blue}{\left(\frac{0.25 \cdot \left(M \cdot \frac{D}{d}\right)}{\frac{d}{D}} \cdot M\right) \cdot h}
\]
Proof
(*.f64 (*.f64 (/.f64 (*.f64 1/4 (*.f64 M (/.f64 D d))) (/.f64 d D)) M) h): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (/.f64 (*.f64 1/4 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 D d) M))) (/.f64 d D)) M) h): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (/.f64 (*.f64 1/4 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 D M) d))) (/.f64 d D)) M) h): 9 points increase in error, 3 points decrease in error
(*.f64 (*.f64 (/.f64 (*.f64 1/4 (Rewrite<= associate-*r/_binary64 (*.f64 D (/.f64 M d)))) (/.f64 d D)) M) h): 7 points increase in error, 12 points decrease in error
(*.f64 (*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D (/.f64 M d)) 1/4)) (/.f64 d D)) M) h): 0 points increase in error, 0 points decrease in error
(*.f64 (*.f64 (/.f64 (Rewrite<= associate-*r*_binary64 (*.f64 D (*.f64 (/.f64 M d) 1/4))) (/.f64 d D)) M) h): 0 points increase in error, 1 points decrease in error
(*.f64 (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D (*.f64 (/.f64 M d) 1/4)) D) d)) M) h): 7 points increase in error, 5 points decrease in error
(*.f64 (*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 D (*.f64 D (*.f64 (/.f64 M d) 1/4)))) d) M) h): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r*_binary64 (*.f64 (/.f64 (*.f64 D (*.f64 D (*.f64 (/.f64 M d) 1/4))) d) (*.f64 M h))): 25 points increase in error, 20 points decrease in error
(*.f64 (/.f64 (*.f64 D (*.f64 D (*.f64 (/.f64 M d) 1/4))) d) (Rewrite<= *-commutative_binary64 (*.f64 h M))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 D (*.f64 D (*.f64 (/.f64 M d) 1/4))) (/.f64 d (*.f64 h M)))): 21 points increase in error, 16 points decrease in error
(/.f64 (Rewrite=> *-commutative_binary64 (*.f64 (*.f64 D (*.f64 (/.f64 M d) 1/4)) D)) (/.f64 d (*.f64 h M))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-/l*_binary64 (/.f64 (*.f64 D (*.f64 (/.f64 M d) 1/4)) (/.f64 (/.f64 d (*.f64 h M)) D))): 10 points increase in error, 21 points decrease in error
(/.f64 (*.f64 D (*.f64 (/.f64 M d) 1/4)) (/.f64 (/.f64 d (Rewrite=> *-commutative_binary64 (*.f64 M h))) D)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 D (*.f64 (/.f64 M d) 1/4)) (/.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 d M) h)) D)): 14 points increase in error, 24 points decrease in error
(/.f64 (*.f64 D (*.f64 (/.f64 M d) 1/4)) (Rewrite<= associate-/r*_binary64 (/.f64 (/.f64 d M) (*.f64 h D)))): 27 points increase in error, 22 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D (*.f64 (/.f64 M d) 1/4)) (*.f64 h D)) (/.f64 d M))): 15 points increase in error, 9 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 h D) (*.f64 D (*.f64 (/.f64 M d) 1/4)))) (/.f64 d M)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> associate-*l*_binary64 (*.f64 h (*.f64 D (*.f64 D (*.f64 (/.f64 M d) 1/4))))) (/.f64 d M)): 15 points increase in error, 26 points decrease in error
(Rewrite=> associate-/l*_binary64 (/.f64 h (/.f64 (/.f64 d M) (*.f64 D (*.f64 D (*.f64 (/.f64 M d) 1/4)))))): 29 points increase in error, 15 points decrease in error
Initial program 57.9
\[\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{c0}{2 \cdot w} \cdot \left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D} + \sqrt{\mathsf{fma}\left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, \frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, -M \cdot M\right)}\right)}
\]
Proof
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (sqrt.f64 (fma.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))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (fma.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))) (neg.f64 (*.f64 M M)))))): 13 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.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))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 4 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.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)))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 7 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.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
Taylor expanded in c0 around -inf 57.4
\[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\left(0.5 \cdot \frac{{D}^{2} \cdot \left(w \cdot \left({M}^{2} \cdot h\right)\right)}{{d}^{2} \cdot c0} + -1 \cdot \left(\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\right)\right)}
\]
Simplified59.3
\[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\mathsf{fma}\left(0.5, \frac{\left(w \cdot \left(h \cdot \left(M \cdot M\right)\right)\right) \cdot \left(D \cdot D\right)}{c0 \cdot \left(d \cdot d\right)}, -c0 \cdot \left(0 \cdot \frac{d \cdot d}{w \cdot \left(D \cdot \left(D \cdot h\right)\right)}\right)\right)}
\]
Proof
(fma.f64 1/2 (/.f64 (*.f64 (*.f64 w (*.f64 h (*.f64 M M))) (*.f64 D D)) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (*.f64 w (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) (*.f64 D D)) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (*.f64 w (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 D D)) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (*.f64 w (*.f64 (pow.f64 M 2) h)))) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 d d) c0))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) c0)) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (*.f64 w (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 D D) h)))))))): 4 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (*.f64 w (Rewrite<= *-commutative_binary64 (*.f64 h (*.f64 D D))))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (*.f64 w h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 w h))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (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))))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (Rewrite<= *-commutative_binary64 (*.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))))) c0)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.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))))) c0)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0))) (*.f64 -1 (*.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))))) c0)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in c0 around 0 31.5
\[\leadsto \color{blue}{0.25 \cdot \frac{{D}^{2} \cdot \left(h \cdot {M}^{2}\right)}{{d}^{2}}}
\]
Simplified18.2
\[\leadsto \color{blue}{\frac{h}{\frac{d}{M}} \cdot \left(\frac{D \cdot D}{\frac{d}{M}} \cdot 0.25\right)}
\]
Proof
(*.f64 (/.f64 h (/.f64 d M)) (*.f64 (/.f64 (*.f64 D D) (/.f64 d M)) 1/4)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 h M) d)) (*.f64 (/.f64 (*.f64 D D) (/.f64 d M)) 1/4)): 16 points increase in error, 11 points decrease in error
(*.f64 (/.f64 (*.f64 h M) d) (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D D) M) d)) 1/4)): 12 points increase in error, 13 points decrease in error
(*.f64 (/.f64 (*.f64 h M) d) (*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 M (*.f64 D D))) d) 1/4)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 (*.f64 h M) d) (/.f64 (*.f64 M (*.f64 D D)) d)) 1/4)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (*.f64 h M) (*.f64 M (*.f64 D D))) (*.f64 d d))) 1/4): 49 points increase in error, 7 points decrease in error
(*.f64 (/.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 (*.f64 h M) M) (*.f64 D D))) (*.f64 d d)) 1/4): 15 points increase in error, 3 points decrease in error
(*.f64 (/.f64 (*.f64 (Rewrite<= associate-*r*_binary64 (*.f64 h (*.f64 M M))) (*.f64 D D)) (*.f64 d d)) 1/4): 15 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (*.f64 h (*.f64 M M)))) (*.f64 d d)) 1/4): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (*.f64 D D) (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) (*.f64 d d)) 1/4): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 h (pow.f64 M 2))) (*.f64 d d)) 1/4): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (Rewrite<= unpow2_binary64 (pow.f64 d 2))) 1/4): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (pow.f64 d 2)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in D around 0 20.6
\[\leadsto \frac{h}{\frac{d}{M}} \cdot \left(\color{blue}{\frac{{D}^{2} \cdot M}{d}} \cdot 0.25\right)
\]
Simplified17.7
\[\leadsto \frac{h}{\frac{d}{M}} \cdot \left(\color{blue}{\left(D \cdot \left(D \cdot \frac{M}{d}\right)\right)} \cdot 0.25\right)
\]
Proof
(*.f64 D (*.f64 D (/.f64 M d))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 D D) (/.f64 M d))): 41 points increase in error, 27 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (*.f64 D D) M) d)): 26 points increase in error, 26 points decrease in error
(/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) M) d): 0 points increase in error, 0 points decrease in error
Applied egg-rr20.6
\[\leadsto \color{blue}{\frac{\frac{\left(h \cdot D\right) \cdot \left(D \cdot \left(\frac{M}{d} \cdot 0.25\right)\right)}{d}}{\frac{1}{M}}}
\]
Initial program 55.4
\[\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)
\]
Simplified55.1
\[\leadsto \color{blue}{\frac{c0}{2 \cdot w} \cdot \left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D} + \sqrt{\mathsf{fma}\left(\frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, \frac{c0}{w \cdot h} \cdot \frac{d \cdot d}{D \cdot D}, -M \cdot M\right)}\right)}
\]
Proof
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (*.f64 (/.f64 c0 (*.f64 w h)) (/.f64 (*.f64 d d) (*.f64 D D))) (sqrt.f64 (fma.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))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))) (sqrt.f64 (fma.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))) (neg.f64 (*.f64 M M)))))): 13 points increase in error, 1 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.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))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 4 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (fma.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)))) (neg.f64 (*.f64 M M)))))): 0 points increase in error, 7 points decrease in error
(*.f64 (/.f64 c0 (*.f64 2 w)) (+.f64 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) (sqrt.f64 (Rewrite<= fma-neg_binary64 (-.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
Taylor expanded in c0 around -inf 55.4
\[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\left(0.5 \cdot \frac{{D}^{2} \cdot \left(w \cdot \left({M}^{2} \cdot h\right)\right)}{{d}^{2} \cdot c0} + -1 \cdot \left(\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\right)\right)}
\]
Simplified55.7
\[\leadsto \frac{c0}{2 \cdot w} \cdot \color{blue}{\mathsf{fma}\left(0.5, \frac{\left(w \cdot \left(h \cdot \left(M \cdot M\right)\right)\right) \cdot \left(D \cdot D\right)}{c0 \cdot \left(d \cdot d\right)}, -c0 \cdot \left(0 \cdot \frac{d \cdot d}{w \cdot \left(D \cdot \left(D \cdot h\right)\right)}\right)\right)}
\]
Proof
(fma.f64 1/2 (/.f64 (*.f64 (*.f64 w (*.f64 h (*.f64 M M))) (*.f64 D D)) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (*.f64 w (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) (*.f64 D D)) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (*.f64 w (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 D D)) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (*.f64 w (*.f64 (pow.f64 M 2) h)))) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 c0 (*.f64 d d))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 d d) c0))) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) c0)) (neg.f64 (*.f64 c0 (*.f64 0 (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (/.f64 (*.f64 d d) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) (*.f64 w (*.f64 D (*.f64 D h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (*.f64 w (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 D D) h)))))))): 4 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (*.f64 w (Rewrite<= *-commutative_binary64 (*.f64 h (*.f64 D D))))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 w h) (*.f64 D D)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (*.f64 w h)))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (*.f64 (+.f64 -1 1) (/.f64 (pow.f64 d 2) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 w h))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (*.f64 c0 (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))))))))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (neg.f64 (Rewrite<= *-commutative_binary64 (*.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))))) c0)))): 0 points increase in error, 0 points decrease in error
(fma.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.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))))) c0)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/2 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 w (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) c0))) (*.f64 -1 (*.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))))) c0)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in c0 around 0 30.6
\[\leadsto \color{blue}{0.25 \cdot \frac{{D}^{2} \cdot \left(h \cdot {M}^{2}\right)}{{d}^{2}}}
\]
Simplified17.8
\[\leadsto \color{blue}{\frac{h}{\frac{d}{M}} \cdot \left(\frac{D \cdot D}{\frac{d}{M}} \cdot 0.25\right)}
\]
Proof
(*.f64 (/.f64 h (/.f64 d M)) (*.f64 (/.f64 (*.f64 D D) (/.f64 d M)) 1/4)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 h M) d)) (*.f64 (/.f64 (*.f64 D D) (/.f64 d M)) 1/4)): 16 points increase in error, 11 points decrease in error
(*.f64 (/.f64 (*.f64 h M) d) (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (*.f64 D D) M) d)) 1/4)): 12 points increase in error, 13 points decrease in error
(*.f64 (/.f64 (*.f64 h M) d) (*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 M (*.f64 D D))) d) 1/4)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 (*.f64 h M) d) (/.f64 (*.f64 M (*.f64 D D)) d)) 1/4)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (*.f64 h M) (*.f64 M (*.f64 D D))) (*.f64 d d))) 1/4): 49 points increase in error, 7 points decrease in error
(*.f64 (/.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 (*.f64 h M) M) (*.f64 D D))) (*.f64 d d)) 1/4): 15 points increase in error, 3 points decrease in error
(*.f64 (/.f64 (*.f64 (Rewrite<= associate-*r*_binary64 (*.f64 h (*.f64 M M))) (*.f64 D D)) (*.f64 d d)) 1/4): 15 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (*.f64 D D) (*.f64 h (*.f64 M M)))) (*.f64 d d)) 1/4): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (*.f64 D D) (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) (*.f64 d d)) 1/4): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 h (pow.f64 M 2))) (*.f64 d d)) 1/4): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (Rewrite<= unpow2_binary64 (pow.f64 d 2))) 1/4): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 1/4 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (pow.f64 d 2)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in D around 0 19.4
\[\leadsto \frac{h}{\frac{d}{M}} \cdot \left(\color{blue}{\frac{{D}^{2} \cdot M}{d}} \cdot 0.25\right)
\]
Simplified17.8
\[\leadsto \frac{h}{\frac{d}{M}} \cdot \left(\color{blue}{\left(D \cdot \left(D \cdot \frac{M}{d}\right)\right)} \cdot 0.25\right)
\]
Proof
(*.f64 D (*.f64 D (/.f64 M d))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 D D) (/.f64 M d))): 41 points increase in error, 27 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (*.f64 D D) M) d)): 26 points increase in error, 26 points decrease in error
(/.f64 (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) M) d): 0 points increase in error, 0 points decrease in error