Diagrams.Solve.Tridiagonal:solveTriDiagonal from diagrams-solve-0.1, A

Average Accuracy: 83.0% → 96.8%

Time: 19.0s

Precision: binary64

Cost: 2128

Math

\[\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right) \]

↓

\[\begin{array}{l} t_1 := \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\\ t_2 := \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, \mathsf{/.f64}\left(y, t_1\right)\right), \mathsf{/.f64}\left(x, t_1\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -200000000000000009655823040897755724991688492844686312786150858374325529235015311074428291647705988527319131870906741220999075456086329715600792597832264821896052782616171141921272736618612235758357506491949112630604620500944543457696353904452597448704\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(y, \mathsf{/.f64}\left(x, z\right)\right), a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-6189700196426901}{1237940039285380274899124224}\right):\\ \;\;\;\;t_2\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 5000000000000000073153476153374365154850214939323275296393053935848981821255741079552\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(z, y\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 500000000000000028237705510260420707420313190991529187350282582077728281983789098594609880794729991489884084673768181048282990322303461938652580072801639889709891970152031159909282119041295638459799794152650876636200924348147564544\right):\\ \;\;\;\;t_2\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(x, a\right), z\right)\right)\\ \end{array} \]

FPCore

(FPCore (x y z t a)
 :precision binary64
 (/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 a z))))

↓

(FPCore (x y z t a)
 :precision binary64
 (let* ((t_1 (-.f64 (*.f64 a z) t))
        (t_2 (-.f64 (*.f64 z (/.f64 y t_1)) (/.f64 x t_1))))
   (if (<=.f64
        (*.f64 a z)
        -200000000000000009655823040897755724991688492844686312786150858374325529235015311074428291647705988527319131870906741220999075456086329715600792597832264821896052782616171141921272736618612235758357506491949112630604620500944543457696353904452597448704)
     (/.f64 (-.f64 y (/.f64 x z)) a)
     (if (<=.f64 (*.f64 a z) -6189700196426901/1237940039285380274899124224)
       t_2
       (if (<=.f64
            (*.f64 a z)
            5000000000000000073153476153374365154850214939323275296393053935848981821255741079552)
         (/.f64 (-.f64 x (*.f64 z y)) (-.f64 t (*.f64 a z)))
         (if (<=.f64
              (*.f64 a z)
              500000000000000028237705510260420707420313190991529187350282582077728281983789098594609880794729991489884084673768181048282990322303461938652580072801639889709891970152031159909282119041295638459799794152650876636200924348147564544)
           t_2
           (-.f64 (/.f64 y a) (/.f64 (/.f64 x a) z))))))))

Target

Original	83.0%
Target	96.8%
Herbie	96.8%

\[\begin{array}{l} \mathbf{if}\;\mathsf{<.f64}\left(z, -32113435955957344\right):\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right), \mathsf{/.f64}\left(y, \mathsf{\_.f64}\left(\mathsf{/.f64}\left(t, z\right), a\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<.f64}\left(z, \frac{4392440296622287}{125000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000}\right):\\ \;\;\;\;\mathsf{*.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{/.f64}\left(1, \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right), \mathsf{/.f64}\left(y, \mathsf{\_.f64}\left(\mathsf{/.f64}\left(t, z\right), a\right)\right)\right)\\ \end{array} \]

Derivation

1. Split input into 4 regimes

2. if (*.f64 a z) < -2.0000000000000001e251

   1. Initial program 39.1%

      \[\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right) \]

   2. Simplified 39.1%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)} \]
      Proof

      [Start] 39.1	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right) \]
      sub-neg [=>] 39.1	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{+.f64}\left(t, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(a, z\right)\right)\right)}\right) \]
      +-commutative [=>] 39.1	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(a, z\right)\right), t\right)}\right) \]
      neg-sub0 [=>] 39.1	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{+.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(a, z\right)\right)}, t\right)\right) \]
      associate-+l- [=>] 39.1	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{\_.f64}\left(0, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)}\right) \]
      sub0-neg [=>] 39.1	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)}\right) \]
      neg-mul-1 [=>] 39.1	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)}\right) \]
      sub-neg [=>] 39.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(y, z\right)\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      +-commutative [=>] 39.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(y, z\right)\right), x\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      neg-sub0 [=>] 39.1	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(y, z\right)\right)}, x\right), \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      associate-+l- [=>] 39.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      sub0-neg [=>] 39.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      neg-mul-1 [=>] 39.1	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      times-frac [=>] 39.1	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(-1, -1\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right)} \]
      metadata-eval [=>] 39.1	\[ \mathsf{*.f64}\left(\color{blue}{1}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      *-lft-identity [=>] 39.1	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)} \]
      *-commutative [=>] 39.1	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(z, a\right)}, t\right)\right) \]

   3. Applied egg-rr 46.9%

      \[\leadsto \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(y, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right), z\right)\right), \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)\right)} \]
      Proof

      [Start] 39.1	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right) \]
      div-sub [=>] 39.1	\[ \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(y, z\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right), \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)\right)} \]
      associate-/l* [=>] 46.9	\[ \mathsf{\_.f64}\left(\color{blue}{\mathsf{/.f64}\left(y, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right), z\right)\right)}, \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)\right) \]

   4. Taylor expanded in a around inf 98.7%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(y, \mathsf{/.f64}\left(x, z\right)\right), a\right)} \]

   if -2.0000000000000001e251 < (*.f64 a z) < -4.9999999999999997e-12 or 5.0000000000000001e84 < (*.f64 a z) < 5.0000000000000003e230

   1. Initial program 87.7%

      \[\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right) \]

   2. Simplified 87.7%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)} \]
      Proof

      [Start] 87.7	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right) \]
      sub-neg [=>] 87.7	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{+.f64}\left(t, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(a, z\right)\right)\right)}\right) \]
      +-commutative [=>] 87.7	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(a, z\right)\right), t\right)}\right) \]
      neg-sub0 [=>] 87.7	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{+.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(a, z\right)\right)}, t\right)\right) \]
      associate-+l- [=>] 87.7	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{\_.f64}\left(0, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)}\right) \]
      sub0-neg [=>] 87.7	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)}\right) \]
      neg-mul-1 [=>] 87.7	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)}\right) \]
      sub-neg [=>] 87.7	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(y, z\right)\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      +-commutative [=>] 87.7	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(y, z\right)\right), x\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      neg-sub0 [=>] 87.7	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(y, z\right)\right)}, x\right), \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      associate-+l- [=>] 87.7	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      sub0-neg [=>] 87.7	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      neg-mul-1 [=>] 87.7	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      times-frac [=>] 87.7	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(-1, -1\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right)} \]
      metadata-eval [=>] 87.7	\[ \mathsf{*.f64}\left(\color{blue}{1}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      *-lft-identity [=>] 87.7	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)} \]
      *-commutative [=>] 87.7	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(z, a\right)}, t\right)\right) \]

   3. Applied egg-rr 98.3%

      \[\leadsto \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(y, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right), z\right)\right), \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)\right)} \]
      Proof

      [Start] 87.7	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right) \]
      div-sub [=>] 87.7	\[ \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(y, z\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right), \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)\right)} \]
      associate-/l* [=>] 98.3	\[ \mathsf{\_.f64}\left(\color{blue}{\mathsf{/.f64}\left(y, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right), z\right)\right)}, \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)\right) \]

   4. Applied egg-rr 94.6%

      \[\leadsto \mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(y, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right), z\right)}, \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)\right) \]
      Proof

      [Start] 98.3	\[ \mathsf{\_.f64}\left(\mathsf{/.f64}\left(y, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right), z\right)\right), \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)\right) \]
      associate-/r/ [=>] 94.6	\[ \mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(y, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right), z\right)}, \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)\right) \]

   if -4.9999999999999997e-12 < (*.f64 a z) < 5.0000000000000001e84

   1. Initial program 97.5%

      \[\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right) \]

   if 5.0000000000000003e230 < (*.f64 a z)

   1. Initial program 40.5%

      \[\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right) \]

   2. Simplified 40.5%

      \[\leadsto \color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, a\right), t\right)\right)} \]
      Proof

      [Start] 40.5	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right) \]
      sub-neg [=>] 40.5	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{+.f64}\left(t, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(a, z\right)\right)\right)}\right) \]
      +-commutative [=>] 40.5	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(a, z\right)\right), t\right)}\right) \]
      neg-sub0 [=>] 40.5	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \mathsf{+.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(a, z\right)\right)}, t\right)\right) \]
      associate-+l- [=>] 40.5	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{\_.f64}\left(0, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)}\right) \]
      sub0-neg [=>] 40.5	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)}\right) \]
      neg-mul-1 [=>] 40.5	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(y, z\right)\right), \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)}\right) \]
      sub-neg [=>] 40.5	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(x, \mathsf{neg.f64}\left(\mathsf{*.f64}\left(y, z\right)\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      +-commutative [=>] 40.5	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{neg.f64}\left(\mathsf{*.f64}\left(y, z\right)\right), x\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      neg-sub0 [=>] 40.5	\[ \mathsf{/.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{*.f64}\left(y, z\right)\right)}, x\right), \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      associate-+l- [=>] 40.5	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{\_.f64}\left(0, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      sub0-neg [=>] 40.5	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      neg-mul-1 [=>] 40.5	\[ \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      times-frac [=>] 40.5	\[ \color{blue}{\mathsf{*.f64}\left(\mathsf{/.f64}\left(-1, -1\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right)} \]
      metadata-eval [=>] 40.5	\[ \mathsf{*.f64}\left(\color{blue}{1}, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right) \]
      *-lft-identity [=>] 40.5	\[ \color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)} \]
      *-commutative [=>] 40.5	\[ \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(y, z\right), x\right), \mathsf{\_.f64}\left(\color{blue}{\mathsf{*.f64}\left(z, a\right)}, t\right)\right) \]

   3. Taylor expanded in z around inf 73.5%

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

   4. Simplified 95.7%

      \[\leadsto \color{blue}{\mathsf{\_.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(x, a\right), \mathsf{*.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{/.f64}\left(t, a\right)\right)\right), z\right)\right)} \]
      Proof

      [Start] 73.5	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(x, \mathsf{*.f64}\left(a, z\right)\right)\right), \mathsf{/.f64}\left(y, a\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 2\right), z\right)\right)\right)\right) \]
      mul-1-neg [=>] 73.5	\[ \mathsf{\_.f64}\left(\mathsf{+.f64}\left(\color{blue}{\mathsf{neg.f64}\left(\mathsf{/.f64}\left(x, \mathsf{*.f64}\left(a, z\right)\right)\right)}, \mathsf{/.f64}\left(y, a\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 2\right), z\right)\right)\right)\right) \]
      +-commutative [=>] 73.5	\[ \mathsf{\_.f64}\left(\color{blue}{\mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{neg.f64}\left(\mathsf{/.f64}\left(x, \mathsf{*.f64}\left(a, z\right)\right)\right)\right)}, \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 2\right), z\right)\right)\right)\right) \]
      associate--l+ [=>] 73.5	\[ \color{blue}{\mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\mathsf{/.f64}\left(x, \mathsf{*.f64}\left(a, z\right)\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 2\right), z\right)\right)\right)\right)\right)} \]
      associate-/r* [=>] 85.9	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{\_.f64}\left(\mathsf{neg.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(x, a\right), z\right)}\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 2\right), z\right)\right)\right)\right)\right) \]
      distribute-neg-frac [=>] 85.9	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{\_.f64}\left(\color{blue}{\mathsf{/.f64}\left(\mathsf{neg.f64}\left(\mathsf{/.f64}\left(x, a\right)\right), z\right)}, \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 2\right), z\right)\right)\right)\right)\right) \]
      mul-1-neg [<=] 85.9	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{\_.f64}\left(\mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(x, a\right)\right)}, z\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{*.f64}\left(\mathsf{pow.f64}\left(a, 2\right), z\right)\right)\right)\right)\right) \]
      associate-/r* [=>] 85.8	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(x, a\right)\right), z\right), \mathsf{*.f64}\left(-1, \color{blue}{\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{pow.f64}\left(a, 2\right)\right), z\right)}\right)\right)\right) \]
      associate-*r/ [=>] 85.8	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{\_.f64}\left(\mathsf{/.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(x, a\right)\right), z\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right), z\right)}\right)\right) \]
      div-sub [<=] 85.8	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \color{blue}{\mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(x, a\right)\right), \mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right)\right), z\right)}\right) \]
      distribute-lft-out-- [=>] 85.8	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{/.f64}\left(\color{blue}{\mathsf{*.f64}\left(-1, \mathsf{\_.f64}\left(\mathsf{/.f64}\left(x, a\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right)\right)}, z\right)\right) \]
      associate-*r/ [<=] 85.8	\[ \mathsf{+.f64}\left(\mathsf{/.f64}\left(y, a\right), \color{blue}{\mathsf{*.f64}\left(-1, \mathsf{/.f64}\left(\mathsf{\_.f64}\left(\mathsf{/.f64}\left(x, a\right), \mathsf{/.f64}\left(\mathsf{*.f64}\left(y, t\right), \mathsf{pow.f64}\left(a, 2\right)\right)\right), z\right)\right)}\right) \]

   5. Taylor expanded in x around inf 96.9%

      \[\leadsto \mathsf{\_.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{/.f64}\left(\color{blue}{\mathsf{/.f64}\left(x, a\right)}, z\right)\right) \]
3. Recombined 4 regimes into one program.

4. Final simplification 96.8%

   \[\leadsto \begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -200000000000000009655823040897755724991688492844686312786150858374325529235015311074428291647705988527319131870906741220999075456086329715600792597832264821896052782616171141921272736618612235758357506491949112630604620500944543457696353904452597448704\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(y, \mathsf{/.f64}\left(x, z\right)\right), a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-6189700196426901}{1237940039285380274899124224}\right):\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, \mathsf{/.f64}\left(y, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right), \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 5000000000000000073153476153374365154850214939323275296393053935848981821255741079552\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(z, y\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 500000000000000028237705510260420707420313190991529187350282582077728281983789098594609880794729991489884084673768181048282990322303461938652580072801639889709891970152031159909282119041295638459799794152650876636200924348147564544\right):\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{*.f64}\left(z, \mathsf{/.f64}\left(y, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right), \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(x, a\right), z\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Accuracy	69.8%
Cost	2529

\[\begin{array}{l} t_1 := \mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -1000000000000000038893577551088388431307372492952020133343023820076912942893848967630799656078777013873264603119412132913531706114094375616540183672212689403544345862626169435445664558076559462193222406635520\right):\\ \;\;\;\;\mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, y\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -499999999999999973297436475782614169496763434109744428272285720156797353246877991443480012589546764662496833043557678065517614119776368694263139634039071761845879577452943421992861696\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -50000000000000000720297379362263692791555931121415631506856157467749463534563065813431628812863228040252718591648116768768\right):\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-6216540455122333}{31082702275611665134711390509176302506278509424834232340028998555822468563283335970816}\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{3757668132438133}{75153362648762663292463379097258784876021841565066235862633311089030688803667470190838367948312598497021919232}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(z, y\right)\right), t\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 100000000000000007629769841091887003294964970946560\right) \lor \neg \mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 4999999999999999797083622281751813657459980448242257198348695049033519614754772127580160\right) \land \mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 50000000000000001187271617932555267870432896391434109373673249433511871477101028628408881410804164706467298456692005803789670658494504078671872\right):\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \end{array} \]

Alternative 2
Accuracy	55.1%
Cost	2272

\[\begin{array}{l} t_1 := \mathsf{/.f64}\left(\mathsf{neg.f64}\left(x\right), \mathsf{*.f64}\left(a, z\right)\right)\\ t_2 := \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, y\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -1000000000000000038893577551088388431307372492952020133343023820076912942893848967630799656078777013873264603119412132913531706114094375616540183672212689403544345862626169435445664558076559462193222406635520\right):\\ \;\;\;\;t_2\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -49999999999999998980852208437685758555356472593342082603381605947872422739278055501808572305519799253930125569581478605944175487936819013075944738996003952930215442747098861295896625152\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -49999999999999997208377623627466690637486435190095003412116017803818992811380155502205974802370865683036809141768159232\right):\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -19999999999999998911504619740856320\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-8627182933488205}{431359146674410236714672241392314090778194310760649159697657763987456}\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, t\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-6216540455122333}{31082702275611665134711390509176302506278509424834232340028998555822468563283335970816}\right):\\ \;\;\;\;t_2\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-2772669694120815}{5545339388241629719156828368286167406872874150751633150340959161229242615611251246079948812208279156194782421922807143657948315648}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(z\right), \mathsf{/.f64}\left(t, y\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 40000000000000000000000\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, t\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \end{array} \]

Alternative 3
Accuracy	54.8%
Cost	2272

\[\begin{array}{l} t_1 := \mathsf{/.f64}\left(1, \mathsf{/.f64}\left(a, y\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -1000000000000000038893577551088388431307372492952020133343023820076912942893848967630799656078777013873264603119412132913531706114094375616540183672212689403544345862626169435445664558076559462193222406635520\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -49999999999999998980852208437685758555356472593342082603381605947872422739278055501808572305519799253930125569581478605944175487936819013075944738996003952930215442747098861295896625152\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(x\right), \mathsf{*.f64}\left(a, z\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -49999999999999997208377623627466690637486435190095003412116017803818992811380155502205974802370865683036809141768159232\right):\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -19999999999999998911504619740856320\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{/.f64}\left(\mathsf{neg.f64}\left(x\right), z\right), a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-8627182933488205}{431359146674410236714672241392314090778194310760649159697657763987456}\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, t\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-6216540455122333}{31082702275611665134711390509176302506278509424834232340028998555822468563283335970816}\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-2772669694120815}{5545339388241629719156828368286167406872874150751633150340959161229242615611251246079948812208279156194782421922807143657948315648}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{neg.f64}\left(z\right), \mathsf{/.f64}\left(t, y\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 40000000000000000000000\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, t\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \end{array} \]

Alternative 4
Accuracy	92.3%
Cost	2248

\[\begin{array}{l} t_1 := \mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(z, y\right)\right), \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(t_1, -\infty\right):\\ \;\;\;\;\mathsf{*.f64}\left(y, \mathsf{/.f64}\left(z, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(t_1, 99999999999999992462348437353960485060448933957923525202610654848990348279466077292501969423268405025328970231162545648343655275306678872441733790178059478330735395060467469727994972900530063978805843953102113868000379620369084502134308975505229555772913629423636305841602377586326247764393984\right):\\ \;\;\;\;t_1\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(y, \mathsf{/.f64}\left(x, z\right)\right), a\right)\\ \end{array} \]

Alternative 5
Accuracy	78.6%
Cost	1616

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -200000000000000000\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(y, \mathsf{/.f64}\left(x, z\right)\right), a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-5521397077432451}{27606985387162255149739023449108101809804435888681546220650096895197184}\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-7167183174968973}{143343663499379469475676305956380433799785311823017570233599302461682679755530300504376159569382855409664}\right):\\ \;\;\;\;\mathsf{*.f64}\left(y, \mathsf{/.f64}\left(z, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 40000000000000000000000\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(z, y\right)\right), t\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(y, a\right), \mathsf{/.f64}\left(\mathsf{/.f64}\left(x, a\right), z\right)\right)\\ \end{array} \]

Alternative 6
Accuracy	97.5%
Cost	1609

\[\begin{array}{l} t_1 := \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -49999999999999997990838700394884966306179965866660791642559438972038274233224047478954738152480007945403339428690378003153531301288658660066937768081850142259483599048726809116347987831785023273225189328871239835991361038587494628380365594466675565382886953520237123630792704\right) \lor \neg \mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 5000000000000000066282994891787081340343280544793230017816015738971246363452126607307989709019681249863687319282946045494061487325003512892275869151373365842953697657627637323430529093779107308789748100916331176292769417786818298761053780855470759280014374688417047589275644482057527862755328\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(y, \mathsf{/.f64}\left(x, z\right)\right), a\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{\_.f64}\left(\mathsf{/.f64}\left(y, \mathsf{/.f64}\left(t_1, z\right)\right), \mathsf{/.f64}\left(x, t_1\right)\right)\\ \end{array} \]

Alternative 7
Accuracy	78.9%
Cost	1488

\[\begin{array}{l} t_1 := \mathsf{/.f64}\left(\mathsf{\_.f64}\left(y, \mathsf{/.f64}\left(x, z\right)\right), a\right)\\ \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), -200000000000000000\right):\\ \;\;\;\;t_1\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-5521397077432451}{27606985387162255149739023449108101809804435888681546220650096895197184}\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), \frac{-7167183174968973}{143343663499379469475676305956380433799785311823017570233599302461682679755530300504376159569382855409664}\right):\\ \;\;\;\;\mathsf{*.f64}\left(y, \mathsf{/.f64}\left(z, \mathsf{\_.f64}\left(\mathsf{*.f64}\left(a, z\right), t\right)\right)\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(a, z\right), 40000000000000000000000\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(x, \mathsf{*.f64}\left(z, y\right)\right), t\right)\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 8
Accuracy	73.1%
Cost	969

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(z, y\right), -2000000000000000000\right) \lor \neg \mathsf{<=.f64}\left(\mathsf{*.f64}\left(z, y\right), \frac{6277101735386681}{3138550867693340381917894711603833208051177722232017256448}\right):\\ \;\;\;\;\mathsf{/.f64}\left(\mathsf{\_.f64}\left(y, \mathsf{/.f64}\left(x, z\right)\right), a\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right)\\ \end{array} \]

Alternative 9
Accuracy	68.8%
Cost	968

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(z, y\right), -999999999999999921281879895665782741935503249059183851809998224123064148429897728\right):\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(z, y\right), 100000000000000004764729344\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, \mathsf{\_.f64}\left(t, \mathsf{*.f64}\left(a, z\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \end{array} \]

Alternative 10
Accuracy	53.9%
Cost	712

\[\begin{array}{l} \mathbf{if}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(z, y\right), -2000000000000000000\right):\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \mathbf{elif}\;\mathsf{<=.f64}\left(\mathsf{*.f64}\left(z, y\right), \frac{6277101735386681}{3138550867693340381917894711603833208051177722232017256448}\right):\\ \;\;\;\;\mathsf{/.f64}\left(x, t\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{/.f64}\left(y, a\right)\\ \end{array} \]

Alternative 11
Accuracy	34.6%
Cost	192

\[\mathsf{/.f64}\left(x, t\right) \]

Reproduce

herbie shell --seed 2023144 
(FPCore (x y z t a)
  :name "Diagrams.Solve.Tridiagonal:solveTriDiagonal from diagrams-solve-0.1, A"
  :precision binary64

  :herbie-target
  (if (< z -32113435955957344.0) (- (/ x (- t (* a z))) (/ y (- (/ t z) a))) (if (< z 3.5139522372978296e-86) (* (- x (* y z)) (/ 1.0 (- t (* a z)))) (- (/ x (- t (* a z))) (/ y (- (/ t z) a)))))

  (/ (- x (* y z)) (- t (* a z))))