Initial program 21.0
\[\left({\left(\frac{d}{h}\right)}^{\left(\frac{1}{2}\right)} \cdot {\left(\frac{d}{\ell}\right)}^{\left(\frac{1}{2}\right)}\right) \cdot \left(1 - \left(\frac{1}{2} \cdot {\left(\frac{M \cdot D}{2 \cdot d}\right)}^{2}\right) \cdot \frac{h}{\ell}\right)
\]
Simplified21.5
\[\leadsto \color{blue}{\sqrt{\frac{d}{h}} \cdot \left(\sqrt{\frac{d}{\ell}} \cdot \mathsf{fma}\left({\left(\frac{\frac{D}{d}}{\frac{2}{M}}\right)}^{2}, \frac{h}{\ell} \cdot -0.5, 1\right)\right)}
\]
Proof
(*.f64 (sqrt.f64 (/.f64 d h)) (*.f64 (sqrt.f64 (/.f64 d l)) (fma.f64 (pow.f64 (/.f64 (/.f64 D d) (/.f64 2 M)) 2) (*.f64 (/.f64 h l) -1/2) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= unpow1/2_binary64 (pow.f64 (/.f64 d h) 1/2)) (*.f64 (sqrt.f64 (/.f64 d l)) (fma.f64 (pow.f64 (/.f64 (/.f64 D d) (/.f64 2 M)) 2) (*.f64 (/.f64 h l) -1/2) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (Rewrite<= metadata-eval (/.f64 1 2))) (*.f64 (sqrt.f64 (/.f64 d l)) (fma.f64 (pow.f64 (/.f64 (/.f64 D d) (/.f64 2 M)) 2) (*.f64 (/.f64 h l) -1/2) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (Rewrite<= unpow1/2_binary64 (pow.f64 (/.f64 d l) 1/2)) (fma.f64 (pow.f64 (/.f64 (/.f64 D d) (/.f64 2 M)) 2) (*.f64 (/.f64 h l) -1/2) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (Rewrite<= metadata-eval (/.f64 1 2))) (fma.f64 (pow.f64 (/.f64 (/.f64 D d) (/.f64 2 M)) 2) (*.f64 (/.f64 h l) -1/2) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (fma.f64 (pow.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (/.f64 D d) M) 2)) 2) (*.f64 (/.f64 h l) -1/2) 1))): 2 points increase in error, 4 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (fma.f64 (pow.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 M (/.f64 D d))) 2) 2) (*.f64 (/.f64 h l) -1/2) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (fma.f64 (pow.f64 (/.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 M D) d)) 2) 2) (*.f64 (/.f64 h l) -1/2) 1))): 6 points increase in error, 3 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (fma.f64 (pow.f64 (Rewrite=> associate-/l/_binary64 (/.f64 (*.f64 M D) (*.f64 2 d))) 2) (*.f64 (/.f64 h l) -1/2) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (fma.f64 (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2) (*.f64 (/.f64 h l) (Rewrite<= metadata-eval (neg.f64 1/2))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (fma.f64 (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2) (*.f64 (/.f64 h l) (neg.f64 (Rewrite<= metadata-eval (/.f64 1 2)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (fma.f64 (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2) (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (/.f64 h l) (/.f64 1 2)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (fma.f64 (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2) (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 1 2) (/.f64 h l)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2) (neg.f64 (*.f64 (/.f64 1 2) (/.f64 h l)))) 1)))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2) (*.f64 (/.f64 1 2) (/.f64 h l))))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (+.f64 (neg.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2) (/.f64 1 2)) (/.f64 h l)))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (+.f64 (neg.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 1 2) (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2))) (/.f64 h l))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (+.f64 (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 (*.f64 (/.f64 1 2) (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2))) (/.f64 h l))) 1))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 (neg.f64 (*.f64 (/.f64 1 2) (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2))) (/.f64 h l)))))): 0 points increase in error, 0 points decrease in error
(*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (*.f64 (pow.f64 (/.f64 d l) (/.f64 1 2)) (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 1 (*.f64 (*.f64 (/.f64 1 2) (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2)) (/.f64 h l)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (pow.f64 (/.f64 d h) (/.f64 1 2)) (pow.f64 (/.f64 d l) (/.f64 1 2))) (-.f64 1 (*.f64 (*.f64 (/.f64 1 2) (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2)) (/.f64 h l))))): 4 points increase in error, 6 points decrease in error
Taylor expanded in D around 0 35.5
\[\leadsto \sqrt{\frac{d}{h}} \cdot \left(\sqrt{\frac{d}{\ell}} \cdot \color{blue}{\left(1 + -0.125 \cdot \frac{{D}^{2} \cdot \left(h \cdot {M}^{2}\right)}{{d}^{2} \cdot \ell}\right)}\right)
\]
Simplified22.0
\[\leadsto \sqrt{\frac{d}{h}} \cdot \left(\sqrt{\frac{d}{\ell}} \cdot \color{blue}{\mathsf{fma}\left(-0.125, h \cdot \left(\frac{D}{\frac{\ell}{M} \cdot \frac{d \cdot d}{D}} \cdot M\right), 1\right)}\right)
\]
Proof
(fma.f64 -1/8 (*.f64 h (*.f64 (/.f64 D (*.f64 (/.f64 l M) (/.f64 (*.f64 d d) D))) M)) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (*.f64 h (*.f64 (/.f64 D (*.f64 (/.f64 l M) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 d 2)) D))) M)) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (*.f64 h (*.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 D (/.f64 (pow.f64 d 2) D)) (/.f64 l M))) M)) 1): 9 points increase in error, 5 points decrease in error
(fma.f64 -1/8 (*.f64 h (*.f64 (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 D D) (pow.f64 d 2))) (/.f64 l M)) M)) 1): 20 points increase in error, 1 points decrease in error
(fma.f64 -1/8 (*.f64 h (*.f64 (/.f64 (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 D 2)) (pow.f64 d 2)) (/.f64 l M)) M)) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (*.f64 h (*.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (/.f64 (pow.f64 D 2) (pow.f64 d 2)) l) M)) M)) 1): 2 points increase in error, 6 points decrease in error
(fma.f64 -1/8 (*.f64 h (*.f64 (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (pow.f64 D 2) (*.f64 (pow.f64 d 2) l))) M) M)) 1): 12 points increase in error, 2 points decrease in error
(fma.f64 -1/8 (*.f64 h (*.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 D 2) (/.f64 (*.f64 (pow.f64 d 2) l) M))) M)) 1): 7 points increase in error, 5 points decrease in error
(fma.f64 -1/8 (*.f64 h (Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 D 2) (/.f64 (/.f64 (*.f64 (pow.f64 d 2) l) M) M)))) 1): 10 points increase in error, 2 points decrease in error
(fma.f64 -1/8 (*.f64 h (/.f64 (pow.f64 D 2) (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 (pow.f64 d 2) l) (*.f64 M M))))) 1): 12 points increase in error, 2 points decrease in error
(fma.f64 -1/8 (*.f64 h (/.f64 (pow.f64 D 2) (/.f64 (*.f64 (pow.f64 d 2) l) (Rewrite<= unpow2_binary64 (pow.f64 M 2))))) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (pow.f64 D 2) (/.f64 (*.f64 (pow.f64 d 2) l) (pow.f64 M 2))) h)) 1): 0 points increase in error, 0 points decrease in error
(fma.f64 -1/8 (Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 D 2) (/.f64 (/.f64 (*.f64 (pow.f64 d 2) l) (pow.f64 M 2)) h))) 1): 7 points increase in error, 2 points decrease in error
(fma.f64 -1/8 (/.f64 (pow.f64 D 2) (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 (pow.f64 d 2) l) (*.f64 (pow.f64 M 2) h)))) 1): 8 points increase in error, 5 points decrease in error
(fma.f64 -1/8 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (*.f64 (pow.f64 d 2) l))) 1): 5 points increase in error, 11 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (*.f64 (pow.f64 d 2) l))) 1)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1/8 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h))) (*.f64 (pow.f64 d 2) l))) 1): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 -1/8 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h))) (Rewrite<= *-commutative_binary64 (*.f64 l (pow.f64 d 2)))) 1): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1/8 (/.f64 (*.f64 (pow.f64 D 2) (*.f64 (pow.f64 M 2) h)) (*.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 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) (*.f64 h (pow.f64 M 2))) (Rewrite=> *-commutative_binary64 (*.f64 (pow.f64 d 2) l)))) 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 h (pow.f64 M 2))) (*.f64 (pow.f64 d 2) l))))): 0 points increase in error, 0 points decrease in error
Applied egg-rr12.6
\[\leadsto \color{blue}{\frac{\sqrt{-d}}{\sqrt{-h}}} \cdot \left(\sqrt{\frac{d}{\ell}} \cdot \mathsf{fma}\left(-0.125, h \cdot \left(\frac{D}{\frac{\ell}{M} \cdot \frac{d \cdot d}{D}} \cdot M\right), 1\right)\right)
\]
Applied egg-rr8.0
\[\leadsto \frac{\sqrt{-d}}{\sqrt{-h}} \cdot \left(\color{blue}{\frac{\sqrt{-d}}{\sqrt{-\ell}}} \cdot \mathsf{fma}\left(-0.125, h \cdot \left(\frac{D}{\frac{\ell}{M} \cdot \frac{d \cdot d}{D}} \cdot M\right), 1\right)\right)
\]