?

Average Accuracy: 6.8% → 85.4%
Time: 33.8s
Precision: binary64
Cost: 2889

?

\[\mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]
\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_0, 0\right) \lor \neg \mathsf{<=.f64}\left(t_0, +\infty\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, d\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(w, D\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), D\right)\right)\right)\\ \end{array} \]
(FPCore (c0 w h D d M)
 :precision binary64
 (*.f64
  (/.f64 c0 (*.f64 2 w))
  (+.f64
   (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))
   (sqrt.f64
    (-.f64
     (*.f64
      (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))
      (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))))
     (*.f64 M M))))))
(FPCore (c0 w h D d M)
 :precision binary64
 (let* ((t_0 (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))))
   (if (or (<=.f64 t_0 0) (not (<=.f64 t_0 +inf.0)))
     (*.f64 1/4 (*.f64 (/.f64 D (/.f64 d M)) (*.f64 h (*.f64 D (/.f64 M d)))))
     (*.f64
      (/.f64 (*.f64 c0 d) (*.f64 w D))
      (/.f64 (*.f64 c0 d) (*.f64 (*.f64 w h) D))))))
\mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right)
\begin{array}{l}
t_0 := \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\\
\mathbf{if}\;\mathsf{<=.f64}\left(t_0, 0\right) \lor \neg \mathsf{<=.f64}\left(t_0, +\infty\right):\\
\;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, d\right)\right)\right)\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(w, D\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), D\right)\right)\right)\\


\end{array}

Error?

Derivation?

  1. Split input into 2 regimes
  2. if (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) < -0.0 or +inf.0 < (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D)))

    1. Initial program 3.6%

      \[\mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]
    2. Simplified1.6%

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

      [Start]3.6

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      associate-*l/ [<=]2.9

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{*.f64}\left(d, d\right)\right)}, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      *-commutative [=>]2.9

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right)}, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      fma-def [=>]2.0

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \color{blue}{\mathsf{fma.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)}\right) \]

      associate-*l* [=>]1.7

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{/.f64}\left(c0, \color{blue}{\mathsf{*.f64}\left(w, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(D, D\right)\right)\right)}\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      *-commutative [=>]1.7

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{/.f64}\left(c0, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, \mathsf{*.f64}\left(D, D\right)\right), w\right)}\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      associate-*r* [=>]1.6

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, D\right), D\right)}, w\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      associate-*l* [=>]1.7

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{/.f64}\left(c0, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(h, D\right), \mathsf{*.f64}\left(D, w\right)\right)}\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      *-commutative [<=]1.7

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{fma.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(\mathsf{*.f64}\left(h, D\right), \color{blue}{\mathsf{*.f64}\left(w, D\right)}\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]
    3. Taylor expanded in c0 around -inf 6.3%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(w, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), h\right)\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), c0\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(w, h\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(w, h\right)\right)\right)\right)\right), c0\right)\right)\right)}\right) \]
    4. Simplified51.9%

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

      [Start]6.3

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(w, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), h\right)\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), c0\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(w, h\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(w, h\right)\right)\right)\right)\right), c0\right)\right)\right)\right) \]

      fma-def [=>]6.3

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \color{blue}{\mathsf{fma.f64}\left(\frac{1}{2}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(w, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(M, 2\right), h\right)\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), c0\right)\right), \mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(w, h\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(w, h\right)\right)\right)\right)\right), c0\right)\right)\right)}\right) \]
    5. Taylor expanded in c0 around 0 50.2%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\frac{1}{4}, \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{pow.f64}\left(d, 2\right)\right)\right)} \]
    6. Simplified53.4%

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

      [Start]50.2

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \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{pow.f64}\left(d, 2\right)\right)\right) \]

      unpow2 [=>]50.2

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

      associate-*r* [<=]53.6

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

      associate-/l* [=>]53.4

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

      unpow2 [=>]53.4

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

      unpow2 [=>]53.4

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, D\right), \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(d, d\right)}, \mathsf{*.f64}\left(M, \mathsf{*.f64}\left(M, h\right)\right)\right)\right)\right) \]
    7. Applied egg-rr77.6%

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

      [Start]53.4

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, D\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{*.f64}\left(M, \mathsf{*.f64}\left(M, h\right)\right)\right)\right)\right) \]

      times-frac [=>]64.5

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, D\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(d, M\right), \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(M, h\right)\right)\right)}\right)\right) \]

      times-frac [=>]77.6

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(M, h\right)\right)\right)\right)}\right) \]
    8. Applied egg-rr85.3%

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

      [Start]77.6

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, \mathsf{*.f64}\left(M, h\right)\right)\right)\right)\right) \]

      associate-/r* [=>]82.1

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{/.f64}\left(D, \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(d, M\right), h\right)}\right)\right)\right) \]

      associate-/r/ [=>]85.5

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), h\right)}\right)\right) \]

      div-inv [=>]85.3

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(D, \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(d, M\right)\right)\right)}, h\right)\right)\right) \]

      clear-num [<=]85.3

      \[ \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(D, \color{blue}{\mathsf{/.f64}\left(M, d\right)}\right), h\right)\right)\right) \]

    if -0.0 < (/.f64 (*.f64 c0 (*.f64 d d)) (*.f64 (*.f64 w h) (*.f64 D D))) < +inf.0

    1. Initial program 25.9%

      \[\mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]
    2. Simplified26.3%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{fma.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(w, h\right)\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(d, d\right), D\right), D\right), \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(w, h\right)\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(d, d\right), D\right), D\right), M\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(w, h\right)\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(d, d\right), D\right), D\right)\right), M\right)\right)\right)\right)\right)} \]
      Proof

      [Start]25.9

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      times-frac [=>]22.6

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(w, h\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{*.f64}\left(D, D\right)\right)\right)}, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      fma-def [=>]22.6

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \color{blue}{\mathsf{fma.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(w, h\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(d, d\right), \mathsf{*.f64}\left(D, D\right)\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)}\right) \]

      associate-/r* [=>]22.6

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{fma.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(w, h\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(d, d\right), D\right), D\right)}, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\right) \]

      difference-of-squares [=>]22.6

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(2, w\right)\right), \mathsf{fma.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(w, h\right)\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(d, d\right), D\right), D\right), \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), M\right), \mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), M\right)\right)}\right)\right)\right) \]
    3. Taylor expanded in c0 around inf 15.1%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \mathsf{pow.f64}\left(c0, 2\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(w, 2\right), h\right)\right)\right)} \]
    4. Simplified49.4%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(c0, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(D, w\right), \mathsf{*.f64}\left(D, w\right)\right), h\right)\right)} \]
      Proof

      [Start]15.1

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(d, 2\right), \mathsf{pow.f64}\left(c0, 2\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(w, 2\right), h\right)\right)\right) \]

      *-commutative [=>]15.1

      \[ \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(c0, 2\right), \mathsf{pow.f64}\left(d, 2\right)\right)}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(w, 2\right), h\right)\right)\right) \]

      unpow2 [=>]15.1

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(c0, c0\right)}, \mathsf{pow.f64}\left(d, 2\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(w, 2\right), h\right)\right)\right) \]

      unpow2 [=>]15.1

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c0, c0\right), \color{blue}{\mathsf{*.f64}\left(d, d\right)}\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(w, 2\right), h\right)\right)\right) \]

      unswap-sqr [=>]30.8

      \[ \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(c0, d\right)\right)}, \mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(w, 2\right), h\right)\right)\right) \]

      associate-*r* [=>]30.1

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(c0, d\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(D, 2\right), \mathsf{pow.f64}\left(w, 2\right)\right), h\right)}\right) \]

      unpow2 [=>]30.1

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(c0, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(D, D\right)}, \mathsf{pow.f64}\left(w, 2\right)\right), h\right)\right) \]

      unpow2 [=>]30.1

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(c0, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(D, D\right), \color{blue}{\mathsf{*.f64}\left(w, w\right)}\right), h\right)\right) \]

      unswap-sqr [=>]49.4

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(c0, d\right)\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(D, w\right), \mathsf{*.f64}\left(D, w\right)\right)}, h\right)\right) \]
    5. Applied egg-rr85.9%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(D, w\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(w, h\right)\right)\right)\right)} \]
      Proof

      [Start]49.4

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(c0, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(D, w\right), \mathsf{*.f64}\left(D, w\right)\right), h\right)\right) \]

      associate-*l* [=>]59.4

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(c0, d\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(D, w\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(D, w\right), h\right)\right)}\right) \]

      times-frac [=>]86.9

      \[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(D, w\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(D, w\right), h\right)\right)\right)} \]

      associate-*l* [=>]85.9

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(D, w\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \color{blue}{\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(w, h\right)\right)}\right)\right) \]
  3. Recombined 2 regimes into one program.
  4. Final simplification85.4%

    \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), 0\right) \lor \neg \mathsf{<=.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, \mathsf{*.f64}\left(d, d\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), \mathsf{*.f64}\left(D, D\right)\right)\right), +\infty\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, d\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(w, D\right)\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(c0, d\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(w, h\right), D\right)\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy67.2%
Cost1736
\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(w, 2\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_0, 499999999999999962433880809496441021272335434917419230719612986112647099987896513301581746881408826875765029206827766141419520\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, M\right), d\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, 49999999999999996962677625276823109300201436100586624765953857856616022815066169514216546287202538742184280590280810862893585968713180152651178994204334413874936507208410055205338551265812204529218599012742757995383198412754109163297745561348039749026730174593312862032038021904229799310374521740690718720\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\mathsf{*.f64}\left(h, D\right), d\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(\mathsf{/.f64}\left(d, h\right), M\right)\right), \mathsf{/.f64}\left(d, M\right)\right)\right)\right)\\ \end{array} \]
Alternative 2
Accuracy67.0%
Cost1348
\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(c0, \mathsf{*.f64}\left(w, 2\right)\right), -100000000000000001440594758724527385583111862242831263013712314935498927069126131626863257625726456080505437183296233537536\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(h, M\right)\right)\right), d\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{*.f64}\left(M, \mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, h\right)\right)\right)\right)\right)\\ \end{array} \]
Alternative 3
Accuracy65.9%
Cost1225
\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(h, \frac{-4183246980753157}{1267650600228229401496703205376}\right) \lor \neg \mathsf{<=.f64}\left(h, 26999999999999999054058823669676079489786479815827088959474171220831679829737195545098705060330622778241289332874140185509345626632994943220276643547988489660158010912437867396785273035451189817959545871269888000\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{/.f64}\left(M, d\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{*.f64}\left(h, M\right)\right)\right), d\right)\right)\right)\\ \end{array} \]
Alternative 4
Accuracy67.2%
Cost1225
\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(D, \frac{5655053629744163}{377003575316277553052632783947358479815640765734281611362288441560101396530857955835685848633641608981764089063400052322800846281248691448694119974860434438887084693231743502178167752441192448774799271819130974018130465379775860716808779827596916922071594850183201524526501846714374614008118077197384100897810808832}\right) \lor \neg \mathsf{<=.f64}\left(D, 3000000000000000011682236791872338282844568556881242454458600847001102360681937407235708182555127571452408010234658816\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, d\right), \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(M, \mathsf{/.f64}\left(\mathsf{*.f64}\left(D, M\right), d\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{*.f64}\left(M, \mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, h\right)\right)\right)\right)\right)\\ \end{array} \]
Alternative 5
Accuracy66.2%
Cost1220
\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(w, 2\right), \frac{3135285318820699}{627057063764139831929324851379409869378845668175598843037877190478889006888518431438644711527536922839520331484815861906173161536477065546885468336421475511783984145060592245840032548652210559519683510272}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(\mathsf{/.f64}\left(d, h\right), M\right)\right), \mathsf{/.f64}\left(d, M\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{/.f64}\left(M, d\right)\right)\right)\right)\right)\right)\\ \end{array} \]
Alternative 6
Accuracy62.9%
Cost960
\[\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(h, M\right), d\right)\right)\right)\right)\right) \]
Alternative 7
Accuracy64.5%
Cost960
\[\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(D, \mathsf{*.f64}\left(\mathsf{/.f64}\left(M, d\right), \mathsf{/.f64}\left(M, d\right)\right)\right)\right)\right)\right) \]
Alternative 8
Accuracy74.1%
Cost960
\[\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{*.f64}\left(\mathsf{/.f64}\left(D, \mathsf{/.f64}\left(d, M\right)\right), \mathsf{*.f64}\left(h, \mathsf{*.f64}\left(D, \mathsf{/.f64}\left(M, d\right)\right)\right)\right)\right) \]
Alternative 9
Accuracy50.5%
Cost64
\[0 \]

Error

Reproduce?

herbie shell --seed 2023144 
(FPCore (c0 w h D d M)
  :name "Henrywood and Agarwal, Equation (13)"
  :precision binary64
  (* (/ c0 (* 2.0 w)) (+ (/ (* c0 (* d d)) (* (* w h) (* D D))) (sqrt (- (* (/ (* c0 (* d d)) (* (* w h) (* D D))) (/ (* c0 (* d d)) (* (* w h) (* D D)))) (* M M))))))