Henrywood and Agarwal, Equation (9a)

Average Accuracy: 77.6% → 86.4%

Time: 16.6s

Precision: binary64

Cost: 7872

\[ \begin{array}{c}[M, D] = \mathsf{sort}([M, D])\\ \end{array} \]

Math

\[\mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]

↓

\[\mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \mathsf{*.f64}\left(\ell, \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{/.f64}\left(2, D\right)\right)\right)\right)\right)\right)\right) \]

FPCore

(FPCore (w0 M D h l d)
 :precision binary64
 (*.f64
  w0
  (sqrt.f64
   (-.f64 1 (*.f64 (pow.f64 (/.f64 (*.f64 M D) (*.f64 2 d)) 2) (/.f64 h l))))))

↓

(FPCore (w0 M D h l d)
 :precision binary64
 (*.f64
  w0
  (sqrt.f64
   (-.f64
    1
    (/.f64
     (*.f64 (*.f64 (/.f64 M d) (*.f64 1/2 D)) h)
     (*.f64 l (*.f64 (/.f64 d M) (/.f64 2 D))))))))

Derivation

1. Initial program 77.6%

   \[\mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]

2. Applied egg-rr 78.4%

   \[\leadsto \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \color{blue}{\mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\frac{1}{2}, d\right)\right)\right), 2\right), \mathsf{/.f64}\left(\ell, h\right)\right)}\right)\right)\right) \]
   Proof

   [Start] 77.6	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
   clear-num [=>] 77.6	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right), \color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(\ell, h\right)\right)}\right)\right)\right)\right) \]
   un-div-inv [=>] 78.5	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \color{blue}{\mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right), \mathsf{/.f64}\left(\ell, h\right)\right)}\right)\right)\right) \]
   div-inv [=>] 78.5	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{/.f64}\left(1, \mathsf{*.f64}\left(2, d\right)\right)\right)}, 2\right), \mathsf{/.f64}\left(\ell, h\right)\right)\right)\right)\right) \]
   associate-*l* [=>] 78.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\color{blue}{\mathsf{*.f64}\left(M, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(1, \mathsf{*.f64}\left(2, d\right)\right)\right)\right)}, 2\right), \mathsf{/.f64}\left(\ell, h\right)\right)\right)\right)\right) \]
   associate-/r* [=>] 78.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{*.f64}\left(D, \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, 2\right), d\right)}\right)\right), 2\right), \mathsf{/.f64}\left(\ell, h\right)\right)\right)\right)\right) \]
   metadata-eval [=>] 78.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\color{blue}{\frac{1}{2}}, d\right)\right)\right), 2\right), \mathsf{/.f64}\left(\ell, h\right)\right)\right)\right)\right) \]

3. Simplified 82.9%

   \[\leadsto \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right), 2\right), \ell\right)\right)}\right)\right)\right) \]
   Proof

   [Start] 78.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\frac{1}{2}, d\right)\right)\right), 2\right), \mathsf{/.f64}\left(\ell, h\right)\right)\right)\right)\right) \]
   associate-/r/ [=>] 83.1	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\frac{1}{2}, d\right)\right)\right), 2\right), \ell\right), h\right)}\right)\right)\right) \]
   *-commutative [=>] 83.1	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\frac{1}{2}, d\right)\right)\right), 2\right), \ell\right)\right)}\right)\right)\right) \]
   *-commutative [=>] 83.1	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\frac{1}{2}, d\right)\right), M\right)}, 2\right), \ell\right)\right)\right)\right)\right) \]
   associate-*r* [<=] 82.9	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\color{blue}{\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\frac{1}{2}, d\right), M\right)\right)}, 2\right), \ell\right)\right)\right)\right)\right) \]
   *-commutative [<=] 82.9	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(D, \color{blue}{\mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\frac{1}{2}, d\right)\right)}\right), 2\right), \ell\right)\right)\right)\right)\right) \]
   associate-*r/ [=>] 82.9	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(D, \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, \frac{1}{2}\right), d\right)}\right), 2\right), \ell\right)\right)\right)\right)\right) \]
   associate-/l* [=>] 82.9	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(D, \color{blue}{\mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)}\right), 2\right), \ell\right)\right)\right)\right)\right) \]

4. Applied egg-rr 85.4%

   \[\leadsto \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), \ell\right)\right)}\right)\right)\right)\right) \]
   Proof

   [Start] 82.9	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right), 2\right), \ell\right)\right)\right)\right)\right) \]
   unpow2 [=>] 82.9	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right), \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right)\right)}, \ell\right)\right)\right)\right)\right) \]
   *-un-lft-identity [=>] 82.9	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right), \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(1, \ell\right)}\right)\right)\right)\right)\right) \]
   times-frac [=>] 85.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right), 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right), \ell\right)\right)}\right)\right)\right)\right) \]
   *-commutative [=>] 85.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right), D\right)}, 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right), \ell\right)\right)\right)\right)\right)\right) \]
   associate-/r/ [=>] 85.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \frac{1}{2}\right)}, D\right), 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right), \ell\right)\right)\right)\right)\right)\right) \]
   associate-*l* [=>] 85.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)}, 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right)\right), \ell\right)\right)\right)\right)\right)\right) \]
   *-commutative [=>] 85.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), 1\right), \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, \mathsf{/.f64}\left(d, \frac{1}{2}\right)\right), D\right)}, \ell\right)\right)\right)\right)\right)\right) \]
   associate-/r/ [=>] 85.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \frac{1}{2}\right)}, D\right), \ell\right)\right)\right)\right)\right)\right) \]
   associate-*l* [=>] 85.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), 1\right), \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)}, \ell\right)\right)\right)\right)\right)\right) \]

5. Applied egg-rr 86.4%

   \[\leadsto \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \mathsf{*.f64}\left(\ell, \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{/.f64}\left(2, D\right)\right)\right)\right)}\right)\right)\right) \]
   Proof

   [Start] 85.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), 1\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), \ell\right)\right)\right)\right)\right)\right) \]
   /-rgt-identity [=>] 85.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), \ell\right)\right)\right)\right)\right)\right) \]
   associate-*r* [=>] 86.3	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), \ell\right)\right)}\right)\right)\right) \]
   clear-num [=>] 86.3	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(\ell, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right)\right)}\right)\right)\right)\right) \]
   un-div-inv [=>] 86.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(h, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right), \mathsf{/.f64}\left(\ell, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right)\right)}\right)\right)\right) \]
   *-commutative [=>] 86.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right)}, \mathsf{/.f64}\left(\ell, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right)\right)\right)\right)\right) \]
   div-inv [=>] 86.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \color{blue}{\mathsf{*.f64}\left(\ell, \mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right)\right)}\right)\right)\right)\right) \]
   /-rgt-identity [<=] 86.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \mathsf{*.f64}\left(\ell, \mathsf{/.f64}\left(1, \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), 1\right)}\right)\right)\right)\right)\right)\right) \]
   associate-/l* [=>] 86.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \mathsf{*.f64}\left(\ell, \mathsf{/.f64}\left(1, \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right)}\right)\right)\right)\right)\right)\right) \]
   associate-/r/ [=>] 86.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \mathsf{*.f64}\left(\ell, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(M, d\right)\right), \mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right)}\right)\right)\right)\right)\right) \]
   clear-num [<=] 86.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \mathsf{*.f64}\left(\ell, \mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(d, M\right)}, \mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right)\right)\right)\right)\right)\right)\right) \]
   associate-/r* [=>] 86.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \mathsf{*.f64}\left(\ell, \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \frac{1}{2}\right), D\right)}\right)\right)\right)\right)\right)\right) \]
   metadata-eval [=>] 86.4	\[ \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \mathsf{*.f64}\left(\ell, \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{/.f64}\left(\color{blue}{2}, D\right)\right)\right)\right)\right)\right)\right) \]

6. Final simplification 86.4%

   \[\leadsto \mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(\frac{1}{2}, D\right)\right), h\right), \mathsf{*.f64}\left(\ell, \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{/.f64}\left(2, D\right)\right)\right)\right)\right)\right)\right) \]

Alternatives

Alternative 1
Accuracy	80.9%
Cost	8264

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(h, \ell\right), -19999999999999999781741223642818392253569612520802717890360030929450604798220516297708225612915260122593317856641907797168065523046908674225209344\right):\\ \;\;\;\;w0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(h, \ell\right), \frac{-3499601159652819}{17498005798264095394980017816940970922825355447145699491406164851279623993595007385788105416184430592}\right):\\ \;\;\;\;\mathsf{*.f64}\left(w0, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{-1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(M, \mathsf{/.f64}\left(h, \ell\right)\right), \mathsf{/.f64}\left(D, d\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;w0\\ \end{array} \]

Alternative 2
Accuracy	78.3%
Cost	64

\[w0 \]

Reproduce

herbie shell --seed 2023144 
(FPCore (w0 M D h l d)
  :name "Henrywood and Agarwal, Equation (9a)"
  :precision binary64
  (* w0 (sqrt (- 1.0 (* (pow (/ (* M D) (* 2.0 d)) 2.0) (/ h l))))))