Simplified60.5
\[\leadsto w0 \cdot \color{blue}{\mathsf{fma}\left(\left(\frac{D}{d} \cdot \frac{D}{d}\right) \cdot \left(\frac{h}{\ell} \cdot \left(M \cdot M\right)\right), -0.125, 1\right)}
\]
Proof
(fma.f64 (*.f64 (*.f64 (/.f64 D d) (/.f64 D d)) (*.f64 (/.f64 h l) (*.f64 M M))) -1/8 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 D D) (*.f64 d d))) (*.f64 (/.f64 h l) (*.f64 M M))) -1/8 1): 38 points increase in error, 1 points decrease in error
(fma.f64 (*.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 d d)) (*.f64 (/.f64 h l) (*.f64 M M))) -1/8 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (/.f64 (pow.f64 D 2) (Rewrite<= unpow2_binary64 (pow.f64 d 2))) (*.f64 (/.f64 h l) (*.f64 M M))) -1/8 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (/.f64 (pow.f64 D 2) (pow.f64 d 2)) (*.f64 (/.f64 h l) (Rewrite<= unpow2_binary64 (pow.f64 M 2)))) -1/8 1): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (/.f64 (pow.f64 D 2) (pow.f64 d 2)) (Rewrite<= associate-/r/_binary64 (/.f64 h (/.f64 l (pow.f64 M 2))))) -1/8 1): 2 points increase in error, 12 points decrease in error
(fma.f64 (*.f64 (/.f64 (pow.f64 D 2) (pow.f64 d 2)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 h (pow.f64 M 2)) l))) -1/8 1): 5 points increase in error, 2 points decrease in error
(fma.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 (pow.f64 d 2) l))) -1/8 1): 10 points increase in error, 9 points decrease in error
(fma.f64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (Rewrite<= *-commutative_binary64 (*.f64 l (pow.f64 d 2)))) -1/8 1): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 l (pow.f64 d 2))) -1/8) 1)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 l (pow.f64 d 2))))) 1): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (Rewrite=> *-commutative_binary64 (*.f64 (pow.f64 M 2) h))) (*.f64 l (pow.f64 d 2)))) 1): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (*.f64 l (pow.f64 d 2)))))): 0 points increase in error, 0 points decrease in error
Simplified30.5
\[\leadsto \color{blue}{\mathsf{fma}\left(\left(h \cdot \left(M \cdot M\right)\right) \cdot \left(\frac{D}{d} \cdot \frac{D}{\ell \cdot d}\right), -0.125 \cdot w0, w0\right)}
\]
Proof
(fma.f64 (*.f64 (*.f64 h (*.f64 M M)) (*.f64 (/.f64 D d) (/.f64 D (*.f64 l d)))) (*.f64 -1/8 w0) w0): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (*.f64 h (Rewrite<= unpow2_binary64 (pow.f64 M 2))) (*.f64 (/.f64 D d) (/.f64 D (*.f64 l d)))) (*.f64 -1/8 w0) w0): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (*.f64 h (pow.f64 M 2)) (*.f64 (/.f64 D d) (/.f64 D (Rewrite<= *-commutative_binary64 (*.f64 d l))))) (*.f64 -1/8 w0) w0): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (*.f64 h (pow.f64 M 2)) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 D D) (*.f64 d (*.f64 d l))))) (*.f64 -1/8 w0) w0): 29 points increase in error, 1 points decrease in error
(fma.f64 (*.f64 (*.f64 h (pow.f64 M 2)) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (*.f64 d (*.f64 d l)))) (*.f64 -1/8 w0) w0): 0 points increase in error, 0 points decrease in error
(fma.f64 (*.f64 (*.f64 h (pow.f64 M 2)) (/.f64 (pow.f64 D 2) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 d d) l)))) (*.f64 -1/8 w0) w0): 8 points increase in error, 1 points decrease in error
(fma.f64 (*.f64 (*.f64 h (pow.f64 M 2)) (/.f64 (pow.f64 D 2) (*.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) l))) (*.f64 -1/8 w0) w0): 0 points increase in error, 0 points decrease in error
(fma.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 D 2) (*.f64 (pow.f64 d 2) l)) (*.f64 h (pow.f64 M 2)))) (*.f64 -1/8 w0) w0): 0 points increase in error, 0 points decrease in error
(fma.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 (pow.f64 d 2) l))) (*.f64 -1/8 w0) w0): 5 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 (pow.f64 d 2) l)) (*.f64 -1/8 w0)) w0)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 (pow.f64 d 2) l)) -1/8) w0)) w0): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 (pow.f64 d 2) l)))) w0) w0): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1/8 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2)))) (*.f64 (pow.f64 d 2) l))) w0) w0): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (/.f64 (*.f64 -1/8 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2)))) (Rewrite=> *-commutative_binary64 (*.f64 l (pow.f64 d 2)))) w0) w0): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 l (pow.f64 d 2))))) w0) w0): 0 points increase in error, 0 points decrease in error
(Rewrite=> distribute-lft1-in_binary64 (*.f64 (+.f64 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 l (pow.f64 d 2)))) 1) w0)): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1/8 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2)))) (*.f64 l (pow.f64 d 2)))) 1) w0): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 (/.f64 (*.f64 -1/8 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2)))) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 d 2) l))) 1) w0): 0 points increase in error, 0 points decrease in error
(*.f64 (+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 (pow.f64 d 2) l)))) 1) w0): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 h (pow.f64 M 2))) (*.f64 (pow.f64 d 2) l))))) w0): 0 points increase in error, 0 points decrease in error