Jmat.Real.dawson

Average Accuracy: 54.5% → 99.8%

Time: 9.9s

Precision: binary64

Cost: 94724

Math

\[\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{106015151}{2500000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{36322091}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1789971}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{7715471019}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{2909738639}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{694555761}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{70002721}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1665589}{2000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, \frac{1789971}{10000000000}\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right), x\right) \]

↓

\[\begin{array}{l} t_0 := \mathsf{pow.f64}\left(\mathsf{*.f64}\left(x, x\right), 4\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right), 2000000000000000084841274748035923968\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(t_0, \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \frac{1665589}{2000000000}\right)\right), \frac{70002721}{5000000000}\right)\right), \mathsf{fma.f64}\left(\frac{1789971}{5000000000}, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(x, x\right), 6\right), \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(x, 4\right), \frac{2909738639}{10000000000}, \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(x, 6\right), \frac{694555761}{10000000000}, \mathsf{fma.f64}\left(x, \mathsf{*.f64}\left(x, \frac{7715471019}{10000000000}\right), 1\right)\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{fma.f64}\left(\frac{106015151}{2500000000}, \mathsf{pow.f64}\left(x, 4\right), \mathsf{fma.f64}\left(\frac{36322091}{5000000000}, \mathsf{pow.f64}\left(x, 6\right), \mathsf{fma.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right), 1\right)\right)\right), \mathsf{*.f64}\left(t_0, \mathsf{+.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \frac{1789971}{10000000000}\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\frac{1}{2}, x\right)\\ \end{array} \]

FPCore

(FPCore (x)
 :precision binary64
 (*.f64
  (/.f64
   (+.f64
    (+.f64
     (+.f64
      (+.f64
       (+.f64 1 (*.f64 1049934947/10000000000 (*.f64 x x)))
       (*.f64 106015151/2500000000 (*.f64 (*.f64 x x) (*.f64 x x))))
      (*.f64
       36322091/5000000000
       (*.f64 (*.f64 (*.f64 x x) (*.f64 x x)) (*.f64 x x))))
     (*.f64
      2532017/5000000000
      (*.f64 (*.f64 (*.f64 (*.f64 x x) (*.f64 x x)) (*.f64 x x)) (*.f64 x x))))
    (*.f64
     1789971/10000000000
     (*.f64
      (*.f64 (*.f64 (*.f64 (*.f64 x x) (*.f64 x x)) (*.f64 x x)) (*.f64 x x))
      (*.f64 x x))))
   (+.f64
    (+.f64
     (+.f64
      (+.f64
       (+.f64
        (+.f64 1 (*.f64 7715471019/10000000000 (*.f64 x x)))
        (*.f64 2909738639/10000000000 (*.f64 (*.f64 x x) (*.f64 x x))))
       (*.f64
        694555761/10000000000
        (*.f64 (*.f64 (*.f64 x x) (*.f64 x x)) (*.f64 x x))))
      (*.f64
       70002721/5000000000
       (*.f64
        (*.f64 (*.f64 (*.f64 x x) (*.f64 x x)) (*.f64 x x))
        (*.f64 x x))))
     (*.f64
      1665589/2000000000
      (*.f64
       (*.f64 (*.f64 (*.f64 (*.f64 x x) (*.f64 x x)) (*.f64 x x)) (*.f64 x x))
       (*.f64 x x))))
    (*.f64
     (*.f64 2 1789971/10000000000)
     (*.f64
      (*.f64
       (*.f64 (*.f64 (*.f64 (*.f64 x x) (*.f64 x x)) (*.f64 x x)) (*.f64 x x))
       (*.f64 x x))
      (*.f64 x x)))))
  x))

↓

(FPCore (x)
 :precision binary64
 (let* ((t_0 (pow.f64 (*.f64 x x) 4)))
   (if (<=.f64
        (*.f64
         (*.f64 x x)
         (*.f64
          (*.f64 x x)
          (*.f64
           (*.f64 x x)
           (*.f64 (*.f64 x x) (*.f64 (*.f64 x x) (*.f64 x x))))))
        2000000000000000084841274748035923968)
     (/.f64
      x
      (/.f64
       (+.f64
        (*.f64
         t_0
         (+.f64 (*.f64 x (*.f64 x 1665589/2000000000)) 70002721/5000000000))
        (fma.f64
         1789971/5000000000
         (pow.f64 (*.f64 x x) 6)
         (fma.f64
          (pow.f64 x 4)
          2909738639/10000000000
          (fma.f64
           (pow.f64 x 6)
           694555761/10000000000
           (fma.f64 x (*.f64 x 7715471019/10000000000) 1)))))
       (+.f64
        (fma.f64
         106015151/2500000000
         (pow.f64 x 4)
         (fma.f64
          36322091/5000000000
          (pow.f64 x 6)
          (fma.f64 1049934947/10000000000 (*.f64 x x) 1)))
        (*.f64
         t_0
         (+.f64 2532017/5000000000 (*.f64 (*.f64 x x) 1789971/10000000000))))))
     (/.f64 1/2 x))))

Derivation

1. Split input into 2 regimes

2. if (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 x x) (*.f64 x x)) (*.f64 x x)) (*.f64 x x)) (*.f64 x x)) (*.f64 x x)) < 2.00000000000000008e36

   1. Initial program 100.0%

      \[\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{106015151}{2500000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{36322091}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1789971}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{7715471019}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{2909738639}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{694555761}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{70002721}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1665589}{2000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, \frac{1789971}{10000000000}\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right), x\right) \]

   2. Simplified 100.0%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(x, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(x, x\right), 4\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \frac{1665589}{2000000000}\right)\right), \frac{70002721}{5000000000}\right)\right), \mathsf{fma.f64}\left(\frac{1789971}{5000000000}, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(x, x\right), 6\right), \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(x, 4\right), \frac{2909738639}{10000000000}, \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(x, 6\right), \frac{694555761}{10000000000}, \mathsf{fma.f64}\left(x, \mathsf{*.f64}\left(x, \frac{7715471019}{10000000000}\right), 1\right)\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{fma.f64}\left(\frac{106015151}{2500000000}, \mathsf{pow.f64}\left(x, 4\right), \mathsf{fma.f64}\left(\frac{36322091}{5000000000}, \mathsf{pow.f64}\left(x, 6\right), \mathsf{fma.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right), 1\right)\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(x, x\right), 4\right), \mathsf{+.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \frac{1789971}{10000000000}\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 100.0

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{106015151}{2500000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{36322091}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1789971}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{7715471019}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{2909738639}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{694555761}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{70002721}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1665589}{2000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, \frac{1789971}{10000000000}\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right), x\right) \]

      *-commutative [=>] 100.0

      \[ \color{blue}{\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{106015151}{2500000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{36322091}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1789971}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{7715471019}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{2909738639}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{694555761}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{70002721}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1665589}{2000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, \frac{1789971}{10000000000}\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right)} \]

   if 2.00000000000000008e36 < (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 (*.f64 x x) (*.f64 x x)) (*.f64 x x)) (*.f64 x x)) (*.f64 x x)) (*.f64 x x))

   1. Initial program 7.5%

      \[\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{106015151}{2500000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{36322091}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1789971}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{7715471019}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{2909738639}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{694555761}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{70002721}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1665589}{2000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, \frac{1789971}{10000000000}\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right), x\right) \]

   2. Simplified 7.5%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{106015151}{2500000000}, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{36322091}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1789971}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \frac{7715471019}{10000000000}\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right), \frac{2909738639}{10000000000}\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \frac{694555761}{10000000000}\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \frac{70002721}{5000000000}\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right), \frac{1665589}{2000000000}\right), \mathsf{*.f64}\left(\frac{1789971}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 7.5

      \[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{106015151}{2500000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{36322091}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1789971}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{7715471019}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{2909738639}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{694555761}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{70002721}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1665589}{2000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, \frac{1789971}{10000000000}\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right), x\right) \]

      *-commutative [=>] 7.5

      \[ \color{blue}{\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{106015151}{2500000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{36322091}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1789971}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\frac{7715471019}{10000000000}, \mathsf{*.f64}\left(x, x\right)\right)\right), \mathsf{*.f64}\left(\frac{2909738639}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{694555761}{10000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{70002721}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\frac{1665589}{2000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(2, \frac{1789971}{10000000000}\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right)} \]

   3. Taylor expanded in x around inf 99.7%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\frac{1}{2}, x\right)} \]
3. Recombined 2 regimes into one program.

4. Final simplification 99.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right), 2000000000000000084841274748035923968\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(x, x\right), 4\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \frac{1665589}{2000000000}\right)\right), \frac{70002721}{5000000000}\right)\right), \mathsf{fma.f64}\left(\frac{1789971}{5000000000}, \mathsf{pow.f64}\left(\mathsf{*.f64}\left(x, x\right), 6\right), \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(x, 4\right), \frac{2909738639}{10000000000}, \mathsf{fma.f64}\left(\mathsf{pow.f64}\left(x, 6\right), \frac{694555761}{10000000000}, \mathsf{fma.f64}\left(x, \mathsf{*.f64}\left(x, \frac{7715471019}{10000000000}\right), 1\right)\right)\right)\right)\right), \mathsf{+.f64}\left(\mathsf{fma.f64}\left(\frac{106015151}{2500000000}, \mathsf{pow.f64}\left(x, 4\right), \mathsf{fma.f64}\left(\frac{36322091}{5000000000}, \mathsf{pow.f64}\left(x, 6\right), \mathsf{fma.f64}\left(\frac{1049934947}{10000000000}, \mathsf{*.f64}\left(x, x\right), 1\right)\right)\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(\mathsf{*.f64}\left(x, x\right), 4\right), \mathsf{+.f64}\left(\frac{2532017}{5000000000}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \frac{1789971}{10000000000}\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\frac{1}{2}, x\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	99.8%
Cost	12484

\[\begin{array}{l} t_0 := \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, \mathsf{*.f64}\left(x, x\right)\right)\right)\\ t_1 := \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), t_0\right)\\ t_2 := \mathsf{*.f64}\left(t_0, t_0\right)\\ t_3 := \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), t_2\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\right)\right), 2000000000000000084841274748035923968\right):\\ \;\;\;\;\mathsf{*.f64}\left(x, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \frac{1049934947}{10000000000}\right)\right), \mathsf{*.f64}\left(\frac{106015151}{2500000000}, t_0\right)\right), \mathsf{*.f64}\left(\frac{36322091}{5000000000}, t_1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{2532017}{5000000000}, t_2\right), \mathsf{*.f64}\left(\frac{1789971}{10000000000}, t_3\right)\right)\right), \mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \frac{7715471019}{10000000000}\right)\right), \mathsf{*.f64}\left(\frac{2909738639}{10000000000}, t_0\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{694555761}{10000000000}, t_1\right), \mathsf{*.f64}\left(\frac{70002721}{5000000000}, t_2\right)\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\frac{1665589}{2000000000}, t_3\right), \mathsf{*.f64}\left(\frac{1789971}{5000000000}, \mathsf{*.f64}\left(t_0, t_2\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\frac{1}{2}, x\right)\\ \end{array} \]

Alternative 2
Accuracy	99.3%
Cost	836

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(x, x\right), \frac{7378697629483821}{36893488147419103232}\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, \mathsf{+.f64}\left(1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(x, x\right), \frac{833192009}{1250000000}\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\frac{1}{2}, x\right)\\ \end{array} \]

Alternative 3
Accuracy	99.1%
Cost	456

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(x, \frac{-3152519739159347}{4503599627370496}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\frac{1}{2}, x\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(x, \frac{3152519739159347}{4503599627370496}\right):\\ \;\;\;\;x\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\frac{1}{2}, x\right)\\ \end{array} \]

Alternative 4
Accuracy	51.7%
Cost	64

\[x \]

Reproduce

herbie shell --seed 2023144 
(FPCore (x)
  :name "Jmat.Real.dawson"
  :precision binary64
  (* (/ (+ (+ (+ (+ (+ 1.0 (* 0.1049934947 (* x x))) (* 0.0424060604 (* (* x x) (* x x)))) (* 0.0072644182 (* (* (* x x) (* x x)) (* x x)))) (* 0.0005064034 (* (* (* (* x x) (* x x)) (* x x)) (* x x)))) (* 0.0001789971 (* (* (* (* (* x x) (* x x)) (* x x)) (* x x)) (* x x)))) (+ (+ (+ (+ (+ (+ 1.0 (* 0.7715471019 (* x x))) (* 0.2909738639 (* (* x x) (* x x)))) (* 0.0694555761 (* (* (* x x) (* x x)) (* x x)))) (* 0.0140005442 (* (* (* (* x x) (* x x)) (* x x)) (* x x)))) (* 0.0008327945 (* (* (* (* (* x x) (* x x)) (* x x)) (* x x)) (* x x)))) (* (* 2.0 0.0001789971) (* (* (* (* (* (* x x) (* x x)) (* x x)) (* x x)) (* x x)) (* x x))))) x))