Maksimov and Kolovsky, Equation (3)

Average Accuracy: 71.8% → 99.9%

Time: 18.6s

Precision: binary64

Cost: 34440

Math

\[\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right) \]

↓

\[\begin{array}{l} t_0 := \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\\ t_1 := \mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_0, -100000000\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_0, 500000\right):\\ \;\;\;\;\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, t_1\right), \mathsf{hypot.f64}\left(1, \mathsf{*.f64}\left(U, \mathsf{/.f64}\left(\mathsf{/.f64}\left(\frac{1}{2}, J\right), t_1\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \end{array} \]

FPCore

(FPCore (J K U)
 :precision binary64
 (*.f64
  (*.f64 (*.f64 -2 J) (cos.f64 (/.f64 K 2)))
  (sqrt.f64
   (+.f64 1 (pow.f64 (/.f64 U (*.f64 (*.f64 2 J) (cos.f64 (/.f64 K 2)))) 2)))))

↓

(FPCore (J K U)
 :precision binary64
 (let* ((t_0 (/.f64 U (*.f64 (*.f64 2 J) (cos.f64 (/.f64 K 2)))))
        (t_1 (cos.f64 (*.f64 K 1/2))))
   (if (<=.f64 t_0 -100000000)
     U
     (if (<=.f64 t_0 500000)
       (*.f64
        J
        (*.f64
         (*.f64 -2 t_1)
         (hypot.f64 1 (*.f64 U (/.f64 (/.f64 1/2 J) t_1)))))
       (neg.f64 U)))))

Derivation

1. Split input into 3 regimes

2. if (/.f64 U (*.f64 (*.f64 2 J) (cos.f64 (/.f64 K 2)))) < -1e8

   1. Initial program 41.1%

      \[\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right) \]

   2. Simplified 73.6%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 41.1	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right) \]
      *-commutative [=>] 41.1	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)} \]
      associate-*l* [=>] 41.1	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(-2, \mathsf{*.f64}\left(J, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)}\right) \]
      associate-*r* [=>] 41.1	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), -2\right), \mathsf{*.f64}\left(J, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)} \]
      *-commutative [=>] 41.1	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(J, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), -2\right)\right)} \]
      associate-*l* [=>] 41.0	\[ \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), -2\right)\right)\right)} \]
      *-commutative [=>] 41.0	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \color{blue}{\mathsf{*.f64}\left(-2, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right)}\right)\right) \]
      unpow2 [=>] 41.0	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)}\right)\right)\right)\right)\right) \]
      hypot-1-def [=>] 73.6	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \color{blue}{\mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)}\right)\right)\right) \]
      *-commutative [=>] 73.6	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(J, 2\right)}, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right) \]
      associate-*l* [=>] 73.6	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)}\right)\right)\right)\right)\right) \]

   3. Taylor expanded in U around -inf 100.0%

      \[\leadsto \color{blue}{U} \]

   if -1e8 < (/.f64 U (*.f64 (*.f64 2 J) (cos.f64 (/.f64 K 2)))) < 5e5

   1. Initial program 99.8%

      \[\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right) \]

   2. Simplified 99.8%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 99.8	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right) \]
      *-commutative [=>] 99.8	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)} \]
      associate-*l* [=>] 99.8	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(-2, \mathsf{*.f64}\left(J, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)}\right) \]
      associate-*r* [=>] 99.8	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), -2\right), \mathsf{*.f64}\left(J, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)} \]
      *-commutative [=>] 99.8	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(J, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), -2\right)\right)} \]
      associate-*l* [=>] 99.8	\[ \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), -2\right)\right)\right)} \]
      *-commutative [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \color{blue}{\mathsf{*.f64}\left(-2, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right)}\right)\right) \]
      unpow2 [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)}\right)\right)\right)\right)\right) \]
      hypot-1-def [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \color{blue}{\mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)}\right)\right)\right) \]
      *-commutative [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(J, 2\right)}, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right) \]
      associate-*l* [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)}\right)\right)\right)\right)\right) \]

   3. Applied egg-rr 99.8%

      \[\leadsto \color{blue}{\mathsf{+.f64}\left(0, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, 2\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), -2\right)\right)\right)\right)} \]
      Proof

      [Start] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right)\right) \]
      add-log-exp [=>] 3.1	\[ \color{blue}{\mathsf{log.f64}\left(\mathsf{exp.f64}\left(\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)} \]
      *-un-lft-identity [=>] 3.1	\[ \mathsf{log.f64}\left(\color{blue}{\mathsf{*.f64}\left(1, \mathsf{exp.f64}\left(\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)}\right) \]
      log-prod [=>] 3.1	\[ \color{blue}{\mathsf{+.f64}\left(\mathsf{log.f64}\left(1\right), \mathsf{log.f64}\left(\mathsf{exp.f64}\left(\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)} \]
      metadata-eval [=>] 3.1	\[ \mathsf{+.f64}\left(\color{blue}{0}, \mathsf{log.f64}\left(\mathsf{exp.f64}\left(\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right) \]
      add-log-exp [<=] 99.8	\[ \mathsf{+.f64}\left(0, \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right)\right)}\right) \]
      associate-*r* [=>] 99.8	\[ \mathsf{+.f64}\left(0, \mathsf{*.f64}\left(J, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), -2\right), \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)}\right)\right) \]
      *-commutative [=>] 99.8	\[ \mathsf{+.f64}\left(0, \mathsf{*.f64}\left(J, \color{blue}{\mathsf{*.f64}\left(\mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), -2\right)\right)}\right)\right) \]

   4. Simplified 99.8%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{*.f64}\left(U, \mathsf{/.f64}\left(\mathsf{/.f64}\left(\frac{1}{2}, J\right), \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 99.8	\[ \mathsf{+.f64}\left(0, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, 2\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), -2\right)\right)\right)\right) \]
      +-lft-identity [=>] 99.8	\[ \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, 2\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), -2\right)\right)\right)} \]
      *-commutative [=>] 99.8	\[ \mathsf{*.f64}\left(J, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), -2\right), \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, 2\right)\right)\right)\right)\right)}\right) \]
      *-commutative [<=] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\color{blue}{\mathsf{*.f64}\left(\frac{1}{2}, K\right)}\right), -2\right), \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, 2\right)\right)\right)\right)\right)\right) \]
      *-commutative [<=] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right)}, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, 2\right)\right)\right)\right)\right)\right) \]
      *-rgt-identity [<=] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(U, 1\right)}, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, 2\right)\right)\right)\right)\right)\right) \]
      associate-*r/ [<=] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right), \mathsf{hypot.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(U, \mathsf{/.f64}\left(1, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, 2\right)\right)\right)\right)}\right)\right)\right) \]
      *-commutative [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{*.f64}\left(U, \mathsf{/.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(J, 2\right), \mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right)\right)}\right)\right)\right)\right)\right) \]
      associate-/r* [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{*.f64}\left(U, \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \mathsf{*.f64}\left(J, 2\right)\right), \mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right)\right)}\right)\right)\right)\right) \]
      *-commutative [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{*.f64}\left(U, \mathsf{/.f64}\left(\mathsf{/.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(2, J\right)}\right), \mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right)\right)\right)\right)\right)\right) \]
      associate-/r* [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{*.f64}\left(U, \mathsf{/.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(1, 2\right), J\right)}, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right)\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{*.f64}\left(U, \mathsf{/.f64}\left(\mathsf{/.f64}\left(\color{blue}{\frac{1}{2}}, J\right), \mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right)\right)\right)\right)\right)\right) \]
      *-commutative [<=] 99.8	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(\frac{1}{2}, K\right)\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{*.f64}\left(U, \mathsf{/.f64}\left(\mathsf{/.f64}\left(\frac{1}{2}, J\right), \mathsf{cos.f64}\left(\color{blue}{\mathsf{*.f64}\left(\frac{1}{2}, K\right)}\right)\right)\right)\right)\right)\right) \]

   if 5e5 < (/.f64 U (*.f64 (*.f64 2 J) (cos.f64 (/.f64 K 2))))

   1. Initial program 43.8%

      \[\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right) \]

   2. Simplified 74.5%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 43.8	\[ \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right) \]
      *-commutative [=>] 43.8	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)} \]
      associate-*l* [=>] 43.8	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(-2, \mathsf{*.f64}\left(J, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)}\right) \]
      associate-*r* [=>] 43.8	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), -2\right), \mathsf{*.f64}\left(J, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)} \]
      *-commutative [=>] 43.8	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(J, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), -2\right)\right)} \]
      associate-*l* [=>] 43.7	\[ \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right), -2\right)\right)\right)} \]
      *-commutative [=>] 43.7	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \color{blue}{\mathsf{*.f64}\left(-2, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{pow.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 2\right)\right)\right)\right)}\right)\right) \]
      unpow2 [=>] 43.7	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)}\right)\right)\right)\right)\right) \]
      hypot-1-def [=>] 74.5	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \color{blue}{\mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)}\right)\right)\right) \]
      *-commutative [=>] 74.5	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(J, 2\right)}, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)\right)\right)\right)\right) \]
      associate-*l* [=>] 74.5	\[ \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \color{blue}{\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right)}\right)\right)\right)\right)\right) \]

   3. Taylor expanded in J around 0 99.9%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(-1, U\right)} \]

   4. Simplified 99.9%

      \[\leadsto \color{blue}{\mathsf{neg.f64}\left(U\right)} \]
      Proof

      [Start] 99.9	\[ \mathsf{*.f64}\left(-1, U\right) \]
      neg-mul-1 [<=] 99.9	\[ \color{blue}{\mathsf{neg.f64}\left(U\right)} \]

3. Recombined 3 regimes into one program.

4. Final simplification 99.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), -100000000\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{/.f64}\left(U, \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, J\right), \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\right)\right), 500000\right):\\ \;\;\;\;\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{*.f64}\left(-2, \mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{*.f64}\left(U, \mathsf{/.f64}\left(\mathsf{/.f64}\left(\frac{1}{2}, J\right), \mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	86.4%
Cost	20873

\[\begin{array}{l} t_0 := \mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{5357543035931337}{10715086071862673209484250490600018105614048117055336074437503883703510511249361224931983788156958581275946729175531468251871452856923140435984577574698574803934567774824230985421074605062371141877954182153046474983581941267398767559165543946077062914571196477686542167660429831652624386837205668069376}\right) \lor \neg \mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{6575169876935467}{657516987693546688405123735360016083193792475352896732437285112883591519287135102764208317034698556403372871107022277214127429031272975482890976846331485106244402958891055574773957969735540339658911656466972672}\right):\\ \;\;\;\;\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(t_0, \mathsf{*.f64}\left(-2, \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(U, \mathsf{*.f64}\left(J, \mathsf{*.f64}\left(2, t_0\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;U\\ \end{array} \]

Alternative 2
Accuracy	73.9%
Cost	14736

\[\begin{array}{l} t_0 := \mathsf{*.f64}\left(\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{/.f64}\left(K, 2\right)\right), -2\right)\right), \mathsf{hypot.f64}\left(1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(U, \frac{1}{2}\right), J\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{-7229475734293037}{361473786714651839609485931802192366508973300717001923159475447150424810286233407987951861887389439612274926783780351561999781998832434041296198795326329101623141899709787663433296905279066051548640942013290819886814068736}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{-432778879906337}{2163894399531684849059183759018052020301198647443953754636127064173256304872345024407213080115843841616586321892381199068702095603722999960578207655784200507016751857659924824755124296402642702553187257992033027703390323887110396882282073697349781407701150027357134841184256}\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{6762169998536515}{67621699985365151533099492469314125634412457732623554832378970755414259527260782012725408753620120050518322559136912470896940487616343748768068989243256265844273495551872650773597634262582584454787101812251032115730947621472199902571314803042180668990660938354910463787008}\right):\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{6575169876935467}{657516987693546688405123735360016083193792475352896732437285112883591519287135102764208317034698556403372871107022277214127429031272975482890976846331485106244402958891055574773957969735540339658911656466972672}\right):\\ \;\;\;\;U\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]

Alternative 3
Accuracy	58.9%
Cost	8020

\[\begin{array}{l} t_0 := \mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, -2\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(U, -23000000000000000039094667870871330424849891269091839649409202752664010702959929149394298238184861349226433749739341598515796195575219268426292089202997231609145957392486736718001283393211189489905204306378752\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, -244999999999999998119694821822431832520529245022698039763029875988138224832832669661501938270569819315312163562517728390837869291270585206382861540768373291221238926892758656360644608\right):\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, -230000000000000012780930231873428186770625938965526796539758599638312011047756831731003125032436136698199092760180171233820672\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, \frac{4594630100936707}{7410693711188236507108543040556026102609279018600996098525285376506440296955904}\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, 24999999999999999215841526979493888\right):\\ \;\;\;\;\mathsf{*.f64}\left(J, \mathsf{*.f64}\left(-2, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{1}{4}, \mathsf{/.f64}\left(\mathsf{*.f64}\left(U, U\right), \mathsf{*.f64}\left(J, J\right)\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, 6600000000000000014920287529321888588708311938418057440338597436998962995265536\right):\\ \;\;\;\;t_0\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, 270000000000000003929391025715019224601693582464301584227702321858631828952131248700324821562364378612752735134113527182066249497434631042182803239906829412958266892098259177578442570640250350327092477952\right):\\ \;\;\;\;U\\ \mathbf{else}:\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \end{array} \]

Alternative 4
Accuracy	59.5%
Cost	7376

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(U, -1039999999999999954903559072715763619037699785789638596928710261969490762249743215724622257159227097442329975043474872380529669853763013565788577493311734512448719952339700183138590996144654026627060198277120\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, -430000000000000015954782875145193380758248169775903145894915804879387641421942543924391985496045254747929129812065643407737765647759827605950454081373025738477247154509209293048250368\right):\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, -59999999999999999249733829577706087175849207053029551487445636586829445130213136047724249809142568767010200920449256788066304\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, 24499999999999998287928129114365253028339294519576413216993272634544044375395864150016\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{cos.f64}\left(\mathsf{*.f64}\left(K, \frac{1}{2}\right)\right), \mathsf{*.f64}\left(J, -2\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(U, 1700000000000000050524802382086897769507591226347516612301988369746025677697693818558821246163636887675668145995578849365847568843588929185412778527122867890435236971320201264005694826600339244624904192000\right):\\ \;\;\;\;U\\ \mathbf{else}:\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \end{array} \]

Alternative 5
Accuracy	40.9%
Cost	1752

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), -1000000000000000042420637374017961984\right):\\ \;\;\;\;\mathsf{*.f64}\left(J, -2\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{-578960446186581}{115792089237316195423570985008687907853269984665640564039457584007913129639936}\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{-5814709794364855}{11629419588729710248789180926208072549658261770997088964503843186890228609814366773219056811420217048972200345700258846936553626057834496}\right):\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{-432778879906337}{2163894399531684849059183759018052020301198647443953754636127064173256304872345024407213080115843841616586321892381199068702095603722999960578207655784200507016751857659924824755124296402642702553187257992033027703390323887110396882282073697349781407701150027357134841184256}\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), \frac{6762169998536515}{67621699985365151533099492469314125634412457732623554832378970755414259527260782012725408753620120050518322559136912470896940487616343748768068989243256265844273495551872650773597634262582584454787101812251032115730947621472199902571314803042180668990660938354910463787008}\right):\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(J, -2\right), 40\right):\\ \;\;\;\;U\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(J, -2\right)\\ \end{array} \]

Alternative 6
Accuracy	27.1%
Cost	1052

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(K, -255000000000000006537617905273964331008\right):\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(K, \frac{-4886469533914257}{4249103942534136789516705652419749018636744941816255385595553105603228478886817941913300018121834285351114635889972008122772634701221657915276159830132698815550650166683145752253825024}\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(K, \frac{-9501681161115}{2436328502849999770088345596968797077719056714398751881716976614303237172691606525616403766470502564806326229057852167045864792466300773511644496824078163354882819424989118257467697413872513412088199898369804594718421399481348718736436590903867241403206934700776069386770457147497978527744}\right):\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(K, \frac{7443573136539277}{1404447761611184302913519680303925573139044514798677009948672509044786529730476274474284979081308875165000889686495260606709295068862629863225370551870891596701311667381761603721111090634735110308227210563164107569048052205800491261514946176100212790338675864723330454999587858894372783631526221325189251072}\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(K, \frac{2370006831801635}{43091033305484275771318189120554014028188383664727440257009917157939053808001686094755156265186004592451444480869811959505055188993505721246743058601180207922833192313884218148386109504588371699886434318219521032192}\right):\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(K, 180000000000000001732756623736176640\right):\\ \;\;\;\;U\\ \mathbf{elif}\;\mathsf{<=.f64}\left(K, 2150000000000000006417121567444103489895891892130738630399825147842228118119626382588998844416000\right):\\ \;\;\;\;\mathsf{neg.f64}\left(U\right)\\ \mathbf{else}:\\ \;\;\;\;U\\ \end{array} \]

Alternative 7
Accuracy	26.5%
Cost	64

\[U \]

Reproduce

herbie shell --seed 2023144 
(FPCore (J K U)
  :name "Maksimov and Kolovsky, Equation (3)"
  :precision binary64
  (* (* (* -2.0 J) (cos (/ K 2.0))) (sqrt (+ 1.0 (pow (/ U (* (* 2.0 J) (cos (/ K 2.0)))) 2.0)))))