Maksimov and Kolovsky, Equation (32)

Average Accuracy: 76.6% → 97.7%

Time: 25.3s

Precision: binary64

Cost: 21192

\[ \begin{array}{c}[m, n] = \mathsf{sort}([m, n])\\ \end{array} \]

Math

\[\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)\right) \]

↓

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_0, -500\right):\\ \;\;\;\;\mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{-1}{4}\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, \frac{5902958103587057}{1180591620717411303424}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(K, \mathsf{/.f64}\left(2, \mathsf{+.f64}\left(m, n\right)\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(n, \mathsf{*.f64}\left(n, \frac{1}{4}\right)\right)\right)\right)\\ \end{array} \]

FPCore

(FPCore (K m n M l)
 :precision binary64
 (*.f64
  (cos.f64 (-.f64 (/.f64 (*.f64 K (+.f64 m n)) 2) M))
  (exp.f64
   (-.f64
    (neg.f64 (pow.f64 (-.f64 (/.f64 (+.f64 m n) 2) M) 2))
    (-.f64 l (fabs.f64 (-.f64 m n)))))))

↓

(FPCore (K m n M l)
 :precision binary64
 (let* ((t_0 (/.f64 (+.f64 m n) 2)))
   (if (<=.f64 t_0 -500)
     (exp.f64 (*.f64 m (*.f64 m -1/4)))
     (if (<=.f64 t_0 5902958103587057/1180591620717411303424)
       (/.f64
        (cos.f64 (-.f64 (/.f64 K (/.f64 2 (+.f64 m n))) M))
        (exp.f64 (+.f64 (-.f64 l (fabs.f64 (-.f64 n m))) (*.f64 M M))))
       (/.f64 (cos.f64 M) (exp.f64 (*.f64 n (*.f64 n 1/4))))))))

Derivation

1. Split input into 3 regimes

2. if (/.f64 (+.f64 m n) 2) < -500

   1. Initial program 72.5%

      \[\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)\right) \]

   2. Simplified 72.6%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 72.5	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)\right) \]
      sub-neg [=>] 72.5	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \color{blue}{\mathsf{+.f64}\left(\ell, \mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)}\right)\right)\right) \]
      associate--r+ [=>] 72.5	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right), \mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)}\right)\right) \]
      exp-diff [=>] 0.0	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right), \mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)}\right) \]
      associate-*r/ [=>] 0.0	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right)\right), \mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)} \]
      associate-/l* [=>] 0.0	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right)\right)\right)} \]
      associate-*r/ [<=] 0.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right)}, M\right)\right), \mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right)\right)\right) \]
      exp-diff [=>] 0.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right)\right), \mathsf{exp.f64}\left(\ell\right)\right)}\right)\right) \]

   3. Taylor expanded in K around 0 100.0%

      \[\leadsto \mathsf{/.f64}\left(\color{blue}{\mathsf{cos.f64}\left(\mathsf{neg.f64}\left(M\right)\right)}, \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]

   4. Simplified 100.0%

      \[\leadsto \mathsf{/.f64}\left(\color{blue}{\mathsf{cos.f64}\left(M\right)}, \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]
      Proof

      [Start] 100.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{neg.f64}\left(M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]
      cos-neg [=>] 100.0	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{cos.f64}\left(M\right)}, \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]

   5. Taylor expanded in m around inf 100.0%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{pow.f64}\left(m, 2\right)\right)}\right)\right) \]

   6. Simplified 100.0%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{1}{4}\right)\right)}\right)\right) \]
      Proof

      [Start] 100.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{pow.f64}\left(m, 2\right)\right)\right)\right) \]
      *-commutative [=>] 100.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(m, 2\right), \frac{1}{4}\right)}\right)\right) \]
      unpow2 [=>] 100.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(m, m\right)}, \frac{1}{4}\right)\right)\right) \]
      associate-*l* [=>] 100.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{1}{4}\right)\right)}\right)\right) \]

   7. Taylor expanded in M around 0 100.0%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(1, \mathsf{exp.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{pow.f64}\left(m, 2\right)\right)\right)\right)} \]

   8. Simplified 100.0%

      \[\leadsto \color{blue}{\mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{-1}{4}\right)\right)\right)} \]
      Proof

      [Start] 100.0	\[ \mathsf{/.f64}\left(1, \mathsf{exp.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{pow.f64}\left(m, 2\right)\right)\right)\right) \]
      *-commutative [=>] 100.0	\[ \mathsf{/.f64}\left(1, \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{pow.f64}\left(m, 2\right), \frac{1}{4}\right)}\right)\right) \]
      unpow2 [=>] 100.0	\[ \mathsf{/.f64}\left(1, \mathsf{exp.f64}\left(\mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(m, m\right)}, \frac{1}{4}\right)\right)\right) \]
      associate-*r* [<=] 100.0	\[ \mathsf{/.f64}\left(1, \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{1}{4}\right)\right)}\right)\right) \]
      rec-exp [=>] 100.0	\[ \color{blue}{\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{1}{4}\right)\right)\right)\right)} \]
      distribute-rgt-neg-in [=>] 100.0	\[ \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(m, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(m, \frac{1}{4}\right)\right)\right)}\right) \]
      distribute-rgt-neg-in [=>] 100.0	\[ \mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \color{blue}{\mathsf{*.f64}\left(m, \mathsf{neg.f64}\left(\frac{1}{4}\right)\right)}\right)\right) \]
      metadata-eval [=>] 100.0	\[ \mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \color{blue}{\frac{-1}{4}}\right)\right)\right) \]

   if -500 < (/.f64 (+.f64 m n) 2) < 5.00000000000000041e-6

   1. Initial program 91.8%

      \[\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)\right) \]

   2. Simplified 91.8%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 91.8	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)\right) \]
      sub-neg [=>] 91.8	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \color{blue}{\mathsf{+.f64}\left(\ell, \mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)}\right)\right)\right) \]
      associate--r+ [=>] 91.8	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right), \mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)}\right)\right) \]
      exp-diff [=>] 91.7	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right), \mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)}\right) \]
      associate-*r/ [=>] 91.7	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right)\right), \mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)} \]
      associate-/l* [=>] 91.7	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right)\right)\right)} \]
      associate-*r/ [<=] 91.7	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right)}, M\right)\right), \mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right)\right)\right) \]
      exp-diff [=>] 78.8	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right)\right), \mathsf{exp.f64}\left(\ell\right)\right)}\right)\right) \]

   3. Taylor expanded in M around inf 91.5%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{pow.f64}\left(M, 2\right)}, \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]

   4. Simplified 91.5%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(M, M\right)}, \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]
      Proof

      [Start] 91.5	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(M, 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]
      unpow2 [=>] 91.5	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(M, M\right)}, \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]

   5. Applied egg-rr 91.6%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{/.f64}\left(K, \mathsf{/.f64}\left(2, \mathsf{+.f64}\left(m, n\right)\right)\right)}, M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(M, M\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]
      Proof

      [Start] 91.5	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(M, M\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]
      clear-num [=>] 91.5	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \color{blue}{\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(2, \mathsf{+.f64}\left(m, n\right)\right)\right)}\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(M, M\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]
      un-div-inv [=>] 91.6	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{/.f64}\left(K, \mathsf{/.f64}\left(2, \mathsf{+.f64}\left(m, n\right)\right)\right)}, M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(M, M\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]

   if 5.00000000000000041e-6 < (/.f64 (+.f64 m n) 2)

   1. Initial program 72.0%

      \[\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)\right) \]

   2. Simplified 72.0%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 72.0	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)\right) \]
      sub-neg [=>] 72.0	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \color{blue}{\mathsf{+.f64}\left(\ell, \mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)}\right)\right)\right) \]
      associate--r+ [=>] 72.0	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right), \mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)}\right)\right) \]
      exp-diff [=>] 1.0	\[ \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right), \mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)}\right) \]
      associate-*r/ [=>] 1.0	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right)\right), \mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right)\right)} \]
      associate-/l* [=>] 1.0	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(K, \mathsf{+.f64}\left(m, n\right)\right), 2\right), M\right)\right), \mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right)\right)\right)} \]
      associate-*r/ [<=] 1.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right)}, M\right)\right), \mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right), \mathsf{exp.f64}\left(\mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right), \ell\right)\right)\right)\right) \]
      exp-diff [=>] 0.8	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(K, \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\right), M\right)\right), \mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(m, n\right)\right)\right)\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right)\right)\right), \mathsf{exp.f64}\left(\ell\right)\right)}\right)\right) \]

   3. Taylor expanded in K around 0 99.9%

      \[\leadsto \mathsf{/.f64}\left(\color{blue}{\mathsf{cos.f64}\left(\mathsf{neg.f64}\left(M\right)\right)}, \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]

   4. Simplified 99.9%

      \[\leadsto \mathsf{/.f64}\left(\color{blue}{\mathsf{cos.f64}\left(M\right)}, \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]
      Proof

      [Start] 99.9	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{neg.f64}\left(M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]
      cos-neg [=>] 99.9	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{cos.f64}\left(M\right)}, \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]

   5. Taylor expanded in n around inf 99.0%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{pow.f64}\left(n, 2\right)\right)}\right)\right) \]

   6. Simplified 99.0%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, n\right), n\right)}\right)\right) \]
      Proof

      [Start] 99.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \mathsf{pow.f64}\left(n, 2\right)\right)\right)\right) \]
      unpow2 [=>] 99.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, \color{blue}{\mathsf{*.f64}\left(n, n\right)}\right)\right)\right) \]
      associate-*r* [=>] 99.0	\[ \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\frac{1}{4}, n\right), n\right)}\right)\right) \]

3. Recombined 3 regimes into one program.

4. Final simplification 97.7%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), -500\right):\\ \;\;\;\;\mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{-1}{4}\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), \frac{5902958103587057}{1180591620717411303424}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(K, \mathsf{/.f64}\left(2, \mathsf{+.f64}\left(m, n\right)\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(n, \mathsf{*.f64}\left(n, \frac{1}{4}\right)\right)\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	98.0%
Cost	26624

\[\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right), M\right), 2\right), \mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right)\right)\right)\right) \]

Alternative 2
Accuracy	97.7%
Cost	21192

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_0, -500\right):\\ \;\;\;\;\mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{-1}{4}\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, \frac{5902958103587057}{1180591620717411303424}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(t_0, K\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(n, \mathsf{*.f64}\left(n, \frac{1}{4}\right)\right)\right)\right)\\ \end{array} \]

Alternative 3
Accuracy	97.6%
Cost	21064

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_0, -500\right):\\ \;\;\;\;\mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{-1}{4}\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, \frac{5902958103587057}{1180591620717411303424}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), M\right)\right), \mathsf{exp.f64}\left(\mathsf{+.f64}\left(\mathsf{\_.f64}\left(\ell, \mathsf{fabs.f64}\left(\mathsf{\_.f64}\left(n, m\right)\right)\right), \mathsf{*.f64}\left(M, M\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(n, \mathsf{*.f64}\left(n, \frac{1}{4}\right)\right)\right)\right)\\ \end{array} \]

Alternative 4
Accuracy	91.6%
Cost	14800

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(M, M\right)\right)\right)\\ t_1 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(m, n\right), 2\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -500\right):\\ \;\;\;\;\mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{-1}{4}\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-5758609657015291}{28793048285076456849987446449190283896766061557132266451844835664715760516297522370041860391064901485759493828054533728788532902755163518009654497157537048672862208}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{5339967589802275}{533996758980227520598755426542388028650676130589163192486760401955554931445160137505740521734144}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(t_1, K\right), M\right)\right), \mathsf{exp.f64}\left(\ell\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{5902958103587057}{1180591620717411303424}\right):\\ \;\;\;\;t_0\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(n, \mathsf{*.f64}\left(n, \frac{1}{4}\right)\right)\right)\right)\\ \end{array} \]

Alternative 5
Accuracy	81.6%
Cost	13513

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(M, \frac{-1152921504606847}{4611686018427387904}\right) \lor \neg \mathsf{<=.f64}\left(M, \frac{53}{2}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(M, M\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{1}{4}\right)\right)\right)\right)\\ \end{array} \]

Alternative 6
Accuracy	84.4%
Cost	13512

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(m, -54\right):\\ \;\;\;\;\mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{-1}{4}\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(m, \frac{-2921258960492219}{132784498204191774672397051638117156832398279431757980799861034550100889965213060684790625566307321417222332371561625253836644834413176809852379994691646837985957817708848304757932032}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(M, M\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(n, \mathsf{*.f64}\left(n, \frac{1}{4}\right)\right)\right)\right)\\ \end{array} \]

Alternative 7
Accuracy	81.4%
Cost	13385

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(M, \frac{-944473296573929}{75557863725914323419136}\right) \lor \neg \mathsf{<=.f64}\left(M, \frac{53}{2}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{cos.f64}\left(M\right), \mathsf{exp.f64}\left(\mathsf{*.f64}\left(M, M\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{-1}{4}\right)\right)\right)\\ \end{array} \]

Alternative 8
Accuracy	69.5%
Cost	6852

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\ell, \frac{112986307451471}{2305843009213693952}\right):\\ \;\;\;\;\mathsf{exp.f64}\left(\mathsf{*.f64}\left(m, \mathsf{*.f64}\left(m, \frac{-1}{4}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right)\\ \end{array} \]

Alternative 9
Accuracy	32.1%
Cost	6528

\[\mathsf{exp.f64}\left(\mathsf{neg.f64}\left(\ell\right)\right) \]

Alternative 10
Accuracy	7.3%
Cost	6464

\[\mathsf{cos.f64}\left(M\right) \]

Reproduce

herbie shell --seed 2023144 
(FPCore (K m n M l)
  :name "Maksimov and Kolovsky, Equation (32)"
  :precision binary64
  (* (cos (- (/ (* K (+ m n)) 2.0) M)) (exp (- (- (pow (- (/ (+ m n) 2.0) M) 2.0)) (- l (fabs (- m n)))))))