Toniolo and Linder, Equation (7)

Average Accuracy: 33.0% → 80.3%

Time: 2.0min

Precision: binary64

Cost: 60892

Math

\[\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]

↓

\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right)\\ t_2 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), 0\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right)\right)\right)\right)\right)\right)\\ t_3 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ t_4 := \mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_3\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -399999999999999966445568\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_3\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-4763410263543689}{95268205270873786358080970147496530326800480428008152797215483387004752771599292606210513399154418065180265231976520474104247304665780191232}\right):\\ \;\;\;\;t_2\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;-1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{/.f64}\left(2, x\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{7229475734293037}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right):\\ \;\;\;\;t_4\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{5363123171977039}{107262463439540776796592199985646769019834926564739147021788491549774112240588375814414994385335227421520254865491888406830031062495572559571469192048672768}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\ell, \mathsf{/.f64}\left(x, \ell\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, 4000000000000000053150220288\right):\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;t_4\\ \end{array} \]

FPCore

(FPCore (x l t)
 :precision binary64
 (/.f64
  (*.f64 (sqrt.f64 2) t)
  (sqrt.f64
   (-.f64
    (*.f64
     (/.f64 (+.f64 x 1) (-.f64 x 1))
     (+.f64 (*.f64 l l) (*.f64 2 (*.f64 t t))))
    (*.f64 l l)))))

↓

(FPCore (x l t)
 :precision binary64
 (let* ((t_1 (*.f64 (sqrt.f64 2) t))
        (t_2
         (*.f64
          (sqrt.f64 2)
          (/.f64
           t
           (sqrt.f64
            (+.f64
             (+.f64 (*.f64 2 (*.f64 t t)) (*.f64 (*.f64 l l) 0))
             (*.f64 2 (/.f64 (*.f64 l l) x)))))))
        (t_3 (/.f64 (+.f64 1 x) (+.f64 x -1)))
        (t_4 (/.f64 1 (sqrt.f64 t_3))))
   (if (<=.f64 t_1 -399999999999999966445568)
     (neg.f64 (sqrt.f64 (/.f64 1 t_3)))
     (if (<=.f64
          t_1
          -4763410263543689/95268205270873786358080970147496530326800480428008152797215483387004752771599292606210513399154418065180265231976520474104247304665780191232)
       t_2
       (if (<=.f64
            t_1
            -8618206661096855/172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768)
         -1
         (if (<=.f64
              t_1
              75075168288047/7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624)
           (*.f64 t (sqrt.f64 (/.f64 2 (*.f64 (*.f64 l l) (/.f64 2 x)))))
           (if (<=.f64
                t_1
                7229475734293037/180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368)
             t_4
             (if (<=.f64
                  t_1
                  5363123171977039/107262463439540776796592199985646769019834926564739147021788491549774112240588375814414994385335227421520254865491888406830031062495572559571469192048672768)
               (*.f64
                (sqrt.f64 2)
                (/.f64 t (sqrt.f64 (*.f64 2 (/.f64 l (/.f64 x l))))))
               (if (<=.f64 t_1 4000000000000000053150220288) t_2 t_4)))))))))

Derivation

1. Split input into 6 regimes

2. if (*.f64 (sqrt.f64 2) t) < -3.9999999999999997e23

   1. Initial program 31.5%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]

   2. Simplified 31.5%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \mathsf{fma.f64}\left(\ell, \ell, \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right)} \]
      Proof

      [Start] 31.5	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]
      associate-/l* [=>] 31.5	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right)} \]
      fma-neg [=>] 31.5	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)}\right), t\right)\right) \]
      remove-double-neg [<=] 31.5	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right), t\right)\right) \]
      fma-neg [<=] 31.5	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}\right), t\right)\right) \]
      sub-neg [=>] 31.5	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(1\right)\right)}\right), \mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]
      metadata-eval [=>] 31.5	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, \color{blue}{-1}\right)\right), \mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]
      remove-double-neg [=>] 31.5	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)}\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]
      fma-def [=>] 31.5	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{fma.f64}\left(\ell, \ell, \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)}\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]

   3. Taylor expanded in t around -inf 92.2%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right)\right)\right)}\right) \]

   4. Simplified 92.2%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)}\right) \]
      Proof

      [Start] 92.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right)\right)\right)\right) \]
      mul-1-neg [=>] 92.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right)\right)\right)}\right) \]
      *-commutative [=>] 92.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right), \mathsf{sqrt.f64}\left(2\right)\right)}\right)\right) \]
      distribute-rgt-neg-in [=>] 92.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)}\right) \]
      +-commutative [=>] 92.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(x, 1\right)}, \mathsf{\_.f64}\left(x, 1\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      sub-neg [=>] 92.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(1\right)\right)}\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      metadata-eval [=>] 92.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, \color{blue}{-1}\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      +-commutative [=>] 92.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(-1, x\right)}\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]

   5. Applied egg-rr 92.2%

      \[\leadsto \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(0, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), 2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), 2\right)\right)\right)\right)} \]
      Proof

      [Start] 92.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      frac-2neg [=>] 92.2	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)} \]
      neg-sub0 [=>] 92.2	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{sqrt.f64}\left(2\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right) \]
      metadata-eval [<=] 92.2	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\color{blue}{\mathsf{log.f64}\left(1\right)}, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right) \]
      div-sub [=>] 92.2	\[ \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{log.f64}\left(1\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)\right)} \]
      metadata-eval [=>] 92.2	\[ \mathsf{\_.f64}\left(\mathsf{/.f64}\left(\color{blue}{0}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)\right) \]
      distribute-rgt-neg-out [=>] 92.2	\[ \mathsf{\_.f64}\left(\mathsf{/.f64}\left(0, \mathsf{neg.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{sqrt.f64}\left(2\right)\right)\right)}\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)\right) \]
      remove-double-neg [=>] 92.2	\[ \mathsf{\_.f64}\left(\mathsf{/.f64}\left(0, \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{sqrt.f64}\left(2\right)\right)}\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)\right) \]
      sqrt-unprod [=>] 92.2	\[ \mathsf{\_.f64}\left(\mathsf{/.f64}\left(0, \color{blue}{\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right), 2\right)\right)}\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)\right) \]
      +-commutative [=>] 92.2	\[ \mathsf{\_.f64}\left(\mathsf{/.f64}\left(0, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, -1\right)}\right), 2\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)\right) \]

   6. Simplified 92.2%

      \[\leadsto \color{blue}{\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 92.2	\[ \mathsf{\_.f64}\left(\mathsf{/.f64}\left(0, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), 2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), 2\right)\right)\right)\right) \]
      div0 [=>] 92.2	\[ \mathsf{\_.f64}\left(\color{blue}{0}, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), 2\right)\right)\right)\right) \]
      neg-sub0 [<=] 92.2	\[ \color{blue}{\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), 2\right)\right)\right)\right)} \]
      *-commutative [=>] 92.2	\[ \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \color{blue}{\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)}\right)\right)\right) \]
      associate-/r* [=>] 92.2	\[ \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(2, 2\right), \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)}\right)\right) \]
      metadata-eval [=>] 92.2	\[ \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\color{blue}{1}, \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right)\right) \]
      +-commutative [=>] 92.2	\[ \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(-1, x\right)}\right)\right)\right)\right) \]

   if -3.9999999999999997e23 < (*.f64 (sqrt.f64 2) t) < -4.99999999999999967e-125 or 5.00000000000000015e-140 < (*.f64 (sqrt.f64 2) t) < 4.0000000000000001e27

   1. Initial program 57.2%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]

   2. Simplified 57.1%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{neg.f64}\left(\ell\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 57.2	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]
      associate-*r/ [<=] 57.1	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)} \]
      fma-neg [=>] 57.1	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)}\right)\right)\right) \]
      sub-neg [=>] 57.1	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(1\right)\right)}\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 57.1	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, \color{blue}{-1}\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)\right) \]
      +-commutative [=>] 57.1	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)\right) \]
      fma-def [=>] 57.1	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)\right) \]
      distribute-rgt-neg-in [=>] 57.1	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), \color{blue}{\mathsf{*.f64}\left(\ell, \mathsf{neg.f64}\left(\ell\right)\right)}\right)\right)\right)\right) \]

   3. Taylor expanded in x around inf 56.3%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right)\right)\right)}\right)\right)\right) \]

   4. Simplified 81.9%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(0, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), x\right)\right)\right)}\right)\right)\right) \]
      Proof

      [Start] 56.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right)\right)\right)\right)\right)\right) \]
      unpow2 [=>] 56.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\ell, \ell\right)}, \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right)\right)\right)\right)\right)\right) \]
      +-commutative [=>] 56.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)}\right)\right)\right)\right) \]
      associate-+r+ [=>] 67.8	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)}\right)\right)\right) \]
      +-commutative [<=] 67.8	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right)}\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      associate-+r+ [=>] 81.8	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right)}, \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      unpow2 [=>] 81.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(-1, \color{blue}{\mathsf{*.f64}\left(\ell, \ell\right)}\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      distribute-rgt1-in [=>] 81.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(-1, 1\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}, \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 81.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\color{blue}{0}, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      unpow2 [=>] 81.9	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(0, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \color{blue}{\mathsf{*.f64}\left(t, t\right)}\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]

   5. Taylor expanded in t around 0 81.3%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(0, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{*.f64}\left(2, \color{blue}{\mathsf{/.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), x\right)}\right)\right)\right)\right)\right) \]

   6. Simplified 81.3%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(0, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{*.f64}\left(2, \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right)}\right)\right)\right)\right)\right) \]
      Proof

      [Start] 81.3

      \[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(0, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), x\right)\right)\right)\right)\right)\right) \]

      unpow2 [=>] 81.3

      \[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(0, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\ell, \ell\right)}, x\right)\right)\right)\right)\right)\right) \]

   if -4.99999999999999967e-125 < (*.f64 (sqrt.f64 2) t) < -4.99999999999999991e-200

   1. Initial program 20.1%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]

   2. Simplified 20.0%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \mathsf{fma.f64}\left(\ell, \ell, \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right)} \]
      Proof

      [Start] 20.1	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]
      associate-/l* [=>] 20.0	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right)} \]
      fma-neg [=>] 20.0	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)}\right), t\right)\right) \]
      remove-double-neg [<=] 20.0	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right), t\right)\right) \]
      fma-neg [<=] 20.0	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}\right), t\right)\right) \]
      sub-neg [=>] 20.0	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(1\right)\right)}\right), \mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]
      metadata-eval [=>] 20.0	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, \color{blue}{-1}\right)\right), \mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]
      remove-double-neg [=>] 20.0	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)}\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]
      fma-def [=>] 20.0	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{fma.f64}\left(\ell, \ell, \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)}\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]

   3. Taylor expanded in t around -inf 53.2%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right)\right)\right)}\right) \]

   4. Simplified 53.2%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)}\right) \]
      Proof

      [Start] 53.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right)\right)\right)\right) \]
      mul-1-neg [=>] 53.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right)\right)\right)}\right) \]
      *-commutative [=>] 53.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right), \mathsf{sqrt.f64}\left(2\right)\right)}\right)\right) \]
      distribute-rgt-neg-in [=>] 53.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)}\right) \]
      +-commutative [=>] 53.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(x, 1\right)}, \mathsf{\_.f64}\left(x, 1\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      sub-neg [=>] 53.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(1\right)\right)}\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      metadata-eval [=>] 53.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, \color{blue}{-1}\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      +-commutative [=>] 53.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(-1, x\right)}\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]

   5. Taylor expanded in x around inf 52.7%

      \[\leadsto \color{blue}{-1} \]

   if -4.99999999999999991e-200 < (*.f64 (sqrt.f64 2) t) < 1e-242

   1. Initial program 1.7%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]

   2. Simplified 1.7%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right), t\right)} \]
      Proof

      [Start] 1.7

      \[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]

      associate-*l/ [<=] 1.7

      \[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right), t\right)} \]

   3. Taylor expanded in x around inf 49.9%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), x\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(t, 2\right), x\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)}\right)\right), t\right) \]

   4. Simplified 49.9%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right), \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), x\right)\right)\right)\right)}\right)\right), t\right) \]
      Proof

      [Start] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), x\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(t, 2\right), x\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right), t\right) \]
      associate--l+ [=>] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), x\right), \mathsf{\_.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(t, 2\right), x\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)}\right)\right), t\right) \]
      unpow2 [=>] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\ell, \ell\right)}, x\right), \mathsf{\_.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(t, 2\right), x\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right), t\right) \]
      distribute-lft-out [=>] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{pow.f64}\left(t, 2\right), x\right), \mathsf{pow.f64}\left(t, 2\right)\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right), t\right) \]
      unpow2 [=>] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(t, t\right)}, x\right), \mathsf{pow.f64}\left(t, 2\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right), t\right) \]
      unpow2 [=>] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right), \color{blue}{\mathsf{*.f64}\left(t, t\right)}\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right), t\right) \]
      mul-1-neg [=>] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right), \mathsf{*.f64}\left(t, t\right)\right)\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)}\right)\right)\right)\right), t\right) \]
      unpow2 [=>] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right), \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\ell, \ell\right)}, \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right), t\right) \]
      +-commutative [=>] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right), \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}, x\right)\right)\right)\right)\right)\right), t\right) \]
      unpow2 [=>] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right), \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \color{blue}{\mathsf{*.f64}\left(t, t\right)}\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), x\right)\right)\right)\right)\right)\right), t\right) \]
      fma-udef [<=] 49.9	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right), \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}, x\right)\right)\right)\right)\right)\right), t\right) \]

   5. Taylor expanded in l around -inf 44.2%

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

   6. Simplified 44.2%

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

      [Start] 44.2	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \ell\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right), t\right) \]
      mul-1-neg [=>] 44.2	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \ell\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)}\right), t\right) \]
      distribute-rgt-neg-in [=>] 44.2	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \ell\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)}\right), t\right) \]
      *-commutative [=>] 44.2	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right)}, \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right), t\right) \]

   7. Applied egg-rr 49.4%

      \[\leadsto \mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)}, t\right) \]
      Proof

      [Start] 44.2	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right), t\right) \]
      add-sqr-sqrt [=>] 32.3	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right)\right)\right)}, t\right) \]
      sqrt-unprod [=>] 51.1	\[ \mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right)\right)\right)}, t\right) \]
      frac-times [=>] 51.0	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right)\right)}\right), t\right) \]
      add-sqr-sqrt [<=] 51.0	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\color{blue}{2}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right)\right)\right), t\right) \]
      *-commutative [=>] 51.0	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right)\right)}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right)\right)\right)\right), t\right) \]
      *-commutative [=>] 51.0	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right)\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right)\right)}\right)\right)\right), t\right) \]
      swap-sqr [=>] 49.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right)\right)\right)}\right)\right), t\right) \]
      sqr-neg [=>] 49.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, x\right)\right)\right)}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)\right), t\right) \]
      add-sqr-sqrt [<=] 49.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\color{blue}{\mathsf{/.f64}\left(1, x\right)}, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)\right), t\right) \]
      *-commutative [=>] 49.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{*.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \ell\right)}, \mathsf{*.f64}\left(\ell, \mathsf{sqrt.f64}\left(2\right)\right)\right)\right)\right)\right), t\right) \]
      *-commutative [=>] 49.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \ell\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \ell\right)}\right)\right)\right)\right), t\right) \]
      swap-sqr [=>] 49.3	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(2\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}\right)\right)\right), t\right) \]

   8. Simplified 49.4%

      \[\leadsto \mathsf{*.f64}\left(\color{blue}{\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{/.f64}\left(2, x\right)\right)\right)\right)}, t\right) \]
      Proof

      [Start] 49.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right), t\right) \]
      associate-*r* [=>] 49.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), 2\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}\right)\right), t\right) \]
      *-commutative [=>] 49.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \color{blue}{\mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, x\right), 2\right)\right)}\right)\right), t\right) \]
      associate-*l/ [=>] 49.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(1, 2\right), x\right)}\right)\right)\right), t\right) \]
      metadata-eval [=>] 49.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{/.f64}\left(\color{blue}{2}, x\right)\right)\right)\right), t\right) \]

   if 1e-242 < (*.f64 (sqrt.f64 2) t) < 4.00000000000000011e-206 or 4.0000000000000001e27 < (*.f64 (sqrt.f64 2) t)

   1. Initial program 31.1%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]

   2. Simplified 31.2%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \mathsf{fma.f64}\left(\ell, \ell, \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right)} \]
      Proof

      [Start] 31.1	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]
      associate-/l* [=>] 31.2	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right)} \]
      fma-neg [=>] 31.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)}\right), t\right)\right) \]
      remove-double-neg [<=] 31.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right), t\right)\right) \]
      fma-neg [<=] 31.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\color{blue}{\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}\right), t\right)\right) \]
      sub-neg [=>] 31.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(1\right)\right)}\right), \mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]
      metadata-eval [=>] 31.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, \color{blue}{-1}\right)\right), \mathsf{neg.f64}\left(\mathsf{neg.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]
      remove-double-neg [=>] 31.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)}\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]
      fma-def [=>] 31.2	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{fma.f64}\left(\ell, \ell, \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)}\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right), t\right)\right) \]

   3. Taylor expanded in t around -inf 1.6%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right)\right)\right)}\right) \]

   4. Simplified 1.6%

      \[\leadsto \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)}\right) \]
      Proof

      [Start] 1.6	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(-1, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right)\right)\right)\right) \]
      mul-1-neg [=>] 1.6	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right)\right)\right)}\right) \]
      *-commutative [=>] 1.6	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right), \mathsf{sqrt.f64}\left(2\right)\right)}\right)\right) \]
      distribute-rgt-neg-in [=>] 1.6	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{\_.f64}\left(x, 1\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)}\right) \]
      +-commutative [=>] 1.6	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(x, 1\right)}, \mathsf{\_.f64}\left(x, 1\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      sub-neg [=>] 1.6	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(1\right)\right)}\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      metadata-eval [=>] 1.6	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, \color{blue}{-1}\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      +-commutative [=>] 1.6	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(-1, x\right)}\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]

   5. Applied egg-rr 89.7%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(2\right)\right)\right)} \]
      Proof

      [Start] 1.6	\[ \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      *-un-lft-identity [=>] 1.6	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(1, \mathsf{sqrt.f64}\left(2\right)\right)}, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      times-frac [=>] 1.6	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)} \]
      +-commutative [=>] 1.6	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, -1\right)}\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right) \]
      add-sqr-sqrt [=>] 0.0	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right), \mathsf{sqrt.f64}\left(\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)}\right)\right) \]
      sqrt-unprod [=>] 89.7	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \color{blue}{\mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right), \mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(2\right)\right)\right)\right)}\right)\right) \]
      sqr-neg [=>] 89.7	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(2\right)\right)}\right)\right)\right) \]
      add-sqr-sqrt [<=] 89.7	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\color{blue}{2}\right)\right)\right) \]

   6. Simplified 89.7%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(-1, x\right)\right)\right)\right)} \]
      Proof

      [Start] 89.7	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right), \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(2\right)\right)\right) \]
      *-inverses [=>] 89.7	\[ \mathsf{*.f64}\left(\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right), \color{blue}{1}\right) \]
      *-rgt-identity [=>] 89.7	\[ \color{blue}{\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right)} \]
      +-commutative [=>] 89.7	\[ \mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(-1, x\right)}\right)\right)\right) \]

   if 4.00000000000000011e-206 < (*.f64 (sqrt.f64 2) t) < 5.00000000000000015e-140

   1. Initial program 13.5%

      \[\mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]

   2. Simplified 13.5%

      \[\leadsto \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(\ell, \mathsf{neg.f64}\left(\ell\right)\right)\right)\right)\right)\right)} \]
      Proof

      [Start] 13.5	\[ \mathsf{/.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right) \]
      associate-*r/ [<=] 13.5	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)} \]
      fma-neg [=>] 13.5	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{\_.f64}\left(x, 1\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)}\right)\right)\right) \]
      sub-neg [=>] 13.5	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(1\right)\right)}\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 13.5	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, \color{blue}{-1}\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)\right) \]
      +-commutative [=>] 13.5	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)\right) \]
      fma-def [=>] 13.5	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \color{blue}{\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right)\right)\right)\right)\right)\right) \]
      distribute-rgt-neg-in [=>] 13.5	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(x, 1\right), \mathsf{+.f64}\left(x, -1\right)\right), \mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), \color{blue}{\mathsf{*.f64}\left(\ell, \mathsf{neg.f64}\left(\ell\right)\right)}\right)\right)\right)\right) \]

   3. Taylor expanded in x around inf 12.4%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right)\right)\right)}\right)\right)\right) \]

   4. Simplified 46.4%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(0, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), x\right)\right)\right)}\right)\right)\right) \]
      Proof

      [Start] 12.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right)\right)\right)\right)\right)\right) \]
      unpow2 [=>] 12.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\ell, \ell\right)}, \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right)\right)\right)\right)\right)\right) \]
      +-commutative [=>] 12.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)}\right)\right)\right)\right) \]
      associate-+r+ [=>] 41.1	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)}\right)\right)\right) \]
      +-commutative [<=] 41.1	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right)}\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      associate-+r+ [=>] 46.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(-1, \mathsf{pow.f64}\left(\ell, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right)}, \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      unpow2 [=>] 46.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(-1, \color{blue}{\mathsf{*.f64}\left(\ell, \ell\right)}\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      distribute-rgt1-in [=>] 46.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{+.f64}\left(-1, 1\right), \mathsf{*.f64}\left(\ell, \ell\right)\right)}, \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      metadata-eval [=>] 46.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\color{blue}{0}, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]
      unpow2 [=>] 46.4	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(0, \mathsf{*.f64}\left(\ell, \ell\right)\right), \mathsf{*.f64}\left(2, \color{blue}{\mathsf{*.f64}\left(t, t\right)}\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{+.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), \mathsf{*.f64}\left(2, \mathsf{pow.f64}\left(t, 2\right)\right)\right), x\right)\right)\right)\right)\right)\right) \]

   5. Taylor expanded in l around inf 38.8%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), x\right)\right)}\right)\right)\right) \]

   6. Simplified 45.6%

      \[\leadsto \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\color{blue}{\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\ell, \mathsf{/.f64}\left(x, \ell\right)\right)\right)}\right)\right)\right) \]
      Proof

      [Start] 38.8	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{pow.f64}\left(\ell, 2\right), x\right)\right)\right)\right)\right) \]
      unpow2 [=>] 38.8	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(\ell, \ell\right)}, x\right)\right)\right)\right)\right) \]
      associate-/l* [=>] 45.6	\[ \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(2, \color{blue}{\mathsf{/.f64}\left(\ell, \mathsf{/.f64}\left(x, \ell\right)\right)}\right)\right)\right)\right) \]

3. Recombined 6 regimes into one program.

4. Final simplification 80.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), -399999999999999966445568\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \frac{-4763410263543689}{95268205270873786358080970147496530326800480428008152797215483387004752771599292606210513399154418065180265231976520474104247304665780191232}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), 0\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;-1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{/.f64}\left(2, x\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \frac{7229475734293037}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), \frac{5363123171977039}{107262463439540776796592199985646769019834926564739147021788491549774112240588375814414994385335227421520254865491888406830031062495572559571469192048672768}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\ell, \mathsf{/.f64}\left(x, \ell\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right), 4000000000000000053150220288\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{*.f64}\left(t, t\right)\right), \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), 0\right)\right), \mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right)\right)\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	81.8%
Cost	61273

\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right)\\ t_2 := \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{*.f64}\left(t, t\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right)\right)\right), \mathsf{/.f64}\left(\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), x\right)\right)\\ t_3 := \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), t_2\right)\right)\\ t_4 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -49999999999999998431683053958987776\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_4\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-5237424972633827}{52374249726338269920211035149241586435466272736689036631732661889538140742474792878132321477214466514414186946040961136147476104734166288853256441430016}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), t_3\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;-1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right):\\ \;\;\;\;\mathsf{/.f64}\left(t_1, t_3\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{7229475734293037}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right) \lor \neg \mathsf{<=.f64}\left(t_1, 4000000000000000053150220288\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_4\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(t_2, \mathsf{*.f64}\left(\ell, \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(x, \ell\right)\right)\right)\right)\right)\right)\right)\\ \end{array} \]

Alternative 2
Accuracy	81.8%
Cost	61145

\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right)\\ t_2 := \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{*.f64}\left(t, t\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right)\right)\right), \mathsf{/.f64}\left(\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), x\right)\right)\right)\right)\\ t_3 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -49999999999999998431683053958987776\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_3\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-5237424972633827}{52374249726338269920211035149241586435466272736689036631732661889538140742474792878132321477214466514414186946040961136147476104734166288853256441430016}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), t_2\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;-1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right) \lor \neg \mathsf{<=.f64}\left(t_1, \frac{7229475734293037}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right) \land \mathsf{<=.f64}\left(t_1, 4000000000000000053150220288\right):\\ \;\;\;\;\mathsf{/.f64}\left(t_1, t_2\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_3\right)\right)\\ \end{array} \]

Alternative 3
Accuracy	82.0%
Cost	61144

\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right)\\ t_2 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ t_3 := \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right), \mathsf{+.f64}\left(\mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{*.f64}\left(t, t\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right)\right)\right), \mathsf{/.f64}\left(\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), x\right)\right)\right)\right)\\ t_4 := \mathsf{+.f64}\left(2, \mathsf{/.f64}\left(4, x\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -49999999999999998431683053958987776\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_2\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-5237424972633827}{52374249726338269920211035149241586435466272736689036631732661889538140742474792878132321477214466514414186946040961136147476104734166288853256441430016}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), t_3\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;-1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-4941461262385513}{24707306311927565716857342128774085333197833223161879682238935306082805123046306993647507776054336486228891340858985829027076261887914242781617846672453431386903982455635542158748401823985988322905245077938567513252198179128990807936780194781391547404884040101606295111368825026273254703636026307207764436438929167613952}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(x\right), \mathsf{/.f64}\left(-1, \ell\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{8139666055761541}{813966605576154086191388158047028539690522256142078632860871314912602201882035164980643579207953404631705311351737456109117285358168867807661542486856790777111225290468019355281137486073219485440547487321275219968468108891293513341206528}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{fma.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{*.f64}\left(t, x\right)\right), \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_4\right)\right), \mathsf{*.f64}\left(t, \mathsf{sqrt.f64}\left(t_4\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, 4000000000000000053150220288\right):\\ \;\;\;\;\mathsf{/.f64}\left(t_1, t_3\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_2\right)\right)\\ \end{array} \]

Alternative 4
Accuracy	81.6%
Cost	54617

\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right)\\ t_2 := \mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right)\\ t_3 := \mathsf{+.f64}\left(t_2, \mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{*.f64}\left(t, t\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right)\right)\right)\right)\\ t_4 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -49999999999999998431683053958987776\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_4\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-5237424972633827}{52374249726338269920211035149241586435466272736689036631732661889538140742474792878132321477214466514414186946040961136147476104734166288853256441430016}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(t_2, t_3\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;-1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{/.f64}\left(2, x\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{7229475734293037}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right) \lor \neg \mathsf{<=.f64}\left(t_1, 4000000000000000053150220288\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_4\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(x, \ell\right)\right)\right), t_3\right)\right)\right)\right)\\ \end{array} \]

Alternative 5
Accuracy	81.7%
Cost	54617

\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right)\\ t_2 := \mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right)\\ t_3 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ t_4 := \mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{*.f64}\left(t, t\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -49999999999999998431683053958987776\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_3\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-5237424972633827}{52374249726338269920211035149241586435466272736689036631732661889538140742474792878132321477214466514414186946040961136147476104734166288853256441430016}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(t_2, \mathsf{+.f64}\left(t_4, \mathsf{/.f64}\left(\mathsf{fma.f64}\left(2, \mathsf{*.f64}\left(t, t\right), \mathsf{*.f64}\left(\ell, \ell\right)\right), x\right)\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;-1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{/.f64}\left(2, x\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{7229475734293037}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right) \lor \neg \mathsf{<=.f64}\left(t_1, 4000000000000000053150220288\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_3\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(\ell, \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(x, \ell\right)\right)\right), \mathsf{+.f64}\left(t_2, t_4\right)\right)\right)\right)\right)\\ \end{array} \]

Alternative 6
Accuracy	81.6%
Cost	54489

\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right)\\ t_2 := \mathsf{/.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), x\right)\\ t_3 := \mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{sqrt.f64}\left(\mathsf{+.f64}\left(t_2, \mathsf{+.f64}\left(t_2, \mathsf{*.f64}\left(2, \mathsf{+.f64}\left(\mathsf{*.f64}\left(t, t\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(t, t\right), x\right)\right)\right)\right)\right)\right)\right)\right)\\ t_4 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -49999999999999998431683053958987776\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_4\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-5237424972633827}{52374249726338269920211035149241586435466272736689036631732661889538140742474792878132321477214466514414186946040961136147476104734166288853256441430016}\right):\\ \;\;\;\;t_3\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;-1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{/.f64}\left(2, x\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{7229475734293037}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right) \lor \neg \mathsf{<=.f64}\left(t_1, 4000000000000000053150220288\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_4\right)\right)\\ \mathbf{else}:\\ \;\;\;\;t_3\\ \end{array} \]

Alternative 7
Accuracy	78.1%
Cost	40145

\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right)\\ t_2 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_2\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{/.f64}\left(2, x\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{7229475734293037}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right) \lor \neg \mathsf{<=.f64}\left(t_1, \frac{5363123171977039}{13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096}\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), \mathsf{/.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{*.f64}\left(2, \mathsf{/.f64}\left(\ell, \mathsf{/.f64}\left(x, \ell\right)\right)\right)\right)\right)\right)\\ \end{array} \]

Alternative 8
Accuracy	77.4%
Cost	33617

\[\begin{array}{l} t_1 := \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(2\right), t\right)\\ t_2 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, \frac{-8618206661096855}{172364133221937103085272756482216056112753534658909761028039668631756215232006744379020625060744018369805777923479247838020220755974022884986972234404720831691332769255536872593544438018353486799545737272878084128768}\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_2\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(2, \mathsf{*.f64}\left(\mathsf{*.f64}\left(\ell, \ell\right), \mathsf{/.f64}\left(2, x\right)\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, \frac{7229475734293037}{180736893357325919804742965901096183254486650358500961579737723575212405143116703993975930943694719806137463391890175780999890999416217020648099397663164550811570949854893831716648452639533025774320471006645409943407034368}\right) \lor \neg \mathsf{<=.f64}\left(t_1, \frac{5363123171977039}{13407807929942597099574024998205846127479365820592393377723561443721764030073546976801874298166903427690031858186486050853753882811946569946433649006084096}\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_2\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(x\right), \ell\right)\right)\\ \end{array} \]

Alternative 9
Accuracy	76.4%
Cost	7636

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{-2151104382609775}{5515652263101987298728728207430913795608113109085112352897269396216198887424215820128660001943808587833784893551335930816647064191168732319583111500951066614122648616177179922993422016587311577585463592732098692120576}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{\_.f64}\left(-1, \mathsf{/.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{75075168288047}{3753758414402350114985578847754628430655879796774751768338949695381315781309615853973705099290165690424277009592352731309591345333151121630880730453319952580019863461295451288668314174944572706159989883958951313077165169522342308559632306943619798833037312}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(x\right), \mathsf{/.f64}\left(-1, \ell\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{691871614739731}{813966605576154086191388158047028539690522256142078632860871314912602201882035164980643579207953404631705311351737456109117285358168867807661542486856790777111225290468019355281137486073219485440547487321275219968468108891293513341206528}\right):\\ \;\;\;\;1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{2813939042295035}{194064761537588616893622436057812819407110752139587076392381504753256369085797110791359801103580809743810966337141384150771447505514351798930535909380147642400556872002606238193783160703949805603157874899214558593861605856727007232}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(x\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(t\right), \ell\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{3299577732759311}{104748499452676539840422070298483172870932545473378073263465323779076281484949585756264642954428933028828373892081922272294952209468332577706512882860032}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(x\right), \ell\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\right)\right)\\ \end{array} \]

Alternative 10
Accuracy	76.6%
Cost	7636

\[\begin{array}{l} t_1 := \mathsf{/.f64}\left(\mathsf{+.f64}\left(1, x\right), \mathsf{+.f64}\left(x, -1\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{-1723641332219371}{344728266443874206170545512964432112225507069317819522056079337263512430464013488758041250121488036739611555846958495676040441511948045769973944468809441663382665538511073745187088876036706973599091474545756168257536}\right):\\ \;\;\;\;\mathsf{neg.f64}\left(\mathsf{sqrt.f64}\left(\mathsf{/.f64}\left(1, t_1\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{7687697232696013}{960962154087001629436308185025184878247905227974336452694771122017616840015261658617268505418282416748614914455642299215255384405286687137505466996049907860485085046091635529899088428785810612776957410293491536147754283397719630991265870577566668501257551872}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(x\right), \mathsf{/.f64}\left(-1, \ell\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{6511732844609233}{6511732844609232689531105264376228317524178049136629062886970519300817615056281319845148633663627237053642490813899648872938282865350942461292339894854326216889802323744154842249099888585755883524379898570201759747744871130348106729652224}\right):\\ \;\;\;\;1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{6292535679128659}{370149157595803483760113594165444983305188659934209969315302857882035005733103009779662706572686786162969525026591079999487776766804412458287307566414161000062097305302822567355696031005763636785808324621609799564097606385664}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(x\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(t\right), \ell\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{392806872947537}{13093562431584567480052758787310396608866568184172259157933165472384535185618698219533080369303616628603546736510240284036869026183541572213314110357504}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(x\right), \ell\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{sqrt.f64}\left(t_1\right)\right)\\ \end{array} \]

Alternative 11
Accuracy	75.7%
Cost	7248

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{-1482331545708659}{689456532887748412341091025928864224451014138635639044112158674527024860928026977516082500242976073479223111693916991352080883023896091539947888937618883326765331077022147490374177752073413947198182949091512336515072}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{\_.f64}\left(-1, \mathsf{/.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{4084089154869757}{480481077043500814718154092512592439123952613987168226347385561008808420007630829308634252709141208374307457227821149607627692202643343568752733498024953930242542523045817764949544214392905306388478705146745768073877141698859815495632935288783334250628775936}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(x\right), \mathsf{/.f64}\left(t, \ell\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{8941389410887987}{21545516652742137885659094560277007014094191832363720128504958578969526904000843047377578132593002296225722240434905979752527594496752860623371529300590103961416596156942109074193054752294185849943217159109760516096}\right):\\ \;\;\;\;1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{4424576616881057}{26815615859885194199148049996411692254958731641184786755447122887443528060147093953603748596333806855380063716372972101707507765623893139892867298012168192}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(x\right), \ell\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 12
Accuracy	75.6%
Cost	7248

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{-1723641332219371}{344728266443874206170545512964432112225507069317819522056079337263512430464013488758041250121488036739611555846958495676040441511948045769973944468809441663382665538511073745187088876036706973599091474545756168257536}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{\_.f64}\left(-1, \mathsf{/.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{75075168288047}{7507516828804700229971157695509256861311759593549503536677899390762631562619231707947410198580331380848554019184705462619182690666302243261761460906639905160039726922590902577336628349889145412319979767917902626154330339044684617119264613887239597666074624}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(x\right), \mathsf{/.f64}\left(\mathsf{neg.f64}\left(t\right), \ell\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{5860559560148309}{13023465689218465379062210528752456635048356098273258125773941038601635230112562639690297267327254474107284981627799297745876565730701884922584679789708652433779604647488309684498199777171511767048759797140403519495489742260696213459304448}\right):\\ \;\;\;\;1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{4424576616881057}{26815615859885194199148049996411692254958731641184786755447122887443528060147093953603748596333806855380063716372972101707507765623893139892867298012168192}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(x\right), \ell\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 13
Accuracy	76.0%
Cost	7248

\[\begin{array}{l} t_1 := \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(x\right), \ell\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{-4964087036791789}{2757826131550993649364364103715456897804056554542556176448634698108099443712107910064330000971904293916892446775667965408323532095584366159791555750475533307061324308088589961496711008293655788792731796366049346060288}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{\_.f64}\left(-1, \mathsf{/.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{7495504801878613}{960962154087001629436308185025184878247905227974336452694771122017616840015261658617268505418282416748614914455642299215255384405286687137505466996049907860485085046091635529899088428785810612776957410293491536147754283397719630991265870577566668501257551872}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t_1, \mathsf{neg.f64}\left(t\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{7814079413531079}{3255866422304616344765552632188114158762089024568314531443485259650408807528140659922574316831813618526821245406949824436469141432675471230646169947427163108444901161872077421124549944292877941762189949285100879873872435565174053364826112}\right):\\ \;\;\;\;1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{4424576616881057}{26815615859885194199148049996411692254958731641184786755447122887443528060147093953603748596333806855380063716372972101707507765623893139892867298012168192}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, t_1\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 14
Accuracy	76.0%
Cost	7248

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{-8273478394652981}{5515652263101987298728728207430913795608113109085112352897269396216198887424215820128660001943808587833784893551335930816647064191168732319583111500951066614122648616177179922993422016587311577585463592732098692120576}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{\_.f64}\left(-1, \mathsf{/.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{5525532386000259}{480481077043500814718154092512592439123952613987168226347385561008808420007630829308634252709141208374307457227821149607627692202643343568752733498024953930242542523045817764949544214392905306388478705146745768073877141698859815495632935288783334250628775936}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(x\right), \mathsf{/.f64}\left(-1, \ell\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{4232626348996001}{813966605576154086191388158047028539690522256142078632860871314912602201882035164980643579207953404631705311351737456109117285358168867807661542486856790777111225290468019355281137486073219485440547487321275219968468108891293513341206528}\right):\\ \;\;\;\;1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{4424576616881057}{26815615859885194199148049996411692254958731641184786755447122887443528060147093953603748596333806855380063716372972101707507765623893139892867298012168192}\right):\\ \;\;\;\;\mathsf{*.f64}\left(t, \mathsf{/.f64}\left(\mathsf{sqrt.f64}\left(x\right), \ell\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 15
Accuracy	76.6%
Cost	6984

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{-6729095760984425}{5515652263101987298728728207430913795608113109085112352897269396216198887424215820128660001943808587833784893551335930816647064191168732319583111500951066614122648616177179922993422016587311577585463592732098692120576}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{\_.f64}\left(-1, \mathsf{/.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t, \frac{7687697232696013}{960962154087001629436308185025184878247905227974336452694771122017616840015261658617268505418282416748614914455642299215255384405286687137505466996049907860485085046091635529899088428785810612776957410293491536147754283397719630991265870577566668501257551872}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{sqrt.f64}\left(x\right), \mathsf{/.f64}\left(t, \ell\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 16
Accuracy	76.0%
Cost	836

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{5890680864316837}{184083777009901148951480851536796132722480842643692193047992403105518260024832986247893480778145316885626996612988306798242600723265962621432675768974821503362834322867062256922933472871676000378319956942935045907290266298718681990629287025193807090855270922941016369397705979841003229496151404881535205516509184}\right):\\ \;\;\;\;\mathsf{+.f64}\left(\mathsf{/.f64}\left(1, x\right), \mathsf{\_.f64}\left(-1, \mathsf{/.f64}\left(\frac{1}{2}, \mathsf{*.f64}\left(x, x\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 17
Accuracy	75.9%
Cost	452

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{5890680864316837}{184083777009901148951480851536796132722480842643692193047992403105518260024832986247893480778145316885626996612988306798242600723265962621432675768974821503362834322867062256922933472871676000378319956942935045907290266298718681990629287025193807090855270922941016369397705979841003229496151404881535205516509184}\right):\\ \;\;\;\;\mathsf{+.f64}\left(-1, \mathsf{/.f64}\left(1, x\right)\right)\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 18
Accuracy	75.8%
Cost	196

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(t, \frac{-20240225330731}{101201126653655309176247673359458653524778324882071059178450679013715169783997673445980191850718562247593538932158405955694904368692896738433506699970369254960758712138283180682233453871046608170619883839236372534281003741712346349309051677824579778170405028256179384776166707307615251266093163754323003131653853870546747392}\right):\\ \;\;\;\;-1\\ \mathbf{else}:\\ \;\;\;\;1\\ \end{array} \]

Alternative 19
Accuracy	38.6%
Cost	64

\[-1 \]

Reproduce

herbie shell --seed 2023144 
(FPCore (x l t)
  :name "Toniolo and Linder, Equation (7)"
  :precision binary64
  (/ (* (sqrt 2.0) t) (sqrt (- (* (/ (+ x 1.0) (- x 1.0)) (+ (* l l) (* 2.0 (* t t)))) (* l l)))))