Maksimov and Kolovsky, Equation (4)

Percentage Accurate: 85.9% → 99.9%
Time: 3.9s
Alternatives: 11
Speedup: 1.2×

Specification

?
\[\begin{array}{l} \\ \left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (+ (* (* J (- (exp l) (exp (- l)))) (cos (/ K 2.0))) U))
double code(double J, double l, double K, double U) {
	return ((J * (exp(l) - exp(-l))) * cos((K / 2.0))) + U;
}
module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(j, l, k, u)
use fmin_fmax_functions
    real(8), intent (in) :: j
    real(8), intent (in) :: l
    real(8), intent (in) :: k
    real(8), intent (in) :: u
    code = ((j * (exp(l) - exp(-l))) * cos((k / 2.0d0))) + u
end function
public static double code(double J, double l, double K, double U) {
	return ((J * (Math.exp(l) - Math.exp(-l))) * Math.cos((K / 2.0))) + U;
}
def code(J, l, K, U):
	return ((J * (math.exp(l) - math.exp(-l))) * math.cos((K / 2.0))) + U
function code(J, l, K, U)
	return Float64(Float64(Float64(J * Float64(exp(l) - exp(Float64(-l)))) * cos(Float64(K / 2.0))) + U)
end
function tmp = code(J, l, K, U)
	tmp = ((J * (exp(l) - exp(-l))) * cos((K / 2.0))) + U;
end
code[J_, l_, K_, U_] := N[(N[(N[(J * N[(N[Exp[l], $MachinePrecision] - N[Exp[(-l)], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[Cos[N[(K / 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] + U), $MachinePrecision]
\begin{array}{l}

\\
\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U
\end{array}

Local Percentage Accuracy vs ?

The average percentage accuracy by input value. Horizontal axis shows value of an input variable; the variable is choosen in the title. Vertical axis is accuracy; higher is better. Red represent the original program, while blue represents Herbie's suggestion. These can be toggled with buttons below the plot. The line is an average while dots represent individual samples.

Accuracy vs Speed?

Herbie found 11 alternatives:

AlternativeAccuracySpeedup
The accuracy (vertical axis) and speed (horizontal axis) of each alternatives. Up and to the right is better. The red square shows the initial program, and each blue circle shows an alternative.The line shows the best available speed-accuracy tradeoffs.

Initial Program: 85.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (+ (* (* J (- (exp l) (exp (- l)))) (cos (/ K 2.0))) U))
double code(double J, double l, double K, double U) {
	return ((J * (exp(l) - exp(-l))) * cos((K / 2.0))) + U;
}
module fmin_fmax_functions
    implicit none
    private
    public fmax
    public fmin

    interface fmax
        module procedure fmax88
        module procedure fmax44
        module procedure fmax84
        module procedure fmax48
    end interface
    interface fmin
        module procedure fmin88
        module procedure fmin44
        module procedure fmin84
        module procedure fmin48
    end interface
contains
    real(8) function fmax88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(4) function fmax44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, max(x, y), y /= y), x /= x)
    end function
    real(8) function fmax84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmax48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
    end function
    real(8) function fmin88(x, y) result (res)
        real(8), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(4) function fmin44(x, y) result (res)
        real(4), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(y, merge(x, min(x, y), y /= y), x /= x)
    end function
    real(8) function fmin84(x, y) result(res)
        real(8), intent (in) :: x
        real(4), intent (in) :: y
        res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
    end function
    real(8) function fmin48(x, y) result(res)
        real(4), intent (in) :: x
        real(8), intent (in) :: y
        res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
    end function
end module

real(8) function code(j, l, k, u)
use fmin_fmax_functions
    real(8), intent (in) :: j
    real(8), intent (in) :: l
    real(8), intent (in) :: k
    real(8), intent (in) :: u
    code = ((j * (exp(l) - exp(-l))) * cos((k / 2.0d0))) + u
end function
public static double code(double J, double l, double K, double U) {
	return ((J * (Math.exp(l) - Math.exp(-l))) * Math.cos((K / 2.0))) + U;
}
def code(J, l, K, U):
	return ((J * (math.exp(l) - math.exp(-l))) * math.cos((K / 2.0))) + U
function code(J, l, K, U)
	return Float64(Float64(Float64(J * Float64(exp(l) - exp(Float64(-l)))) * cos(Float64(K / 2.0))) + U)
end
function tmp = code(J, l, K, U)
	tmp = ((J * (exp(l) - exp(-l))) * cos((K / 2.0))) + U;
end
code[J_, l_, K_, U_] := N[(N[(N[(J * N[(N[Exp[l], $MachinePrecision] - N[Exp[(-l)], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[Cos[N[(K / 2.0), $MachinePrecision]], $MachinePrecision]), $MachinePrecision] + U), $MachinePrecision]
\begin{array}{l}

\\
\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U
\end{array}

Alternative 1: 99.9% accurate, 1.2× speedup?

\[\begin{array}{l} \\ \mathsf{fma}\left(\left(\cos \left(-0.5 \cdot K\right) \cdot J\right) \cdot \sinh \ell, 2, U\right) \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (fma (* (* (cos (* -0.5 K)) J) (sinh l)) 2.0 U))
double code(double J, double l, double K, double U) {
	return fma(((cos((-0.5 * K)) * J) * sinh(l)), 2.0, U);
}
function code(J, l, K, U)
	return fma(Float64(Float64(cos(Float64(-0.5 * K)) * J) * sinh(l)), 2.0, U)
end
code[J_, l_, K_, U_] := N[(N[(N[(N[Cos[N[(-0.5 * K), $MachinePrecision]], $MachinePrecision] * J), $MachinePrecision] * N[Sinh[l], $MachinePrecision]), $MachinePrecision] * 2.0 + U), $MachinePrecision]
\begin{array}{l}

\\
\mathsf{fma}\left(\left(\cos \left(-0.5 \cdot K\right) \cdot J\right) \cdot \sinh \ell, 2, U\right)
\end{array}
Derivation
  1. Initial program 85.9%

    \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
  2. Step-by-step derivation
    1. lift-+.f64N/A

      \[\leadsto \color{blue}{\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U} \]
    2. lift-*.f64N/A

      \[\leadsto \color{blue}{\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right)} + U \]
    3. *-commutativeN/A

      \[\leadsto \color{blue}{\cos \left(\frac{K}{2}\right) \cdot \left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right)} + U \]
    4. lift-*.f64N/A

      \[\leadsto \cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right)} + U \]
    5. associate-*r*N/A

      \[\leadsto \color{blue}{\left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \left(e^{\ell} - e^{-\ell}\right)} + U \]
    6. lift--.f64N/A

      \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \color{blue}{\left(e^{\ell} - e^{-\ell}\right)} + U \]
    7. lift-exp.f64N/A

      \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \left(\color{blue}{e^{\ell}} - e^{-\ell}\right) + U \]
    8. lift-exp.f64N/A

      \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \left(e^{\ell} - \color{blue}{e^{-\ell}}\right) + U \]
    9. lift-neg.f64N/A

      \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) + U \]
    10. sinh-undefN/A

      \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \color{blue}{\left(2 \cdot \sinh \ell\right)} + U \]
    11. *-commutativeN/A

      \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \color{blue}{\left(\sinh \ell \cdot 2\right)} + U \]
    12. associate-*r*N/A

      \[\leadsto \color{blue}{\left(\left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \sinh \ell\right) \cdot 2} + U \]
    13. lower-fma.f64N/A

      \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \sinh \ell, 2, U\right)} \]
  3. Applied rewrites99.9%

    \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\cos \left(-0.5 \cdot K\right) \cdot J\right) \cdot \sinh \ell, 2, U\right)} \]
  4. Add Preprocessing

Alternative 2: 88.6% accurate, 0.7× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\ \;\;\;\;\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \left(1 + -0.125 \cdot {K}^{2}\right) + U\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\ \end{array} \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (if (<= (cos (/ K 2.0)) -0.005)
   (+ (* (* J (- (exp l) (exp (- l)))) (+ 1.0 (* -0.125 (pow K 2.0)))) U)
   (fma (+ J J) (sinh l) U)))
double code(double J, double l, double K, double U) {
	double tmp;
	if (cos((K / 2.0)) <= -0.005) {
		tmp = ((J * (exp(l) - exp(-l))) * (1.0 + (-0.125 * pow(K, 2.0)))) + U;
	} else {
		tmp = fma((J + J), sinh(l), U);
	}
	return tmp;
}
function code(J, l, K, U)
	tmp = 0.0
	if (cos(Float64(K / 2.0)) <= -0.005)
		tmp = Float64(Float64(Float64(J * Float64(exp(l) - exp(Float64(-l)))) * Float64(1.0 + Float64(-0.125 * (K ^ 2.0)))) + U);
	else
		tmp = fma(Float64(J + J), sinh(l), U);
	end
	return tmp
end
code[J_, l_, K_, U_] := If[LessEqual[N[Cos[N[(K / 2.0), $MachinePrecision]], $MachinePrecision], -0.005], N[(N[(N[(J * N[(N[Exp[l], $MachinePrecision] - N[Exp[(-l)], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(1.0 + N[(-0.125 * N[Power[K, 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + U), $MachinePrecision], N[(N[(J + J), $MachinePrecision] * N[Sinh[l], $MachinePrecision] + U), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\
\;\;\;\;\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \left(1 + -0.125 \cdot {K}^{2}\right) + U\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (cos.f64 (/.f64 K #s(literal 2 binary64))) < -0.0050000000000000001

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \color{blue}{\left(1 + \frac{-1}{8} \cdot {K}^{2}\right)} + U \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto \left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \left(1 + \color{blue}{\frac{-1}{8} \cdot {K}^{2}}\right) + U \]
      2. lower-*.f64N/A

        \[\leadsto \left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \left(1 + \frac{-1}{8} \cdot \color{blue}{{K}^{2}}\right) + U \]
      3. lower-pow.f6464.2

        \[\leadsto \left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \left(1 + -0.125 \cdot {K}^{\color{blue}{2}}\right) + U \]
    4. Applied rewrites64.2%

      \[\leadsto \left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \color{blue}{\left(1 + -0.125 \cdot {K}^{2}\right)} + U \]

    if -0.0050000000000000001 < (cos.f64 (/.f64 K #s(literal 2 binary64)))

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      2. lower-*.f64N/A

        \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. lower--.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
      4. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
      5. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
      6. lower-neg.f6473.0

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
    4. Applied rewrites73.0%

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
    5. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
      2. +-commutativeN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
      3. add-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
      4. sub-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      6. lift--.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      7. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      9. lift-neg.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      10. sinh-undefN/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      11. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      12. associate-*r*N/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      13. *-commutativeN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
      14. remove-double-negN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      15. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
      16. count-2-revN/A

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
      17. lower-+.f6480.5

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
    6. Applied rewrites80.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 3: 87.7% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\ \;\;\;\;\mathsf{fma}\left(\sinh \ell \cdot \mathsf{fma}\left(K \cdot K, -0.125, 1\right), J + J, U\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\ \end{array} \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (if (<= (cos (/ K 2.0)) -0.005)
   (fma (* (sinh l) (fma (* K K) -0.125 1.0)) (+ J J) U)
   (fma (+ J J) (sinh l) U)))
double code(double J, double l, double K, double U) {
	double tmp;
	if (cos((K / 2.0)) <= -0.005) {
		tmp = fma((sinh(l) * fma((K * K), -0.125, 1.0)), (J + J), U);
	} else {
		tmp = fma((J + J), sinh(l), U);
	}
	return tmp;
}
function code(J, l, K, U)
	tmp = 0.0
	if (cos(Float64(K / 2.0)) <= -0.005)
		tmp = fma(Float64(sinh(l) * fma(Float64(K * K), -0.125, 1.0)), Float64(J + J), U);
	else
		tmp = fma(Float64(J + J), sinh(l), U);
	end
	return tmp
end
code[J_, l_, K_, U_] := If[LessEqual[N[Cos[N[(K / 2.0), $MachinePrecision]], $MachinePrecision], -0.005], N[(N[(N[Sinh[l], $MachinePrecision] * N[(N[(K * K), $MachinePrecision] * -0.125 + 1.0), $MachinePrecision]), $MachinePrecision] * N[(J + J), $MachinePrecision] + U), $MachinePrecision], N[(N[(J + J), $MachinePrecision] * N[Sinh[l], $MachinePrecision] + U), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\
\;\;\;\;\mathsf{fma}\left(\sinh \ell \cdot \mathsf{fma}\left(K \cdot K, -0.125, 1\right), J + J, U\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (cos.f64 (/.f64 K #s(literal 2 binary64))) < -0.0050000000000000001

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto \color{blue}{\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U} \]
      2. lift-*.f64N/A

        \[\leadsto \color{blue}{\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right)} + U \]
      3. *-commutativeN/A

        \[\leadsto \color{blue}{\cos \left(\frac{K}{2}\right) \cdot \left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right)} + U \]
      4. lift-*.f64N/A

        \[\leadsto \cos \left(\frac{K}{2}\right) \cdot \color{blue}{\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right)} + U \]
      5. associate-*r*N/A

        \[\leadsto \color{blue}{\left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \left(e^{\ell} - e^{-\ell}\right)} + U \]
      6. lift--.f64N/A

        \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \color{blue}{\left(e^{\ell} - e^{-\ell}\right)} + U \]
      7. lift-exp.f64N/A

        \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \left(\color{blue}{e^{\ell}} - e^{-\ell}\right) + U \]
      8. lift-exp.f64N/A

        \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \left(e^{\ell} - \color{blue}{e^{-\ell}}\right) + U \]
      9. lift-neg.f64N/A

        \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) + U \]
      10. sinh-undefN/A

        \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \color{blue}{\left(2 \cdot \sinh \ell\right)} + U \]
      11. *-commutativeN/A

        \[\leadsto \left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \color{blue}{\left(\sinh \ell \cdot 2\right)} + U \]
      12. associate-*r*N/A

        \[\leadsto \color{blue}{\left(\left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \sinh \ell\right) \cdot 2} + U \]
      13. lower-fma.f64N/A

        \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\cos \left(\frac{K}{2}\right) \cdot J\right) \cdot \sinh \ell, 2, U\right)} \]
    3. Applied rewrites99.9%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\left(\cos \left(-0.5 \cdot K\right) \cdot J\right) \cdot \sinh \ell, 2, U\right)} \]
    4. Taylor expanded in K around 0

      \[\leadsto \mathsf{fma}\left(\left(\color{blue}{\left(1 + \frac{-1}{8} \cdot {K}^{2}\right)} \cdot J\right) \cdot \sinh \ell, 2, U\right) \]
    5. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto \mathsf{fma}\left(\left(\left(1 + \color{blue}{\frac{-1}{8} \cdot {K}^{2}}\right) \cdot J\right) \cdot \sinh \ell, 2, U\right) \]
      2. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\left(\left(1 + \frac{-1}{8} \cdot \color{blue}{{K}^{2}}\right) \cdot J\right) \cdot \sinh \ell, 2, U\right) \]
      3. lower-pow.f6468.7

        \[\leadsto \mathsf{fma}\left(\left(\left(1 + -0.125 \cdot {K}^{\color{blue}{2}}\right) \cdot J\right) \cdot \sinh \ell, 2, U\right) \]
    6. Applied rewrites68.7%

      \[\leadsto \mathsf{fma}\left(\left(\color{blue}{\left(1 + -0.125 \cdot {K}^{2}\right)} \cdot J\right) \cdot \sinh \ell, 2, U\right) \]
    7. Step-by-step derivation
      1. lift-fma.f64N/A

        \[\leadsto \color{blue}{\left(\left(\left(1 + \frac{-1}{8} \cdot {K}^{2}\right) \cdot J\right) \cdot \sinh \ell\right) \cdot 2 + U} \]
      2. *-commutativeN/A

        \[\leadsto \color{blue}{2 \cdot \left(\left(\left(1 + \frac{-1}{8} \cdot {K}^{2}\right) \cdot J\right) \cdot \sinh \ell\right)} + U \]
    8. Applied rewrites69.2%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\sinh \ell \cdot \mathsf{fma}\left(K \cdot K, -0.125, 1\right), J + J, U\right)} \]

    if -0.0050000000000000001 < (cos.f64 (/.f64 K #s(literal 2 binary64)))

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      2. lower-*.f64N/A

        \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. lower--.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
      4. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
      5. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
      6. lower-neg.f6473.0

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
    4. Applied rewrites73.0%

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
    5. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
      2. +-commutativeN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
      3. add-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
      4. sub-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      6. lift--.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      7. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      9. lift-neg.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      10. sinh-undefN/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      11. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      12. associate-*r*N/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      13. *-commutativeN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
      14. remove-double-negN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      15. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
      16. count-2-revN/A

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
      17. lower-+.f6480.5

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
    6. Applied rewrites80.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 4: 87.2% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\ \;\;\;\;\mathsf{fma}\left(\frac{J}{e^{\ell}}, \ell \cdot \left(2 + 2 \cdot \ell\right), U\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\ \end{array} \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (if (<= (cos (/ K 2.0)) -0.005)
   (fma (/ J (exp l)) (* l (+ 2.0 (* 2.0 l))) U)
   (fma (+ J J) (sinh l) U)))
double code(double J, double l, double K, double U) {
	double tmp;
	if (cos((K / 2.0)) <= -0.005) {
		tmp = fma((J / exp(l)), (l * (2.0 + (2.0 * l))), U);
	} else {
		tmp = fma((J + J), sinh(l), U);
	}
	return tmp;
}
function code(J, l, K, U)
	tmp = 0.0
	if (cos(Float64(K / 2.0)) <= -0.005)
		tmp = fma(Float64(J / exp(l)), Float64(l * Float64(2.0 + Float64(2.0 * l))), U);
	else
		tmp = fma(Float64(J + J), sinh(l), U);
	end
	return tmp
end
code[J_, l_, K_, U_] := If[LessEqual[N[Cos[N[(K / 2.0), $MachinePrecision]], $MachinePrecision], -0.005], N[(N[(J / N[Exp[l], $MachinePrecision]), $MachinePrecision] * N[(l * N[(2.0 + N[(2.0 * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + U), $MachinePrecision], N[(N[(J + J), $MachinePrecision] * N[Sinh[l], $MachinePrecision] + U), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\
\;\;\;\;\mathsf{fma}\left(\frac{J}{e^{\ell}}, \ell \cdot \left(2 + 2 \cdot \ell\right), U\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (cos.f64 (/.f64 K #s(literal 2 binary64))) < -0.0050000000000000001

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      2. lower-*.f64N/A

        \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. lower--.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
      4. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
      5. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
      6. lower-neg.f6473.0

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
    4. Applied rewrites73.0%

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
    5. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
      2. +-commutativeN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
      3. add-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
      4. sub-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      6. lift--.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      7. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      9. lift-neg.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      10. sinh-undefN/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      11. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      12. associate-*r*N/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      13. *-commutativeN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
      14. remove-double-negN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      15. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
      16. count-2-revN/A

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
      17. lower-+.f6480.5

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
    6. Applied rewrites80.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
    7. Step-by-step derivation
      1. lift-fma.f64N/A

        \[\leadsto \left(J + J\right) \cdot \sinh \ell + \color{blue}{U} \]
      2. lift-+.f64N/A

        \[\leadsto \left(J + J\right) \cdot \sinh \ell + U \]
      3. count-2N/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      4. *-commutativeN/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + U \]
      5. associate-*r*N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + U \]
      6. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + U \]
      7. sinh-undefN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + U \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + U \]
      9. exp-negN/A

        \[\leadsto J \cdot \left(e^{\ell} - \frac{1}{e^{\ell}}\right) + U \]
      10. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - \frac{1}{e^{\ell}}\right) + U \]
      11. sub-to-fractionN/A

        \[\leadsto J \cdot \frac{e^{\ell} \cdot e^{\ell} - 1}{e^{\ell}} + U \]
      12. lift-exp.f64N/A

        \[\leadsto J \cdot \frac{e^{\ell} \cdot e^{\ell} - 1}{e^{\ell}} + U \]
      13. lift-exp.f64N/A

        \[\leadsto J \cdot \frac{e^{\ell} \cdot e^{\ell} - 1}{e^{\ell}} + U \]
      14. exp-sumN/A

        \[\leadsto J \cdot \frac{e^{\ell + \ell} - 1}{e^{\ell}} + U \]
      15. lift-+.f64N/A

        \[\leadsto J \cdot \frac{e^{\ell + \ell} - 1}{e^{\ell}} + U \]
      16. lift-expm1.f64N/A

        \[\leadsto J \cdot \frac{\mathsf{expm1}\left(\ell + \ell\right)}{e^{\ell}} + U \]
      17. associate-/l*N/A

        \[\leadsto \frac{J \cdot \mathsf{expm1}\left(\ell + \ell\right)}{e^{\ell}} + U \]
      18. *-commutativeN/A

        \[\leadsto \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{e^{\ell}} + U \]
      19. associate-/l*N/A

        \[\leadsto \mathsf{expm1}\left(\ell + \ell\right) \cdot \frac{J}{e^{\ell}} + U \]
      20. *-commutativeN/A

        \[\leadsto \frac{J}{e^{\ell}} \cdot \mathsf{expm1}\left(\ell + \ell\right) + U \]
    8. Applied rewrites62.6%

      \[\leadsto \mathsf{fma}\left(\frac{J}{e^{\ell}}, \color{blue}{\mathsf{expm1}\left(\ell + \ell\right)}, U\right) \]
    9. Taylor expanded in l around 0

      \[\leadsto \mathsf{fma}\left(\frac{J}{e^{\ell}}, \ell \cdot \color{blue}{\left(2 + 2 \cdot \ell\right)}, U\right) \]
    10. Step-by-step derivation
      1. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\frac{J}{e^{\ell}}, \ell \cdot \left(2 + \color{blue}{2 \cdot \ell}\right), U\right) \]
      2. lower-+.f64N/A

        \[\leadsto \mathsf{fma}\left(\frac{J}{e^{\ell}}, \ell \cdot \left(2 + 2 \cdot \color{blue}{\ell}\right), U\right) \]
      3. lower-*.f6449.3

        \[\leadsto \mathsf{fma}\left(\frac{J}{e^{\ell}}, \ell \cdot \left(2 + 2 \cdot \ell\right), U\right) \]
    11. Applied rewrites49.3%

      \[\leadsto \mathsf{fma}\left(\frac{J}{e^{\ell}}, \ell \cdot \color{blue}{\left(2 + 2 \cdot \ell\right)}, U\right) \]

    if -0.0050000000000000001 < (cos.f64 (/.f64 K #s(literal 2 binary64)))

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      2. lower-*.f64N/A

        \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. lower--.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
      4. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
      5. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
      6. lower-neg.f6473.0

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
    4. Applied rewrites73.0%

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
    5. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
      2. +-commutativeN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
      3. add-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
      4. sub-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      6. lift--.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      7. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      9. lift-neg.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      10. sinh-undefN/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      11. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      12. associate-*r*N/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      13. *-commutativeN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
      14. remove-double-negN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      15. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
      16. count-2-revN/A

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
      17. lower-+.f6480.5

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
    6. Applied rewrites80.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 5: 86.3% accurate, 1.1× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\ \;\;\;\;\mathsf{fma}\left(J + -1 \cdot \left(J \cdot \ell\right), \mathsf{expm1}\left(\ell + \ell\right), U\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\ \end{array} \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (if (<= (cos (/ K 2.0)) -0.005)
   (fma (+ J (* -1.0 (* J l))) (expm1 (+ l l)) U)
   (fma (+ J J) (sinh l) U)))
double code(double J, double l, double K, double U) {
	double tmp;
	if (cos((K / 2.0)) <= -0.005) {
		tmp = fma((J + (-1.0 * (J * l))), expm1((l + l)), U);
	} else {
		tmp = fma((J + J), sinh(l), U);
	}
	return tmp;
}
function code(J, l, K, U)
	tmp = 0.0
	if (cos(Float64(K / 2.0)) <= -0.005)
		tmp = fma(Float64(J + Float64(-1.0 * Float64(J * l))), expm1(Float64(l + l)), U);
	else
		tmp = fma(Float64(J + J), sinh(l), U);
	end
	return tmp
end
code[J_, l_, K_, U_] := If[LessEqual[N[Cos[N[(K / 2.0), $MachinePrecision]], $MachinePrecision], -0.005], N[(N[(J + N[(-1.0 * N[(J * l), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] * N[(Exp[N[(l + l), $MachinePrecision]] - 1), $MachinePrecision] + U), $MachinePrecision], N[(N[(J + J), $MachinePrecision] * N[Sinh[l], $MachinePrecision] + U), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\
\;\;\;\;\mathsf{fma}\left(J + -1 \cdot \left(J \cdot \ell\right), \mathsf{expm1}\left(\ell + \ell\right), U\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (cos.f64 (/.f64 K #s(literal 2 binary64))) < -0.0050000000000000001

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      2. lower-*.f64N/A

        \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. lower--.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
      4. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
      5. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
      6. lower-neg.f6473.0

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
    4. Applied rewrites73.0%

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
    5. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
      2. +-commutativeN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
      3. add-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
      4. sub-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      6. lift--.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      7. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      9. lift-neg.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      10. sinh-undefN/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      11. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      12. associate-*r*N/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      13. *-commutativeN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
      14. remove-double-negN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      15. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
      16. count-2-revN/A

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
      17. lower-+.f6480.5

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
    6. Applied rewrites80.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
    7. Step-by-step derivation
      1. lift-fma.f64N/A

        \[\leadsto \left(J + J\right) \cdot \sinh \ell + \color{blue}{U} \]
      2. lift-+.f64N/A

        \[\leadsto \left(J + J\right) \cdot \sinh \ell + U \]
      3. count-2N/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      4. *-commutativeN/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + U \]
      5. associate-*r*N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + U \]
      6. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + U \]
      7. sinh-undefN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + U \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + U \]
      9. exp-negN/A

        \[\leadsto J \cdot \left(e^{\ell} - \frac{1}{e^{\ell}}\right) + U \]
      10. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - \frac{1}{e^{\ell}}\right) + U \]
      11. sub-to-fractionN/A

        \[\leadsto J \cdot \frac{e^{\ell} \cdot e^{\ell} - 1}{e^{\ell}} + U \]
      12. lift-exp.f64N/A

        \[\leadsto J \cdot \frac{e^{\ell} \cdot e^{\ell} - 1}{e^{\ell}} + U \]
      13. lift-exp.f64N/A

        \[\leadsto J \cdot \frac{e^{\ell} \cdot e^{\ell} - 1}{e^{\ell}} + U \]
      14. exp-sumN/A

        \[\leadsto J \cdot \frac{e^{\ell + \ell} - 1}{e^{\ell}} + U \]
      15. lift-+.f64N/A

        \[\leadsto J \cdot \frac{e^{\ell + \ell} - 1}{e^{\ell}} + U \]
      16. lift-expm1.f64N/A

        \[\leadsto J \cdot \frac{\mathsf{expm1}\left(\ell + \ell\right)}{e^{\ell}} + U \]
      17. associate-/l*N/A

        \[\leadsto \frac{J \cdot \mathsf{expm1}\left(\ell + \ell\right)}{e^{\ell}} + U \]
      18. *-commutativeN/A

        \[\leadsto \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{e^{\ell}} + U \]
      19. associate-/l*N/A

        \[\leadsto \mathsf{expm1}\left(\ell + \ell\right) \cdot \frac{J}{e^{\ell}} + U \]
      20. *-commutativeN/A

        \[\leadsto \frac{J}{e^{\ell}} \cdot \mathsf{expm1}\left(\ell + \ell\right) + U \]
    8. Applied rewrites62.6%

      \[\leadsto \mathsf{fma}\left(\frac{J}{e^{\ell}}, \color{blue}{\mathsf{expm1}\left(\ell + \ell\right)}, U\right) \]
    9. Taylor expanded in l around 0

      \[\leadsto \mathsf{fma}\left(J + -1 \cdot \left(J \cdot \ell\right), \mathsf{expm1}\left(\color{blue}{\ell + \ell}\right), U\right) \]
    10. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto \mathsf{fma}\left(J + -1 \cdot \left(J \cdot \ell\right), \mathsf{expm1}\left(\ell + \color{blue}{\ell}\right), U\right) \]
      2. lower-*.f64N/A

        \[\leadsto \mathsf{fma}\left(J + -1 \cdot \left(J \cdot \ell\right), \mathsf{expm1}\left(\ell + \ell\right), U\right) \]
      3. lower-*.f6455.8

        \[\leadsto \mathsf{fma}\left(J + -1 \cdot \left(J \cdot \ell\right), \mathsf{expm1}\left(\ell + \ell\right), U\right) \]
    11. Applied rewrites55.8%

      \[\leadsto \mathsf{fma}\left(J + -1 \cdot \left(J \cdot \ell\right), \mathsf{expm1}\left(\color{blue}{\ell + \ell}\right), U\right) \]

    if -0.0050000000000000001 < (cos.f64 (/.f64 K #s(literal 2 binary64)))

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      2. lower-*.f64N/A

        \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. lower--.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
      4. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
      5. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
      6. lower-neg.f6473.0

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
    4. Applied rewrites73.0%

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
    5. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
      2. +-commutativeN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
      3. add-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
      4. sub-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      6. lift--.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      7. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      9. lift-neg.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      10. sinh-undefN/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      11. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      12. associate-*r*N/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      13. *-commutativeN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
      14. remove-double-negN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      15. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
      16. count-2-revN/A

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
      17. lower-+.f6480.5

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
    6. Applied rewrites80.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 6: 86.3% accurate, 1.1× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\ \;\;\;\;2 \cdot \left(J \cdot \left(\ell + -0.125 \cdot \left(\left(\ell \cdot K\right) \cdot K\right)\right)\right) + U\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\ \end{array} \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (if (<= (cos (/ K 2.0)) -0.005)
   (+ (* 2.0 (* J (+ l (* -0.125 (* (* l K) K))))) U)
   (fma (+ J J) (sinh l) U)))
double code(double J, double l, double K, double U) {
	double tmp;
	if (cos((K / 2.0)) <= -0.005) {
		tmp = (2.0 * (J * (l + (-0.125 * ((l * K) * K))))) + U;
	} else {
		tmp = fma((J + J), sinh(l), U);
	}
	return tmp;
}
function code(J, l, K, U)
	tmp = 0.0
	if (cos(Float64(K / 2.0)) <= -0.005)
		tmp = Float64(Float64(2.0 * Float64(J * Float64(l + Float64(-0.125 * Float64(Float64(l * K) * K))))) + U);
	else
		tmp = fma(Float64(J + J), sinh(l), U);
	end
	return tmp
end
code[J_, l_, K_, U_] := If[LessEqual[N[Cos[N[(K / 2.0), $MachinePrecision]], $MachinePrecision], -0.005], N[(N[(2.0 * N[(J * N[(l + N[(-0.125 * N[(N[(l * K), $MachinePrecision] * K), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + U), $MachinePrecision], N[(N[(J + J), $MachinePrecision] * N[Sinh[l], $MachinePrecision] + U), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\
\;\;\;\;2 \cdot \left(J \cdot \left(\ell + -0.125 \cdot \left(\left(\ell \cdot K\right) \cdot K\right)\right)\right) + U\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (cos.f64 (/.f64 K #s(literal 2 binary64))) < -0.0050000000000000001

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in l around 0

      \[\leadsto \color{blue}{2 \cdot \left(J \cdot \left(\ell \cdot \cos \left(\frac{1}{2} \cdot K\right)\right)\right)} + U \]
    3. Step-by-step derivation
      1. lower-*.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(J \cdot \left(\ell \cdot \cos \left(\frac{1}{2} \cdot K\right)\right)\right)} + U \]
      2. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \color{blue}{\left(\ell \cdot \cos \left(\frac{1}{2} \cdot K\right)\right)}\right) + U \]
      3. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell \cdot \color{blue}{\cos \left(\frac{1}{2} \cdot K\right)}\right)\right) + U \]
      4. lower-cos.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell \cdot \cos \left(\frac{1}{2} \cdot K\right)\right)\right) + U \]
      5. lower-*.f6464.7

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell \cdot \cos \left(0.5 \cdot K\right)\right)\right) + U \]
    4. Applied rewrites64.7%

      \[\leadsto \color{blue}{2 \cdot \left(J \cdot \left(\ell \cdot \cos \left(0.5 \cdot K\right)\right)\right)} + U \]
    5. Taylor expanded in K around 0

      \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \color{blue}{\frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)}\right)\right) + U \]
    6. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \color{blue}{\left({K}^{2} \cdot \ell\right)}\right)\right) + U \]
      2. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left({K}^{2} \cdot \color{blue}{\ell}\right)\right)\right) + U \]
      3. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)\right)\right) + U \]
      4. lower-pow.f6449.9

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + -0.125 \cdot \left({K}^{2} \cdot \ell\right)\right)\right) + U \]
    7. Applied rewrites49.9%

      \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \color{blue}{-0.125 \cdot \left({K}^{2} \cdot \ell\right)}\right)\right) + U \]
    8. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)\right)\right) + U \]
      2. *-commutativeN/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left(\ell \cdot {K}^{\color{blue}{2}}\right)\right)\right) + U \]
      3. lift-pow.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left(\ell \cdot {K}^{2}\right)\right)\right) + U \]
      4. unpow2N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left(\ell \cdot \left(K \cdot K\right)\right)\right)\right) + U \]
      5. associate-*r*N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left(\left(\ell \cdot K\right) \cdot K\right)\right)\right) + U \]
      6. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left(\left(\ell \cdot K\right) \cdot K\right)\right)\right) + U \]
      7. lower-*.f6451.2

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + -0.125 \cdot \left(\left(\ell \cdot K\right) \cdot K\right)\right)\right) + U \]
    9. Applied rewrites51.2%

      \[\leadsto 2 \cdot \left(J \cdot \left(\ell + -0.125 \cdot \left(\left(\ell \cdot K\right) \cdot K\right)\right)\right) + U \]

    if -0.0050000000000000001 < (cos.f64 (/.f64 K #s(literal 2 binary64)))

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      2. lower-*.f64N/A

        \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. lower--.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
      4. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
      5. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
      6. lower-neg.f6473.0

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
    4. Applied rewrites73.0%

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
    5. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
      2. +-commutativeN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
      3. add-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
      4. sub-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      6. lift--.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      7. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      9. lift-neg.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      10. sinh-undefN/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      11. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      12. associate-*r*N/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      13. *-commutativeN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
      14. remove-double-negN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      15. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
      16. count-2-revN/A

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
      17. lower-+.f6480.5

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
    6. Applied rewrites80.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 7: 85.7% accurate, 1.1× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\ \;\;\;\;\left(J + J\right) \cdot \mathsf{fma}\left(\left(K \cdot K\right) \cdot \ell, -0.125, \ell\right) + U\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\ \end{array} \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (if (<= (cos (/ K 2.0)) -0.005)
   (+ (* (+ J J) (fma (* (* K K) l) -0.125 l)) U)
   (fma (+ J J) (sinh l) U)))
double code(double J, double l, double K, double U) {
	double tmp;
	if (cos((K / 2.0)) <= -0.005) {
		tmp = ((J + J) * fma(((K * K) * l), -0.125, l)) + U;
	} else {
		tmp = fma((J + J), sinh(l), U);
	}
	return tmp;
}
function code(J, l, K, U)
	tmp = 0.0
	if (cos(Float64(K / 2.0)) <= -0.005)
		tmp = Float64(Float64(Float64(J + J) * fma(Float64(Float64(K * K) * l), -0.125, l)) + U);
	else
		tmp = fma(Float64(J + J), sinh(l), U);
	end
	return tmp
end
code[J_, l_, K_, U_] := If[LessEqual[N[Cos[N[(K / 2.0), $MachinePrecision]], $MachinePrecision], -0.005], N[(N[(N[(J + J), $MachinePrecision] * N[(N[(N[(K * K), $MachinePrecision] * l), $MachinePrecision] * -0.125 + l), $MachinePrecision]), $MachinePrecision] + U), $MachinePrecision], N[(N[(J + J), $MachinePrecision] * N[Sinh[l], $MachinePrecision] + U), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\cos \left(\frac{K}{2}\right) \leq -0.005:\\
\;\;\;\;\left(J + J\right) \cdot \mathsf{fma}\left(\left(K \cdot K\right) \cdot \ell, -0.125, \ell\right) + U\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(J + J, \sinh \ell, U\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if (cos.f64 (/.f64 K #s(literal 2 binary64))) < -0.0050000000000000001

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in l around 0

      \[\leadsto \color{blue}{2 \cdot \left(J \cdot \left(\ell \cdot \cos \left(\frac{1}{2} \cdot K\right)\right)\right)} + U \]
    3. Step-by-step derivation
      1. lower-*.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(J \cdot \left(\ell \cdot \cos \left(\frac{1}{2} \cdot K\right)\right)\right)} + U \]
      2. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \color{blue}{\left(\ell \cdot \cos \left(\frac{1}{2} \cdot K\right)\right)}\right) + U \]
      3. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell \cdot \color{blue}{\cos \left(\frac{1}{2} \cdot K\right)}\right)\right) + U \]
      4. lower-cos.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell \cdot \cos \left(\frac{1}{2} \cdot K\right)\right)\right) + U \]
      5. lower-*.f6464.7

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell \cdot \cos \left(0.5 \cdot K\right)\right)\right) + U \]
    4. Applied rewrites64.7%

      \[\leadsto \color{blue}{2 \cdot \left(J \cdot \left(\ell \cdot \cos \left(0.5 \cdot K\right)\right)\right)} + U \]
    5. Taylor expanded in K around 0

      \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \color{blue}{\frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)}\right)\right) + U \]
    6. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \color{blue}{\left({K}^{2} \cdot \ell\right)}\right)\right) + U \]
      2. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left({K}^{2} \cdot \color{blue}{\ell}\right)\right)\right) + U \]
      3. lower-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)\right)\right) + U \]
      4. lower-pow.f6449.9

        \[\leadsto 2 \cdot \left(J \cdot \left(\ell + -0.125 \cdot \left({K}^{2} \cdot \ell\right)\right)\right) + U \]
    7. Applied rewrites49.9%

      \[\leadsto 2 \cdot \left(J \cdot \left(\ell + \color{blue}{-0.125 \cdot \left({K}^{2} \cdot \ell\right)}\right)\right) + U \]
    8. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto 2 \cdot \color{blue}{\left(J \cdot \left(\ell + \frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)\right)\right)} + U \]
      2. lift-*.f64N/A

        \[\leadsto 2 \cdot \left(J \cdot \color{blue}{\left(\ell + \frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)\right)}\right) + U \]
      3. associate-*r*N/A

        \[\leadsto \left(2 \cdot J\right) \cdot \color{blue}{\left(\ell + \frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)\right)} + U \]
      4. count-2N/A

        \[\leadsto \left(J + J\right) \cdot \left(\color{blue}{\ell} + \frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)\right) + U \]
      5. lift-+.f64N/A

        \[\leadsto \left(J + J\right) \cdot \left(\color{blue}{\ell} + \frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right)\right) + U \]
      6. lower-*.f6449.8

        \[\leadsto \left(J + J\right) \cdot \color{blue}{\left(\ell + -0.125 \cdot \left({K}^{2} \cdot \ell\right)\right)} + U \]
      7. lift-+.f64N/A

        \[\leadsto \left(J + J\right) \cdot \left(\ell + \frac{-1}{8} \cdot \color{blue}{\left({K}^{2} \cdot \ell\right)}\right) + U \]
      8. +-commutativeN/A

        \[\leadsto \left(J + J\right) \cdot \left(\frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right) + \ell\right) + U \]
      9. lift-*.f64N/A

        \[\leadsto \left(J + J\right) \cdot \left(\frac{-1}{8} \cdot \left({K}^{2} \cdot \ell\right) + \ell\right) + U \]
      10. *-commutativeN/A

        \[\leadsto \left(J + J\right) \cdot \left(\left({K}^{2} \cdot \ell\right) \cdot \frac{-1}{8} + \ell\right) + U \]
      11. lower-fma.f6449.8

        \[\leadsto \left(J + J\right) \cdot \mathsf{fma}\left({K}^{2} \cdot \ell, -0.125, \ell\right) + U \]
      12. lift-pow.f64N/A

        \[\leadsto \left(J + J\right) \cdot \mathsf{fma}\left({K}^{2} \cdot \ell, \frac{-1}{8}, \ell\right) + U \]
      13. unpow2N/A

        \[\leadsto \left(J + J\right) \cdot \mathsf{fma}\left(\left(K \cdot K\right) \cdot \ell, \frac{-1}{8}, \ell\right) + U \]
      14. lower-*.f6449.8

        \[\leadsto \left(J + J\right) \cdot \mathsf{fma}\left(\left(K \cdot K\right) \cdot \ell, -0.125, \ell\right) + U \]
    9. Applied rewrites49.8%

      \[\leadsto \left(J + J\right) \cdot \color{blue}{\mathsf{fma}\left(\left(K \cdot K\right) \cdot \ell, -0.125, \ell\right)} + U \]

    if -0.0050000000000000001 < (cos.f64 (/.f64 K #s(literal 2 binary64)))

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      2. lower-*.f64N/A

        \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. lower--.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
      4. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
      5. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
      6. lower-neg.f6473.0

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
    4. Applied rewrites73.0%

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
    5. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
      2. +-commutativeN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
      3. add-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
      4. sub-flipN/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
      5. lift-*.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      6. lift--.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      7. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      8. lift-exp.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      9. lift-neg.f64N/A

        \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      10. sinh-undefN/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      11. lift-sinh.f64N/A

        \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
      12. associate-*r*N/A

        \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
      13. *-commutativeN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
      14. remove-double-negN/A

        \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
      15. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
      16. count-2-revN/A

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
      17. lower-+.f6480.5

        \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
    6. Applied rewrites80.5%

      \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 8: 80.3% accurate, 2.9× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\ell \leq -0.43:\\ \;\;\;\;\mathsf{fma}\left(1 - e^{-\ell}, J, U\right)\\ \mathbf{else}:\\ \;\;\;\;U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{1}\\ \end{array} \end{array} \]
(FPCore (J l K U)
 :precision binary64
 (if (<= l -0.43)
   (fma (- 1.0 (exp (- l))) J U)
   (+ U (/ (* (expm1 (+ l l)) J) 1.0))))
double code(double J, double l, double K, double U) {
	double tmp;
	if (l <= -0.43) {
		tmp = fma((1.0 - exp(-l)), J, U);
	} else {
		tmp = U + ((expm1((l + l)) * J) / 1.0);
	}
	return tmp;
}
function code(J, l, K, U)
	tmp = 0.0
	if (l <= -0.43)
		tmp = fma(Float64(1.0 - exp(Float64(-l))), J, U);
	else
		tmp = Float64(U + Float64(Float64(expm1(Float64(l + l)) * J) / 1.0));
	end
	return tmp
end
code[J_, l_, K_, U_] := If[LessEqual[l, -0.43], N[(N[(1.0 - N[Exp[(-l)], $MachinePrecision]), $MachinePrecision] * J + U), $MachinePrecision], N[(U + N[(N[(N[(Exp[N[(l + l), $MachinePrecision]] - 1), $MachinePrecision] * J), $MachinePrecision] / 1.0), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\ell \leq -0.43:\\
\;\;\;\;\mathsf{fma}\left(1 - e^{-\ell}, J, U\right)\\

\mathbf{else}:\\
\;\;\;\;U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{1}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if l < -0.429999999999999993

    1. Initial program 85.9%

      \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
    2. Taylor expanded in K around 0

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
    3. Step-by-step derivation
      1. lower-+.f64N/A

        \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      2. lower-*.f64N/A

        \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. lower--.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
      4. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
      5. lower-exp.f64N/A

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
      6. lower-neg.f6473.0

        \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
    4. Applied rewrites73.0%

      \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
    5. Taylor expanded in l around 0

      \[\leadsto U + J \cdot \left(1 - e^{\color{blue}{-\ell}}\right) \]
    6. Step-by-step derivation
      1. Applied rewrites55.7%

        \[\leadsto U + J \cdot \left(1 - e^{\color{blue}{-\ell}}\right) \]
      2. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto U + \color{blue}{J \cdot \left(1 - e^{-\ell}\right)} \]
        2. +-commutativeN/A

          \[\leadsto J \cdot \left(1 - e^{-\ell}\right) + \color{blue}{U} \]
        3. lift-*.f64N/A

          \[\leadsto J \cdot \left(1 - e^{-\ell}\right) + U \]
        4. *-commutativeN/A

          \[\leadsto \left(1 - e^{-\ell}\right) \cdot J + U \]
        5. lower-fma.f6455.7

          \[\leadsto \mathsf{fma}\left(1 - e^{-\ell}, \color{blue}{J}, U\right) \]
      3. Applied rewrites55.7%

        \[\leadsto \mathsf{fma}\left(1 - e^{-\ell}, \color{blue}{J}, U\right) \]

      if -0.429999999999999993 < l

      1. Initial program 85.9%

        \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
      2. Taylor expanded in K around 0

        \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
      3. Step-by-step derivation
        1. lower-+.f64N/A

          \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
        2. lower-*.f64N/A

          \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
        3. lower--.f64N/A

          \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
        4. lower-exp.f64N/A

          \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
        5. lower-exp.f64N/A

          \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
        6. lower-neg.f6473.0

          \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
      4. Applied rewrites73.0%

        \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
      5. Step-by-step derivation
        1. lift-*.f64N/A

          \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{-\ell}\right)} \]
        2. *-commutativeN/A

          \[\leadsto U + \left(e^{\ell} - e^{-\ell}\right) \cdot \color{blue}{J} \]
        3. lift--.f64N/A

          \[\leadsto U + \left(e^{\ell} - e^{-\ell}\right) \cdot J \]
        4. lift-exp.f64N/A

          \[\leadsto U + \left(e^{\ell} - e^{-\ell}\right) \cdot J \]
        5. lift-neg.f64N/A

          \[\leadsto U + \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \cdot J \]
        6. exp-negN/A

          \[\leadsto U + \left(e^{\ell} - \frac{1}{e^{\ell}}\right) \cdot J \]
        7. lift-exp.f64N/A

          \[\leadsto U + \left(e^{\ell} - \frac{1}{e^{\ell}}\right) \cdot J \]
        8. sub-to-fractionN/A

          \[\leadsto U + \frac{e^{\ell} \cdot e^{\ell} - 1}{e^{\ell}} \cdot J \]
        9. associate-*l/N/A

          \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{\color{blue}{e^{\ell}}} \]
        10. lower-/.f64N/A

          \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{\color{blue}{e^{\ell}}} \]
        11. lower-*.f64N/A

          \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{e^{\color{blue}{\ell}}} \]
        12. lift-exp.f64N/A

          \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{e^{\ell}} \]
        13. lift-exp.f64N/A

          \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{e^{\ell}} \]
        14. exp-lft-sqr-revN/A

          \[\leadsto U + \frac{\left(e^{\ell \cdot 2} - 1\right) \cdot J}{e^{\ell}} \]
        15. *-commutativeN/A

          \[\leadsto U + \frac{\left(e^{2 \cdot \ell} - 1\right) \cdot J}{e^{\ell}} \]
        16. lift-*.f64N/A

          \[\leadsto U + \frac{\left(e^{2 \cdot \ell} - 1\right) \cdot J}{e^{\ell}} \]
        17. lower-expm1.f6462.6

          \[\leadsto U + \frac{\mathsf{expm1}\left(2 \cdot \ell\right) \cdot J}{e^{\ell}} \]
        18. lift-*.f64N/A

          \[\leadsto U + \frac{\mathsf{expm1}\left(2 \cdot \ell\right) \cdot J}{e^{\ell}} \]
        19. count-2-revN/A

          \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{e^{\ell}} \]
        20. lower-+.f6462.6

          \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{e^{\ell}} \]
      6. Applied rewrites62.6%

        \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{\color{blue}{e^{\ell}}} \]
      7. Taylor expanded in l around 0

        \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{1} \]
      8. Step-by-step derivation
        1. Applied rewrites61.9%

          \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{1} \]
      9. Recombined 2 regimes into one program.
      10. Add Preprocessing

      Alternative 9: 67.0% accurate, 2.9× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\ell \leq 7600:\\ \;\;\;\;\mathsf{fma}\left(J + J, \ell, U\right)\\ \mathbf{else}:\\ \;\;\;\;U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{1}\\ \end{array} \end{array} \]
      (FPCore (J l K U)
       :precision binary64
       (if (<= l 7600.0) (fma (+ J J) l U) (+ U (/ (* (expm1 (+ l l)) J) 1.0))))
      double code(double J, double l, double K, double U) {
      	double tmp;
      	if (l <= 7600.0) {
      		tmp = fma((J + J), l, U);
      	} else {
      		tmp = U + ((expm1((l + l)) * J) / 1.0);
      	}
      	return tmp;
      }
      
      function code(J, l, K, U)
      	tmp = 0.0
      	if (l <= 7600.0)
      		tmp = fma(Float64(J + J), l, U);
      	else
      		tmp = Float64(U + Float64(Float64(expm1(Float64(l + l)) * J) / 1.0));
      	end
      	return tmp
      end
      
      code[J_, l_, K_, U_] := If[LessEqual[l, 7600.0], N[(N[(J + J), $MachinePrecision] * l + U), $MachinePrecision], N[(U + N[(N[(N[(Exp[N[(l + l), $MachinePrecision]] - 1), $MachinePrecision] * J), $MachinePrecision] / 1.0), $MachinePrecision]), $MachinePrecision]]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;\ell \leq 7600:\\
      \;\;\;\;\mathsf{fma}\left(J + J, \ell, U\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{1}\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if l < 7600

        1. Initial program 85.9%

          \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
        2. Taylor expanded in K around 0

          \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
        3. Step-by-step derivation
          1. lower-+.f64N/A

            \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
          2. lower-*.f64N/A

            \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
          3. lower--.f64N/A

            \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
          4. lower-exp.f64N/A

            \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
          5. lower-exp.f64N/A

            \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
          6. lower-neg.f6473.0

            \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
        4. Applied rewrites73.0%

          \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
        5. Step-by-step derivation
          1. lift-+.f64N/A

            \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
          2. +-commutativeN/A

            \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
          3. add-flipN/A

            \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
          4. sub-flipN/A

            \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
          5. lift-*.f64N/A

            \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
          6. lift--.f64N/A

            \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
          7. lift-exp.f64N/A

            \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
          8. lift-exp.f64N/A

            \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
          9. lift-neg.f64N/A

            \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
          10. sinh-undefN/A

            \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
          11. lift-sinh.f64N/A

            \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
          12. associate-*r*N/A

            \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
          13. *-commutativeN/A

            \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
          14. remove-double-negN/A

            \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
          15. lower-fma.f64N/A

            \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
          16. count-2-revN/A

            \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
          17. lower-+.f6480.5

            \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
        6. Applied rewrites80.5%

          \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
        7. Taylor expanded in l around 0

          \[\leadsto \mathsf{fma}\left(J + J, \ell, U\right) \]
        8. Step-by-step derivation
          1. Applied rewrites54.5%

            \[\leadsto \mathsf{fma}\left(J + J, \ell, U\right) \]

          if 7600 < l

          1. Initial program 85.9%

            \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
          2. Taylor expanded in K around 0

            \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
          3. Step-by-step derivation
            1. lower-+.f64N/A

              \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
            2. lower-*.f64N/A

              \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
            3. lower--.f64N/A

              \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
            4. lower-exp.f64N/A

              \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
            5. lower-exp.f64N/A

              \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
            6. lower-neg.f6473.0

              \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
          4. Applied rewrites73.0%

            \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
          5. Step-by-step derivation
            1. lift-*.f64N/A

              \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{-\ell}\right)} \]
            2. *-commutativeN/A

              \[\leadsto U + \left(e^{\ell} - e^{-\ell}\right) \cdot \color{blue}{J} \]
            3. lift--.f64N/A

              \[\leadsto U + \left(e^{\ell} - e^{-\ell}\right) \cdot J \]
            4. lift-exp.f64N/A

              \[\leadsto U + \left(e^{\ell} - e^{-\ell}\right) \cdot J \]
            5. lift-neg.f64N/A

              \[\leadsto U + \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \cdot J \]
            6. exp-negN/A

              \[\leadsto U + \left(e^{\ell} - \frac{1}{e^{\ell}}\right) \cdot J \]
            7. lift-exp.f64N/A

              \[\leadsto U + \left(e^{\ell} - \frac{1}{e^{\ell}}\right) \cdot J \]
            8. sub-to-fractionN/A

              \[\leadsto U + \frac{e^{\ell} \cdot e^{\ell} - 1}{e^{\ell}} \cdot J \]
            9. associate-*l/N/A

              \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{\color{blue}{e^{\ell}}} \]
            10. lower-/.f64N/A

              \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{\color{blue}{e^{\ell}}} \]
            11. lower-*.f64N/A

              \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{e^{\color{blue}{\ell}}} \]
            12. lift-exp.f64N/A

              \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{e^{\ell}} \]
            13. lift-exp.f64N/A

              \[\leadsto U + \frac{\left(e^{\ell} \cdot e^{\ell} - 1\right) \cdot J}{e^{\ell}} \]
            14. exp-lft-sqr-revN/A

              \[\leadsto U + \frac{\left(e^{\ell \cdot 2} - 1\right) \cdot J}{e^{\ell}} \]
            15. *-commutativeN/A

              \[\leadsto U + \frac{\left(e^{2 \cdot \ell} - 1\right) \cdot J}{e^{\ell}} \]
            16. lift-*.f64N/A

              \[\leadsto U + \frac{\left(e^{2 \cdot \ell} - 1\right) \cdot J}{e^{\ell}} \]
            17. lower-expm1.f6462.6

              \[\leadsto U + \frac{\mathsf{expm1}\left(2 \cdot \ell\right) \cdot J}{e^{\ell}} \]
            18. lift-*.f64N/A

              \[\leadsto U + \frac{\mathsf{expm1}\left(2 \cdot \ell\right) \cdot J}{e^{\ell}} \]
            19. count-2-revN/A

              \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{e^{\ell}} \]
            20. lower-+.f6462.6

              \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{e^{\ell}} \]
          6. Applied rewrites62.6%

            \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{\color{blue}{e^{\ell}}} \]
          7. Taylor expanded in l around 0

            \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{1} \]
          8. Step-by-step derivation
            1. Applied rewrites61.9%

              \[\leadsto U + \frac{\mathsf{expm1}\left(\ell + \ell\right) \cdot J}{1} \]
          9. Recombined 2 regimes into one program.
          10. Add Preprocessing

          Alternative 10: 54.5% accurate, 7.9× speedup?

          \[\begin{array}{l} \\ \mathsf{fma}\left(J + J, \ell, U\right) \end{array} \]
          (FPCore (J l K U) :precision binary64 (fma (+ J J) l U))
          double code(double J, double l, double K, double U) {
          	return fma((J + J), l, U);
          }
          
          function code(J, l, K, U)
          	return fma(Float64(J + J), l, U)
          end
          
          code[J_, l_, K_, U_] := N[(N[(J + J), $MachinePrecision] * l + U), $MachinePrecision]
          
          \begin{array}{l}
          
          \\
          \mathsf{fma}\left(J + J, \ell, U\right)
          \end{array}
          
          Derivation
          1. Initial program 85.9%

            \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
          2. Taylor expanded in K around 0

            \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
          3. Step-by-step derivation
            1. lower-+.f64N/A

              \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
            2. lower-*.f64N/A

              \[\leadsto U + J \cdot \color{blue}{\left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right)} \]
            3. lower--.f64N/A

              \[\leadsto U + J \cdot \left(e^{\ell} - \color{blue}{e^{\mathsf{neg}\left(\ell\right)}}\right) \]
            4. lower-exp.f64N/A

              \[\leadsto U + J \cdot \left(e^{\ell} - e^{\color{blue}{\mathsf{neg}\left(\ell\right)}}\right) \]
            5. lower-exp.f64N/A

              \[\leadsto U + J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) \]
            6. lower-neg.f6473.0

              \[\leadsto U + J \cdot \left(e^{\ell} - e^{-\ell}\right) \]
          4. Applied rewrites73.0%

            \[\leadsto \color{blue}{U + J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
          5. Step-by-step derivation
            1. lift-+.f64N/A

              \[\leadsto U + \color{blue}{J \cdot \left(e^{\ell} - e^{-\ell}\right)} \]
            2. +-commutativeN/A

              \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{U} \]
            3. add-flipN/A

              \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) - \color{blue}{\left(\mathsf{neg}\left(U\right)\right)} \]
            4. sub-flipN/A

              \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \color{blue}{\left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right)} \]
            5. lift-*.f64N/A

              \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
            6. lift--.f64N/A

              \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
            7. lift-exp.f64N/A

              \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
            8. lift-exp.f64N/A

              \[\leadsto J \cdot \left(e^{\ell} - e^{-\ell}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
            9. lift-neg.f64N/A

              \[\leadsto J \cdot \left(e^{\ell} - e^{\mathsf{neg}\left(\ell\right)}\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
            10. sinh-undefN/A

              \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
            11. lift-sinh.f64N/A

              \[\leadsto J \cdot \left(2 \cdot \sinh \ell\right) + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(U\right)\right)\right)\right) \]
            12. associate-*r*N/A

              \[\leadsto \left(J \cdot 2\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\color{blue}{\left(\mathsf{neg}\left(U\right)\right)}\right)\right) \]
            13. *-commutativeN/A

              \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + \left(\mathsf{neg}\left(\left(\mathsf{neg}\left(\color{blue}{U}\right)\right)\right)\right) \]
            14. remove-double-negN/A

              \[\leadsto \left(2 \cdot J\right) \cdot \sinh \ell + U \]
            15. lower-fma.f64N/A

              \[\leadsto \mathsf{fma}\left(2 \cdot J, \color{blue}{\sinh \ell}, U\right) \]
            16. count-2-revN/A

              \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
            17. lower-+.f6480.5

              \[\leadsto \mathsf{fma}\left(J + J, \sinh \color{blue}{\ell}, U\right) \]
          6. Applied rewrites80.5%

            \[\leadsto \color{blue}{\mathsf{fma}\left(J + J, \sinh \ell, U\right)} \]
          7. Taylor expanded in l around 0

            \[\leadsto \mathsf{fma}\left(J + J, \ell, U\right) \]
          8. Step-by-step derivation
            1. Applied rewrites54.5%

              \[\leadsto \mathsf{fma}\left(J + J, \ell, U\right) \]
            2. Add Preprocessing

            Alternative 11: 36.6% accurate, 68.7× speedup?

            \[\begin{array}{l} \\ U \end{array} \]
            (FPCore (J l K U) :precision binary64 U)
            double code(double J, double l, double K, double U) {
            	return U;
            }
            
            module fmin_fmax_functions
                implicit none
                private
                public fmax
                public fmin
            
                interface fmax
                    module procedure fmax88
                    module procedure fmax44
                    module procedure fmax84
                    module procedure fmax48
                end interface
                interface fmin
                    module procedure fmin88
                    module procedure fmin44
                    module procedure fmin84
                    module procedure fmin48
                end interface
            contains
                real(8) function fmax88(x, y) result (res)
                    real(8), intent (in) :: x
                    real(8), intent (in) :: y
                    res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                end function
                real(4) function fmax44(x, y) result (res)
                    real(4), intent (in) :: x
                    real(4), intent (in) :: y
                    res = merge(y, merge(x, max(x, y), y /= y), x /= x)
                end function
                real(8) function fmax84(x, y) result(res)
                    real(8), intent (in) :: x
                    real(4), intent (in) :: y
                    res = merge(dble(y), merge(x, max(x, dble(y)), y /= y), x /= x)
                end function
                real(8) function fmax48(x, y) result(res)
                    real(4), intent (in) :: x
                    real(8), intent (in) :: y
                    res = merge(y, merge(dble(x), max(dble(x), y), y /= y), x /= x)
                end function
                real(8) function fmin88(x, y) result (res)
                    real(8), intent (in) :: x
                    real(8), intent (in) :: y
                    res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                end function
                real(4) function fmin44(x, y) result (res)
                    real(4), intent (in) :: x
                    real(4), intent (in) :: y
                    res = merge(y, merge(x, min(x, y), y /= y), x /= x)
                end function
                real(8) function fmin84(x, y) result(res)
                    real(8), intent (in) :: x
                    real(4), intent (in) :: y
                    res = merge(dble(y), merge(x, min(x, dble(y)), y /= y), x /= x)
                end function
                real(8) function fmin48(x, y) result(res)
                    real(4), intent (in) :: x
                    real(8), intent (in) :: y
                    res = merge(y, merge(dble(x), min(dble(x), y), y /= y), x /= x)
                end function
            end module
            
            real(8) function code(j, l, k, u)
            use fmin_fmax_functions
                real(8), intent (in) :: j
                real(8), intent (in) :: l
                real(8), intent (in) :: k
                real(8), intent (in) :: u
                code = u
            end function
            
            public static double code(double J, double l, double K, double U) {
            	return U;
            }
            
            def code(J, l, K, U):
            	return U
            
            function code(J, l, K, U)
            	return U
            end
            
            function tmp = code(J, l, K, U)
            	tmp = U;
            end
            
            code[J_, l_, K_, U_] := U
            
            \begin{array}{l}
            
            \\
            U
            \end{array}
            
            Derivation
            1. Initial program 85.9%

              \[\left(J \cdot \left(e^{\ell} - e^{-\ell}\right)\right) \cdot \cos \left(\frac{K}{2}\right) + U \]
            2. Taylor expanded in J around 0

              \[\leadsto \color{blue}{U} \]
            3. Step-by-step derivation
              1. Applied rewrites36.6%

                \[\leadsto \color{blue}{U} \]
              2. Add Preprocessing

              Reproduce

              ?
              herbie shell --seed 2025156 
              (FPCore (J l K U)
                :name "Maksimov and Kolovsky, Equation (4)"
                :precision binary64
                (+ (* (* J (- (exp l) (exp (- l)))) (cos (/ K 2.0))) U))