Henrywood and Agarwal, Equation (12)

Average Accuracy: 58.2% → 69.5%

Time: 1.2min

Precision: binary64

Cost: 33668

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

Math

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

↓

\[\begin{array}{l} t_0 := \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right)\\ t_1 := \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right)\\ t_2 := \mathsf{/.f64}\left(t_1, \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(h, -10999999999999999171953497884844250523529691012412235626036558041901464462448164171098019924470539502084351596882522486672778602423884998913414301791154048434817917175130382501194005217280\right):\\ \;\;\;\;\mathsf{*.f64}\left(t_0, \mathsf{*.f64}\left(t_2, \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\mathsf{/.f64}\left(D, d\right), 2\right)\right), 2\right), \mathsf{/.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(\ell, h\right)\right), 1\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-6931674235302037}{86645927941275464361825443254471365732388658605494267974077486894206915868925800719999200190754361815543475342543861619655442432}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right)\right), \ell\right), -1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-8688048222344579}{129672361527531029953512745740348785969138944757576153124864291552832900356653379574990845279596993571506183956603149661949848471106617978371464838566061365220661931356297172615168}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t_0, \mathsf{*.f64}\left(t_2, \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{/.f64}\left(M, 2\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-3119885634089587}{70906491683854249133971333415503528601229677279443476631916611638829262598057001759775558209235971002092300595769547131083230268742795262708226708464736682213924924871800416657575912944521796077262840069882938251784694133132833485038618990914757637167551284096438594475925700608}\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-20240225330731}{101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t_1, \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(h\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(h, D\right)\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

FPCore

(FPCore (d h l M D)
 :precision 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)))))

↓

(FPCore (d h l M D)
 :precision binary64
 (let* ((t_0 (sqrt.f64 (/.f64 d h)))
        (t_1 (sqrt.f64 (neg.f64 d)))
        (t_2 (/.f64 t_1 (sqrt.f64 (neg.f64 l)))))
   (if (<=.f64
        h
        -10999999999999999171953497884844250523529691012412235626036558041901464462448164171098019924470539502084351596882522486672778602423884998913414301791154048434817917175130382501194005217280)
     (*.f64
      t_0
      (*.f64
       t_2
       (fma.f64
        (pow.f64 (*.f64 M (/.f64 (/.f64 D d) 2)) 2)
        (/.f64 -1/2 (/.f64 l h))
        1)))
     (if (<=.f64
          h
          -6931674235302037/86645927941275464361825443254471365732388658605494267974077486894206915868925800719999200190754361815543475342543861619655442432)
       (*.f64
        (*.f64 d (sqrt.f64 (/.f64 1 (*.f64 h l))))
        (+.f64
         (/.f64
          (*.f64 (*.f64 h 1/2) (pow.f64 (*.f64 1/2 (/.f64 (*.f64 M D) d)) 2))
          l)
         -1))
       (if (<=.f64
            h
            -8688048222344579/129672361527531029953512745740348785969138944757576153124864291552832900356653379574990845279596993571506183956603149661949848471106617978371464838566061365220661931356297172615168)
         (*.f64
          t_0
          (*.f64
           t_2
           (-.f64
            1
            (*.f64
             1/2
             (*.f64
              (pow.f64 (*.f64 (/.f64 D d) (/.f64 M 2)) 2)
              (/.f64 h l))))))
         (if (<=.f64
              h
              -3119885634089587/70906491683854249133971333415503528601229677279443476631916611638829262598057001759775558209235971002092300595769547131083230268742795262708226708464736682213924924871800416657575912944521796077262840069882938251784694133132833485038618990914757637167551284096438594475925700608)
           (*.f64 d (neg.f64 (sqrt.f64 (/.f64 (/.f64 1 l) h))))
           (if (<=.f64
                h
                -20240225330731/101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392)
             (*.f64
              (*.f64 (/.f64 t_1 (sqrt.f64 (neg.f64 h))) (sqrt.f64 (/.f64 d l)))
              (-.f64
               1
               (*.f64
                1/8
                (*.f64
                 (/.f64 (*.f64 M M) d)
                 (/.f64 (*.f64 D (*.f64 h D)) (*.f64 d l))))))
             (*.f64
              (+.f64
               1
               (*.f64
                (pow.f64 (*.f64 (/.f64 D d) (*.f64 M 1/2)) 2)
                (*.f64 -1/2 (/.f64 h l))))
              (/.f64 d (*.f64 (sqrt.f64 h) (sqrt.f64 l)))))))))))

Derivation

1. Split input into 6 regimes

2. if h < -1.0999999999999999e187

   1. Initial program 47.1%

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

   2. Simplified 47.4%

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

      [Start] 47.1	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      associate-*l* [=>] 46.9	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)} \]
      metadata-eval [=>] 46.9	\[ \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \color{blue}{\frac{1}{2}}\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      unpow1/2 [=>] 46.9	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right)}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 46.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \color{blue}{\frac{1}{2}}\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      unpow1/2 [=>] 46.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)}, \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      sub-neg [=>] 46.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \color{blue}{\mathsf{+.f64}\left(1, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)}\right)\right) \]
      +-commutative [=>] 46.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right), 1\right)}\right)\right) \]
      *-commutative [=>] 46.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\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(1, 2\right)\right)}, \mathsf{/.f64}\left(h, \ell\right)\right)\right), 1\right)\right)\right) \]
      associate-*l* [=>] 46.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{+.f64}\left(\mathsf{neg.f64}\left(\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(\mathsf{/.f64}\left(1, 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)}\right), 1\right)\right)\right) \]
      distribute-rgt-neg-in [=>] 46.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{+.f64}\left(\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{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)}, 1\right)\right)\right) \]
      *-commutative [<=] 46.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{+.f64}\left(\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{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(h, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)}\right)\right), 1\right)\right)\right) \]

   3. Applied egg-rr 48.3%

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

      [Start] 47.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\mathsf{/.f64}\left(D, d\right), 2\right)\right), 2\right), \mathsf{/.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(\ell, h\right)\right), 1\right)\right)\right) \]
      frac-2neg [=>] 47.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(d\right), \mathsf{neg.f64}\left(\ell\right)\right)}\right), \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\mathsf{/.f64}\left(D, d\right), 2\right)\right), 2\right), \mathsf{/.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(\ell, h\right)\right), 1\right)\right)\right) \]
      sqrt-div [=>] 48.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right), \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right)\right)}, \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\mathsf{/.f64}\left(D, d\right), 2\right)\right), 2\right), \mathsf{/.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(\ell, h\right)\right), 1\right)\right)\right) \]

   if -1.0999999999999999e187 < h < -7.99999999999999983e-113

   1. Initial program 66.1%

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

   2. Applied egg-rr 51.5%

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

      [Start] 66.1

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

      pow1 [=>] 66.1

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

   3. Taylor expanded in d around -inf 71.4%

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

   4. Simplified 71.4%

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

      [Start] 71.4	\[ \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\ell, h\right)\right)\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, h\right)\right), \ell\right)\right)\right), 1\right) \]
      mul-1-neg [=>] 71.4	\[ \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\ell, h\right)\right)\right)\right)\right)}, \mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, h\right)\right), \ell\right)\right)\right), 1\right) \]
      *-commutative [<=] 71.4	\[ \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\ell, h\right)\right)\right), d\right)}\right), \mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, h\right)\right), \ell\right)\right)\right), 1\right) \]
      distribute-rgt-neg-in [=>] 71.4	\[ \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\ell, h\right)\right)\right), \mathsf{neg.f64}\left(d\right)\right)}, \mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, h\right)\right), \ell\right)\right)\right), 1\right) \]

   if -7.99999999999999983e-113 < h < -6.69999999999999999e-164

   1. Initial program 66.7%

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

   2. Simplified 65.5%

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

      [Start] 66.7	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      associate-*l* [=>] 66.7	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)} \]
      metadata-eval [=>] 66.7	\[ \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \color{blue}{\frac{1}{2}}\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      unpow1/2 [=>] 66.7	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right)}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 66.7	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \color{blue}{\frac{1}{2}}\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      unpow1/2 [=>] 66.7	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)}, \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      associate-*l* [=>] 66.7	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{\_.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \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)\right) \]
      metadata-eval [=>] 66.7	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\color{blue}{\frac{1}{2}}, \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)\right) \]
      times-frac [=>] 65.5	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right)}, 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]

   3. Applied egg-rr 70.9%

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

      [Start] 65.5	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      frac-2neg [=>] 65.5	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(d\right), \mathsf{neg.f64}\left(\ell\right)\right)}\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      sqrt-div [=>] 70.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right), \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right)\right)}, \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]

   if -6.69999999999999999e-164 < h < -4.4000000000000001e-263

   1. Initial program 47.4%

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

   2. Simplified 45.5%

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

      [Start] 47.4	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      metadata-eval [=>] 47.4	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \color{blue}{\frac{1}{2}}\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      unpow1/2 [=>] 47.4	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right)}, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      metadata-eval [=>] 47.4	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \color{blue}{\frac{1}{2}}\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      unpow1/2 [=>] 47.4	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)}\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      *-commutative [=>] 47.4	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\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(1, 2\right)\right)}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      associate-*l* [=>] 47.4	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \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(\mathsf{/.f64}\left(1, 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)}\right)\right) \]
      times-frac [=>] 45.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right)}, 2\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 45.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\color{blue}{\frac{1}{2}}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]

   3. Applied egg-rr 53.0%

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

      [Start] 45.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      frac-2neg [=>] 45.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(d\right), \mathsf{neg.f64}\left(\ell\right)\right)}\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      sqrt-div [=>] 53.0	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right), \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right)\right)}\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]

   4. Taylor expanded in d around -inf 62.7%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\ell, h\right)\right)\right)\right)\right)} \]

   5. Simplified 62.7%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)\right), \mathsf{neg.f64}\left(d\right)\right)} \]
      Proof

      [Start] 62.7	\[ \mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\ell, h\right)\right)\right)\right)\right) \]
      mul-1-neg [=>] 62.7	\[ \color{blue}{\mathsf{neg.f64}\left(\mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\ell, h\right)\right)\right)\right)\right)} \]
      *-commutative [=>] 62.7	\[ \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\ell, h\right)\right)\right), d\right)}\right) \]
      distribute-rgt-neg-in [=>] 62.7	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\ell, h\right)\right)\right), \mathsf{neg.f64}\left(d\right)\right)} \]
      associate-/r* [=>] 62.7	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)}\right), \mathsf{neg.f64}\left(d\right)\right) \]

   if -4.4000000000000001e-263 < h < -1.999999999999994e-310

   1. Initial program 41.5%

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

   2. Simplified 40.7%

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

      [Start] 41.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      metadata-eval [=>] 41.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \color{blue}{\frac{1}{2}}\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      unpow1/2 [=>] 41.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right)}, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      metadata-eval [=>] 41.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \color{blue}{\frac{1}{2}}\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      unpow1/2 [=>] 41.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)}\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      *-commutative [=>] 41.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\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(1, 2\right)\right)}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      associate-*l* [=>] 41.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \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(\mathsf{/.f64}\left(1, 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)}\right)\right) \]
      times-frac [=>] 40.7	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right)}, 2\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 40.7	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\color{blue}{\frac{1}{2}}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]

   3. Taylor expanded in M around 0 23.7%

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

   4. Simplified 32.3%

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

      [Start] 23.7	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), h\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{pow.f64}\left(d, 2\right)\right)\right)\right)\right)\right) \]
      associate-*r/ [=>] 23.7	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), h\right)\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{pow.f64}\left(d, 2\right)\right)\right)}\right)\right) \]
      *-commutative [=>] 23.7	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), h\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \ell\right)}\right)\right)\right) \]
      associate-*r/ [<=] 23.7	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), h\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \ell\right)\right)\right)}\right)\right) \]
      associate-*r* [=>] 23.7	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{pow.f64}\left(M, 2\right)\right), h\right)}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \ell\right)\right)\right)\right)\right) \]
      *-commutative [=>] 23.7	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), \mathsf{pow.f64}\left(D, 2\right)\right)}, h\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \ell\right)\right)\right)\right)\right) \]
      associate-*l* [=>] 24.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), h\right)\right)}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \ell\right)\right)\right)\right)\right) \]
      unpow2 [=>] 24.5	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), h\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(d, d\right)}, \ell\right)\right)\right)\right)\right) \]
      associate-*l* [=>] 25.2	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), h\right)\right), \color{blue}{\mathsf{*.f64}\left(d, \mathsf{*.f64}\left(d, \ell\right)\right)}\right)\right)\right)\right) \]
      times-frac [=>] 27.8	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{pow.f64}\left(M, 2\right), d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), h\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)}\right)\right)\right) \]
      unpow2 [=>] 27.8	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(M, M\right)}, d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), h\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right)\right) \]
      unpow2 [=>] 27.8	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(D, D\right)}, h\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right)\right) \]
      associate-*l* [=>] 32.3	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(D, h\right)\right)}, \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right)\right) \]

   5. Applied egg-rr 57.3%

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

      [Start] 32.3	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(D, h\right)\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right)\right) \]
      frac-2neg [=>] 32.3	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(d\right), \mathsf{neg.f64}\left(h\right)\right)}\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(D, h\right)\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right)\right) \]
      sqrt-div [=>] 57.3	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right), \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(h\right)\right)\right)}, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(D, h\right)\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right)\right) \]

   if -1.999999999999994e-310 < h

   1. Initial program 58.6%

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

   2. Simplified 57.9%

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

      [Start] 58.6	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(1, 2\right)\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      metadata-eval [=>] 58.6	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, h\right), \color{blue}{\frac{1}{2}}\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      unpow1/2 [=>] 58.6	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right)}, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \mathsf{/.f64}\left(1, 2\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      metadata-eval [=>] 58.6	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(d, \ell\right), \color{blue}{\frac{1}{2}}\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      unpow1/2 [=>] 58.6	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)}\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(2, d\right)\right), 2\right)\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      *-commutative [=>] 58.6	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\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(1, 2\right)\right)}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right) \]
      associate-*l* [=>] 58.6	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \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(\mathsf{/.f64}\left(1, 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)}\right)\right) \]
      times-frac [=>] 57.9	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right)}, 2\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 57.9	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\color{blue}{\frac{1}{2}}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]

   3. Applied egg-rr 74.6%

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

      [Start] 57.9	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right) \]
      sub-neg [=>] 57.9	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \color{blue}{\mathsf{+.f64}\left(1, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)}\right) \]
      distribute-lft-in [=>] 57.9	\[ \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), 1\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right)} \]
      *-commutative [<=] 57.9	\[ \mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(1, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right)\right)}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      *-un-lft-identity [<=] 57.9	\[ \mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right)}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      sqrt-div [=>] 58.4	\[ \mathsf{+.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(d\right), \mathsf{sqrt.f64}\left(h\right)\right)}, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      sqrt-div [=>] 62.0	\[ \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(d\right), \mathsf{sqrt.f64}\left(h\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(d\right), \mathsf{sqrt.f64}\left(\ell\right)\right)}\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      frac-times [=>] 62.0	\[ \mathsf{+.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(d\right), \mathsf{sqrt.f64}\left(d\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      add-sqr-sqrt [<=] 62.1	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(\color{blue}{d}, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      sqrt-div [=>] 71.5	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(d\right), \mathsf{sqrt.f64}\left(h\right)\right)}, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      sqrt-div [=>] 74.6	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(d\right), \mathsf{sqrt.f64}\left(h\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(d\right), \mathsf{sqrt.f64}\left(\ell\right)\right)}\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      frac-times [=>] 74.6	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(d\right), \mathsf{sqrt.f64}\left(d\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      add-sqr-sqrt [<=] 74.6	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(\color{blue}{d}, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      distribute-rgt-neg-in [=>] 74.6	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(M, 2\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)}\right)\right) \]

   4. Simplified 74.6%

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

      [Start] 74.6	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(M, \frac{1}{2}\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right) \]
      *-commutative [<=] 74.6	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(M, \frac{1}{2}\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)}\right) \]
      distribute-rgt1-in [=>] 74.6	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(M, \frac{1}{2}\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), 1\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)} \]
      distribute-lft-neg-in [=>] 74.6	\[ \mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(M, \frac{1}{2}\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\frac{1}{2}\right), \mathsf{/.f64}\left(h, \ell\right)\right)}\right), 1\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right) \]
      metadata-eval [=>] 74.6	\[ \mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(M, \frac{1}{2}\right), \mathsf{/.f64}\left(D, d\right)\right), 2\right), \mathsf{*.f64}\left(\color{blue}{\frac{-1}{2}}, \mathsf{/.f64}\left(h, \ell\right)\right)\right), 1\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right) \]

3. Recombined 6 regimes into one program.

4. Final simplification 69.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(h, -10999999999999999171953497884844250523529691012412235626036558041901464462448164171098019924470539502084351596882522486672778602423884998913414301791154048434817917175130382501194005217280\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right), \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right)\right), \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\mathsf{/.f64}\left(D, d\right), 2\right)\right), 2\right), \mathsf{/.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(\ell, h\right)\right), 1\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-6931674235302037}{86645927941275464361825443254471365732388658605494267974077486894206915868925800719999200190754361815543475342543861619655442432}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right)\right), \ell\right), -1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-8688048222344579}{129672361527531029953512745740348785969138944757576153124864291552832900356653379574990845279596993571506183956603149661949848471106617978371464838566061365220661931356297172615168}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right), \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{/.f64}\left(M, 2\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-3119885634089587}{70906491683854249133971333415503528601229677279443476631916611638829262598057001759775558209235971002092300595769547131083230268742795262708226708464736682213924924871800416657575912944521796077262840069882938251784694133132833485038618990914757637167551284096438594475925700608}\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-20240225330731}{101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right), \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(h\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(h, D\right)\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	68.1%
Cost	28048

\[\begin{array}{l} t_0 := \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right)\\ t_1 := \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(d, 2\right), -500000000000000003724490251037159945720997469291576936179821270656319926233908080131859938186953529204232801301392323141862716916404886591545284620558119418548269448680219607040\right):\\ \;\;\;\;\mathsf{/.f64}\left(d, \mathsf{neg.f64}\left(t_1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(d, 2\right), \frac{-4230758200257591}{42307582002575910332922579714097346549017899709713998034217522897561970639123926132812109468141778230245837569601494931472384}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{+.f64}\left(1, \mathsf{+.f64}\left(1, \mathsf{\_.f64}\left(-1, \mathsf{*.f64}\left(t_0, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(d, 2\right), \frac{-1487016908477783}{148701690847778306279806249814990056013126020165939445905577185931594065716040437354516831449615635058979872379019297305045458524554490570779083058110239462578297084044745987394268640983429773687023919578235143720606774870687788008815709894034865808301204510545414391282376534881468416}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(d, t_1\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{/.f64}\left(d, M\right), D\right)\right), 2\right)\right), \ell\right), -1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(d, 2\right), \frac{178220336625867}{17822033662586700072817076584766762987864173856439687228824970773044043621908896041038721919208482030385321521771853153557377752817872804680674458280164899172859354196719784961261227313463296}\right):\\ \;\;\;\;\mathsf{fma.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(h, \ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(h, \mathsf{pow.f64}\left(\ell, 3\right)\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(\frac{-1}{8}, d\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(M, D\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(t_0, \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternative 2
Accuracy	68.6%
Cost	28048

\[\begin{array}{l} t_0 := \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right)\\ t_1 := \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(d, 2\right), -500000000000000003724490251037159945720997469291576936179821270656319926233908080131859938186953529204232801301392323141862716916404886591545284620558119418548269448680219607040\right):\\ \;\;\;\;\mathsf{/.f64}\left(d, \mathsf{neg.f64}\left(t_1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(d, 2\right), \frac{-4542742026847543}{22713710134237715329666368996500141698551292521478689383796568724394977753543685103943470334805111423773828800195818060422956300894208}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(t_0, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(h, \ell\right)\right)\right), 2\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(d, 2\right), \frac{-1487016908477783}{148701690847778306279806249814990056013126020165939445905577185931594065716040437354516831449615635058979872379019297305045458524554490570779083058110239462578297084044745987394268640983429773687023919578235143720606774870687788008815709894034865808301204510545414391282376534881468416}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(d, t_1\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), \mathsf{pow.f64}\left(\mathsf{/.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{/.f64}\left(d, M\right), D\right)\right), 2\right)\right), \ell\right), -1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(d, 2\right), \frac{178220336625867}{17822033662586700072817076584766762987864173856439687228824970773044043621908896041038721919208482030385321521771853153557377752817872804680674458280164899172859354196719784961261227313463296}\right):\\ \;\;\;\;\mathsf{fma.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(h, \ell\right)\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(h, \mathsf{pow.f64}\left(\ell, 3\right)\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(\frac{-1}{8}, d\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(M, D\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(t_0, 2\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternative 3
Accuracy	69.5%
Cost	27660

\[\begin{array}{l} t_0 := \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right)\\ t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(t_0, \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{/.f64}\left(M, 2\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(h, -949999999999999988242881872021390734567600721361268519705276401293316602519976139987779130391981160399461440439089024282188833036386678095164696694835410500879363435665300089408827893141170733136740352\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-7581518694861603}{21661481985318866090456360813617841433097164651373566993519371723551728967231450179999800047688590453885868835635965404913860608}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right)\right), \ell\right), -1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-8428703499289517}{129672361527531029953512745740348785969138944757576153124864291552832900356653379574990845279596993571506183956603149661949848471106617978371464838566061365220661931356297172615168}\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-283625966735417}{8863311460481781141746416676937941075153709659930434578989576454853657824757125219971944776154496375261537574471193391385403783592849407838528338558092085276740615608975052082196989118065224509657855008735367281473086766641604185629827373864344704645943910512054824309490712576}\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-20240225330731}{101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(t_0, \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(h\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(h, D\right)\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternative 4
Accuracy	69.4%
Cost	21188

\[\begin{array}{l} t_0 := \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right)\\ t_1 := \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\ell, -78000000000000002850058554676951385781446834406520554834761296606148494433175742042349556625315774922430434820706048865521164157169030466327363085214606996920225287506417121099167915504736997254479755699488232805319878758933749483974955520031310496137216\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(t_0, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(d\right)\right), \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(h, D\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(d, \ell\right), \mathsf{/.f64}\left(d, M\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\ell, \frac{-2612212911805101}{1412006979354108748474554421102313931675676955925788762341700965431346915180599249952936960497614998485448932749141998289061648432939195473813276544243473053215398045741358060286316036246351763861878679739417265182867456}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right)\right), \ell\right), -1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\ell, \frac{6134599390373507}{21153791001287955166461289857048673274508949854856999017108761448780985319561963066406054734070889115122918784800747465736192}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(t_0, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), t_1\right), \ell\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(t_1, \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternative 5
Accuracy	67.4%
Cost	21132

\[\begin{array}{l} t_0 := \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right)\\ t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\ell, -18000000000000001780008343538797832551807609702604492827114516903080237993839429948315573974649423558329658808954231711277123425412106573364373972281286044415155620367551627845531820688153163765486425145430292624930943788436949731116839865067641935785432157828456810283008\right):\\ \;\;\;\;\mathsf{*.f64}\left(t_1, \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(M, \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(h, D\right)\right), \mathsf{/.f64}\left(\ell, D\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\ell, -117999999999999999094030336\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\right), \mathsf{+.f64}\left(-1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\frac{1}{2}, d\right)\right)\right), 2\right), \mathsf{/.f64}\left(\ell, h\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\ell, \frac{6972074670834653}{1291124939043454294827959586001505937164852896414611756415329678270323811008420597314822676640068915717951585986373746688}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t_1, \mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), t_0\right), \ell\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(t_0, \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternative 6
Accuracy	68.8%
Cost	21132

\[\begin{array}{l} t_0 := \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right)\\ t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\ell, -41999999999999999148341582387394789306779292299905909055427477074184864200359076037648630861360849671162404834005620093943941869491273591728412157788171929127722509764350358279756299878422330561716092079907074578185690227751131936385733655368086437322932443440000779943936\right):\\ \;\;\;\;\mathsf{*.f64}\left(t_1, \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(M, \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(h, D\right)\right), \mathsf{/.f64}\left(\ell, D\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\ell, \frac{-7048738840935711}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(d, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right)\right), \ell\right), -1\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\ell, \frac{2340163952016261}{161390617380431786853494948250188242145606612051826469551916209783790476376052574664352834580008614464743948248296718336}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t_1, \mathsf{\_.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \frac{1}{2}\right), t_0\right), \ell\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(t_0, \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternative 7
Accuracy	68.6%
Cost	21004

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(d, -449999999999999991186922566169646521151791657090283757561770864714079943707886397246817891658047827479840140455650940429667499782434620215966198221098193419175049822208\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{-5288447750321989}{10576895500643977583230644928524336637254474927428499508554380724390492659780981533203027367035444557561459392400373732868096}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(\ell, D\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{3668540841195005}{6325070415853456823515479584966165845298645305129441198653167438357198111499854590373761990669910140474596183259900372230931523043306046152094168748148078435047419508642698792639590866940413010663742739952273283392562733857021646831815729864036236135650314266011211548510419206725953204130822734645187695728365866909171712}\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternative 8
Accuracy	67.8%
Cost	21004

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(d, -559999999999999979721637019884312129395823368958293309771755256232804084306229847322592799845607451418055023284460456638841875988636658731428850277959300458838916857856\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{-2003687083641995}{5415370496329716522614090203404460358274291162843391748379842930887932241807862544999950011922147613471467208908991351228465152}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{*.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{/.f64}\left(M, 2\right)\right), 2\right), \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{3459022883669859}{24707306311927565716857342128774085333197833223161879682238935306082805123046306993647507776054336486228891340858985829027076261887914242781617846672453431386903982455635542158748401823985988322905245077938567513252198179128990807936780194781391547404884040101606295111368825026273254703636026307207764436438929167613952}\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternative 9
Accuracy	67.8%
Cost	21004

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(d, -749999999999999950395371126057230921778962662322748638958769616730775485024702735719269324446884460378185915949773891106654535610083609594959593879052796463120788750336\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{-6931674235302037}{43322963970637732180912721627235682866194329302747133987038743447103457934462900359999600095377180907771737671271930809827721216}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{/.f64}\left(M, 2\right)\right), 2\right), \mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{3668540841195005}{6325070415853456823515479584966165845298645305129441198653167438357198111499854590373761990669910140474596183259900372230931523043306046152094168748148078435047419508642698792639590866940413010663742739952273283392562733857021646831815729864036236135650314266011211548510419206725953204130822734645187695728365866909171712}\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(M, \frac{1}{2}\right)\right), 2\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{/.f64}\left(h, \ell\right)\right)\right)\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(h\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\right)\\ \end{array} \]

Alternative 10
Accuracy	65.0%
Cost	15188

\[\begin{array}{l} t_0 := \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(\ell, D\right)\right)\right)\right)\right)\right)\right)\\ t_1 := \mathsf{/.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(d, -54999999999999999399195712042861843983973923997292381397719463591100635622864867622392636604429917340024829037787045052946881823978555222005624674703103166829412674902687744\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{-6346137300386387}{1322111937580497197903830616065542079656809365928562438569297590548811582472622691650378420879430569695182424050046716608512}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{-101201126653655}{202402253307310618352495346718917307049556649764142118356901358027430339567995346891960383701437124495187077864316811911389808737385793476867013399940738509921517424276566361364466907742093216341239767678472745068562007483424692698618103355649159556340810056512358769552333414615230502532186327508646006263307707741093494784}\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{3504353730807743}{4171849679533027504677776769862406473833407270227837441302815640277772901915313574263597826048}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(h, \frac{-1}{2}\right)\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, 21499999999999999782608382652754161255850738085808615665875668623463406433892701883329624377730924061218056899826248043250396446431169606447458766752004808901027430400\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{pow.f64}\left(h, \frac{-1}{2}\right), \mathsf{/.f64}\left(d, \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\\ \end{array} \]

Alternative 11
Accuracy	63.0%
Cost	15056

\[\begin{array}{l} t_0 := \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{/.f64}\left(M, \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(h, D\right)\right), \mathsf{/.f64}\left(\ell, D\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(h, -6199999999999999764697155357665101075003386584975977446570217950880864730611712\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-20240225330731}{101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392}\right):\\ \;\;\;\;\mathsf{/.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{5476250592985951}{20282409603651670423947251286016}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{pow.f64}\left(h, \frac{-1}{2}\right), \mathsf{/.f64}\left(d, \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, 8799999999999999940412054634584491033218175325306546070205165050979282439122022269087656659433486937438103273472\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(h, \frac{-1}{2}\right)\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\\ \end{array} \]

Alternative 12
Accuracy	58.8%
Cost	14864

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(h, -9999999999999999338604948347429745623719502164303315186116928223077006466996036476256924325958459471709145545996985214755393808134448127932794585054037286174943850004480\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right), \mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(h, D\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(D, d\right), \ell\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-20240225330731}{101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392}\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, 25999999999999997256817825017964609482768800836853525517434880\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{pow.f64}\left(h, \frac{-1}{2}\right), \mathsf{/.f64}\left(d, \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, 250000000000000008195561495715524562142676320755373391065833394360235650799343583981983594668102948263454374395456037704675408669227673923998497775323260630281194701061405016453818318088787399122582137228127575157273150348111208913032737141206501155519696419202713776425316175052800\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{/.f64}\left(h, \ell\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right)\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\ell, d\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(h, \frac{-1}{2}\right)\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\\ \end{array} \]

Alternative 13
Accuracy	58.5%
Cost	14864

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(h, -8200000000000000630839251514869637624177179117740254607060390444757565853748376236185030578721297236965500437321577798977210513987776914608356305789635444976398245036032\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{\_.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{8}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(M, M\right), d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(h, D\right)\right), \mathsf{*.f64}\left(d, \ell\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, \frac{-20240225330731}{101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392}\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, 95000000000000002328016316751831197652976123293749638856704\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{pow.f64}\left(h, \frac{-1}{2}\right), \mathsf{/.f64}\left(d, \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, 290000000000000009506851335030008492085504532076233133636366737457873354927238557419100969814999419985607074298729003737423474056304101751838257419374982331126185853231229819086429248982993382982195279184627987182436854403809002339117975083799541340402847846275147980653366763061248\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{/.f64}\left(h, \ell\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right)\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\ell, d\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(h, \frac{-1}{2}\right)\right), \mathsf{sqrt.f64}\left(\ell\right)\right)\\ \end{array} \]

Alternative 14
Accuracy	61.9%
Cost	14600

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(d, -380000000000000017675540837311538515958300672\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{-3384606560206073}{84615164005151820665845159428194693098035799419427996068435045795123941278247852265624218936283556460491675139202989862944768}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{/.f64}\left(h, \ell\right), \mathsf{*.f64}\left(\frac{-1}{2}, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(M, D\right), d\right)\right), 2\right)\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \mathsf{*.f64}\left(h, \mathsf{/.f64}\left(\ell, d\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{8168717604814363}{23010472126237643618935106442099516590310105330461524130999050388189782503104123280986685097268164610703374576623538349780325090408245327679084471121852687920354290358382782115366684108959500047289994617866880738411283287339835248828660878149225886356908865367627046174713247480125403687018925610191900689563648}\right):\\ \;\;\;\;\mathsf{/.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{pow.f64}\left(h, \frac{-1}{2}\right), \mathsf{/.f64}\left(d, \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\\ \end{array} \]

Alternative 15
Accuracy	61.8%
Cost	13580

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(h, \ell\right)\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(d, -1700000000000000013261040562274904564538799726111371026758932365976779015547714735855214917352441017708126288134207121102465617881162908502517730821185431897555913932800\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{-5427754182999197}{904625697166532776746648320380374280103671755200316906558262375061821325312}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, h\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(d, \ell\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(d, \frac{5007078734669311}{2945340432158418383223693624588738123559693482299075088767878449688292160397327779966295692450325070170031945807812908771881611572255401942922812303597144053805349165872996110766935565946816006053119311086960734516644260779498911850068592403100913453684334767056261910363295677456051671938422478104563288264146944}\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{pow.f64}\left(h, \frac{-1}{2}\right), \mathsf{/.f64}\left(d, \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\\ \end{array} \]

Alternative 16
Accuracy	60.5%
Cost	13316

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\ell, \frac{5778221434296339}{33018408195979077897021236557282287907427957877257595132997544314167118909795303717151078492978574243417149687078570542430146722468917846078158686153933723556774167749937817760545719854776652565814014556763199275259251768296972608677399806172939779780596161306108624896}\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{pow.f64}\left(h, \frac{-1}{2}\right), \mathsf{/.f64}\left(d, \mathsf{sqrt.f64}\left(\ell\right)\right)\right)\\ \end{array} \]

Alternative 17
Accuracy	48.7%
Cost	7113

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(h, \frac{-8482580444616245}{94250893829069388263158195986839619953910191433570402840572110390025349132714488958921462158410402245441022265850013080700211570312172862173529993715108609721771173307935875544541938110298112193699817954782743504532616344943965179202194956899229230517898712545800381131625461678593653502029519299346025224452702208}\right) \lor \neg \mathsf{<=.f64}\left(h, 179999999999999984217607690792114027531587407770687660963029359974670982070394038534385755893135755381946974208\right):\\ \;\;\;\;\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(d, \mathsf{/.f64}\left(\mathsf{/.f64}\left(d, h\right), \ell\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(h, \ell\right), \frac{-1}{2}\right)\right)\\ \end{array} \]

Alternative 18
Accuracy	48.1%
Cost	7113

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(h, \frac{-8482580444616245}{94250893829069388263158195986839619953910191433570402840572110390025349132714488958921462158410402245441022265850013080700211570312172862173529993715108609721771173307935875544541938110298112193699817954782743504532616344943965179202194956899229230517898712545800381131625461678593653502029519299346025224452702208}\right) \lor \neg \mathsf{<=.f64}\left(h, 669999999999999974190387679263636777768431691617009664\right):\\ \;\;\;\;\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(d, \ell\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(h, \ell\right), \frac{-1}{2}\right)\right)\\ \end{array} \]

Alternative 19
Accuracy	56.4%
Cost	7112

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(h, \frac{-8482580444616245}{94250893829069388263158195986839619953910191433570402840572110390025349132714488958921462158410402245441022265850013080700211570312172862173529993715108609721771173307935875544541938110298112193699817954782743504532616344943965179202194956899229230517898712545800381131625461678593653502029519299346025224452702208}\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(h, \ell\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, 350000000000000018894979968585223758222510919165935616\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(h, \ell\right), \frac{-1}{2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(d, \ell\right)\right)\right)\\ \end{array} \]

Alternative 20
Accuracy	56.7%
Cost	7112

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(h, \frac{-8482580444616245}{94250893829069388263158195986839619953910191433570402840572110390025349132714488958921462158410402245441022265850013080700211570312172862173529993715108609721771173307935875544541938110298112193699817954782743504532616344943965179202194956899229230517898712545800381131625461678593653502029519299346025224452702208}\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \ell\right), h\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(h, 239999999999999998373027681846790714350810026066575360\right):\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(h, \ell\right), \frac{-1}{2}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(d, h\right), \mathsf{/.f64}\left(d, \ell\right)\right)\right)\\ \end{array} \]

Alternative 21
Accuracy	46.1%
Cost	6980

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(h, \frac{-8482580444616245}{94250893829069388263158195986839619953910191433570402840572110390025349132714488958921462158410402245441022265850013080700211570312172862173529993715108609721771173307935875544541938110298112193699817954782743504532616344943965179202194956899229230517898712545800381131625461678593653502029519299346025224452702208}\right):\\ \;\;\;\;\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(d, \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(h, \ell\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(h, \ell\right), \frac{-1}{2}\right)\right)\\ \end{array} \]

Alternative 22
Accuracy	31.6%
Cost	6784

\[\mathsf{*.f64}\left(d, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(h, \ell\right), \frac{-1}{2}\right)\right) \]

Reproduce

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