Error

Derivation

1. Split input into 5 regimes

2. if t < -2.8052590030851903e+38

   1. Initial program 43.5

      \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}}\]

   2. Taylor expanded around -inf 4.1

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{2 \cdot \frac{t}{{\left(\sqrt{2}\right)}^{3} \cdot {x}^{2}} - \left(2 \cdot \frac{t}{\sqrt{2} \cdot {x}^{2}} + \left(t \cdot \sqrt{2} + 2 \cdot \frac{t}{\sqrt{2} \cdot x}\right)\right)}}\]

   3. Simplified4.1

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\left(\frac{\frac{2}{x}}{x} \cdot \left(\frac{\frac{t}{\sqrt{2}}}{2} - \frac{t}{\sqrt{2}}\right) - \sqrt{2} \cdot t\right) + -2 \cdot \frac{\frac{t}{\sqrt{2}}}{x}}}\]

   if -2.8052590030851903e+38 < t < -7.933867885932409e-206

   1. Initial program 34.6

      \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}}\]

   2. Taylor expanded around inf 13.6

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{2 \cdot {t}^{2} + \left(2 \cdot \frac{{\ell}^{2}}{x} + 4 \cdot \frac{{t}^{2}}{x}\right)}}}\]

   3. Simplified8.9

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\frac{\ell \cdot 2}{\frac{x}{\ell}} + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}}\]
   4. Using strategy rm

   5. Applied div-inv8.9

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\frac{\ell \cdot 2}{\color{blue}{x \cdot \frac{1}{\ell}}} + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}\]

   6. Applied times-frac8.9

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\frac{\ell}{x} \cdot \frac{2}{\frac{1}{\ell}}} + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}\]

   7. Simplified8.9

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\frac{\ell}{x} \cdot \color{blue}{\left(2 \cdot \ell\right)} + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}\]
   8. Using strategy rm

   9. Applied add-sqr-sqrt9.1

      \[\leadsto \frac{\color{blue}{\left(\sqrt{\sqrt{2}} \cdot \sqrt{\sqrt{2}}\right)} \cdot t}{\sqrt{\frac{\ell}{x} \cdot \left(2 \cdot \ell\right) + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}\]

   10. Applied associate-*l*9.0

       \[\leadsto \frac{\color{blue}{\sqrt{\sqrt{2}} \cdot \left(\sqrt{\sqrt{2}} \cdot t\right)}}{\sqrt{\frac{\ell}{x} \cdot \left(2 \cdot \ell\right) + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}\]

   if -7.933867885932409e-206 < t < 4.697398522904137e-166

   1. Initial program 61.6

      \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}}\]

   2. Taylor expanded around inf 32.5

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{2 \cdot {t}^{2} + \left(2 \cdot \frac{{\ell}^{2}}{x} + 4 \cdot \frac{{t}^{2}}{x}\right)}}}\]

   3. Simplified31.3

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\frac{\ell \cdot 2}{\frac{x}{\ell}} + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}}\]
   4. Using strategy rm

   5. Applied div-inv31.3

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\frac{\ell \cdot 2}{\color{blue}{x \cdot \frac{1}{\ell}}} + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}\]

   6. Applied times-frac31.3

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\frac{\ell}{x} \cdot \frac{2}{\frac{1}{\ell}}} + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}\]

   7. Simplified31.3

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\frac{\ell}{x} \cdot \color{blue}{\left(2 \cdot \ell\right)} + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}\]
   8. Using strategy rm

   9. Applied flip3-+31.3

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\frac{\ell}{x} \cdot \left(2 \cdot \ell\right) + t \cdot \left(t \cdot \color{blue}{\frac{{2}^{3} + {\left(\frac{4}{x}\right)}^{3}}{2 \cdot 2 + \left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right)}}\right)}}\]

   10. Applied associate-*r/31.3

       \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\frac{\ell}{x} \cdot \left(2 \cdot \ell\right) + t \cdot \color{blue}{\frac{t \cdot \left({2}^{3} + {\left(\frac{4}{x}\right)}^{3}\right)}{2 \cdot 2 + \left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right)}}}}\]

   11. Applied associate-*r/31.3

       \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\frac{\ell}{x} \cdot \left(2 \cdot \ell\right) + \color{blue}{\frac{t \cdot \left(t \cdot \left({2}^{3} + {\left(\frac{4}{x}\right)}^{3}\right)\right)}{2 \cdot 2 + \left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right)}}}}\]

   12. Applied associate-*l/32.5

       \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\frac{\ell \cdot \left(2 \cdot \ell\right)}{x}} + \frac{t \cdot \left(t \cdot \left({2}^{3} + {\left(\frac{4}{x}\right)}^{3}\right)\right)}{2 \cdot 2 + \left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right)}}}\]

   13. Applied frac-add32.9

       \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\frac{\left(\ell \cdot \left(2 \cdot \ell\right)\right) \cdot \left(2 \cdot 2 + \left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right)\right) + x \cdot \left(t \cdot \left(t \cdot \left({2}^{3} + {\left(\frac{4}{x}\right)}^{3}\right)\right)\right)}{x \cdot \left(2 \cdot 2 + \left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right)\right)}}}}\]

   14. Applied sqrt-div27.4

       \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\frac{\sqrt{\left(\ell \cdot \left(2 \cdot \ell\right)\right) \cdot \left(2 \cdot 2 + \left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right)\right) + x \cdot \left(t \cdot \left(t \cdot \left({2}^{3} + {\left(\frac{4}{x}\right)}^{3}\right)\right)\right)}}{\sqrt{x \cdot \left(2 \cdot 2 + \left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right)\right)}}}}\]

   15. Simplified20.1

       \[\leadsto \frac{\sqrt{2} \cdot t}{\frac{\color{blue}{\sqrt{\left(t \cdot x\right) \cdot \left(\left(\frac{4}{x} \cdot \left(\frac{4}{x} \cdot \frac{4}{x}\right) + 8\right) \cdot t\right) + \left(\ell \cdot \left(\ell \cdot 2\right)\right) \cdot \left(\frac{4}{x} \cdot \left(\frac{4}{x} - 2\right) + 4\right)}}}{\sqrt{x \cdot \left(2 \cdot 2 + \left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right)\right)}}}\]

   if 4.697398522904137e-166 < t < 7.445703208013277e+140

   1. Initial program 25.3

      \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}}\]

   2. Taylor expanded around inf 11.5

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{2 \cdot {t}^{2} + \left(2 \cdot \frac{{\ell}^{2}}{x} + 4 \cdot \frac{{t}^{2}}{x}\right)}}}\]

   3. Simplified5.1

      \[\leadsto \frac{\sqrt{2} \cdot t}{\sqrt{\color{blue}{\frac{\ell \cdot 2}{\frac{x}{\ell}} + t \cdot \left(t \cdot \left(2 + \frac{4}{x}\right)\right)}}}\]

   if 7.445703208013277e+140 < t

   1. Initial program 58.5

      \[\frac{\sqrt{2} \cdot t}{\sqrt{\frac{x + 1}{x - 1} \cdot \left(\ell \cdot \ell + 2 \cdot \left(t \cdot t\right)\right) - \ell \cdot \ell}}\]

   2. Taylor expanded around inf 2.1

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\left(2 \cdot \frac{t}{\sqrt{2} \cdot {x}^{2}} + \left(t \cdot \sqrt{2} + 2 \cdot \frac{t}{\sqrt{2} \cdot x}\right)\right) - 2 \cdot \frac{t}{{\left(\sqrt{2}\right)}^{3} \cdot {x}^{2}}}}\]

   3. Simplified2.1

      \[\leadsto \frac{\sqrt{2} \cdot t}{\color{blue}{\left(\sqrt{2} \cdot t + \frac{\frac{t}{\sqrt{2}} \cdot 2}{x}\right) + \left(\frac{\frac{t}{\sqrt{2}} \cdot 2}{x \cdot x} - \frac{\frac{t}{\sqrt{2}}}{x \cdot x}\right)}}\]
3. Recombined 5 regimes into one program.

4. Final simplification7.5

   \[\leadsto \begin{array}{l} \mathbf{if}\;t \le -2.8052590030851903 \cdot 10^{+38}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t}{\left(\left(\frac{\frac{t}{\sqrt{2}}}{2} - \frac{t}{\sqrt{2}}\right) \cdot \frac{\frac{2}{x}}{x} - \sqrt{2} \cdot t\right) + \frac{\frac{t}{\sqrt{2}}}{x} \cdot -2}\\ \mathbf{elif}\;t \le -7.933867885932409 \cdot 10^{-206}:\\ \;\;\;\;\frac{\sqrt{\sqrt{2}} \cdot \left(\sqrt{\sqrt{2}} \cdot t\right)}{\sqrt{\left(t \cdot \left(2 + \frac{4}{x}\right)\right) \cdot t + \frac{\ell}{x} \cdot \left(\ell \cdot 2\right)}}\\ \mathbf{elif}\;t \le 4.697398522904137 \cdot 10^{-166}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t}{\frac{\sqrt{\left(\left(\ell \cdot 2\right) \cdot \ell\right) \cdot \left(4 + \left(\frac{4}{x} - 2\right) \cdot \frac{4}{x}\right) + \left(t \cdot x\right) \cdot \left(t \cdot \left(8 + \frac{4}{x} \cdot \left(\frac{4}{x} \cdot \frac{4}{x}\right)\right)\right)}}{\sqrt{\left(\left(\frac{4}{x} \cdot \frac{4}{x} - 2 \cdot \frac{4}{x}\right) + 4\right) \cdot x}}}\\ \mathbf{elif}\;t \le 7.445703208013277 \cdot 10^{+140}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t}{\sqrt{\frac{\ell \cdot 2}{\frac{x}{\ell}} + \left(t \cdot \left(2 + \frac{4}{x}\right)\right) \cdot t}}\\ \mathbf{else}:\\ \;\;\;\;\frac{\sqrt{2} \cdot t}{\left(\frac{2 \cdot \frac{t}{\sqrt{2}}}{x \cdot x} - \frac{\frac{t}{\sqrt{2}}}{x \cdot x}\right) + \left(\sqrt{2} \cdot t + \frac{2 \cdot \frac{t}{\sqrt{2}}}{x}\right)}\\ \end{array}\]

Reproduce

herbie shell --seed 2019053 
(FPCore (x l t)
  :name "Toniolo and Linder, Equation (7)"
  (/ (* (sqrt 2) t) (sqrt (- (* (/ (+ x 1) (- x 1)) (+ (* l l) (* 2 (* t t)))) (* l l)))))