cos2 (problem 3.4.1)

Percentage Accurate: 51.2% → 99.6%
Time: 3.8s
Alternatives: 7
Speedup: 120.0×

Specification

?
\[\begin{array}{l} \\ \frac{1 - \cos x}{x \cdot x} \end{array} \]
(FPCore (x) :precision binary64 (/ (- 1.0 (cos x)) (* x x)))
double code(double x) {
	return (1.0 - cos(x)) / (x * x);
}
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(x)
use fmin_fmax_functions
    real(8), intent (in) :: x
    code = (1.0d0 - cos(x)) / (x * x)
end function
public static double code(double x) {
	return (1.0 - Math.cos(x)) / (x * x);
}
def code(x):
	return (1.0 - math.cos(x)) / (x * x)
function code(x)
	return Float64(Float64(1.0 - cos(x)) / Float64(x * x))
end
function tmp = code(x)
	tmp = (1.0 - cos(x)) / (x * x);
end
code[x_] := N[(N[(1.0 - N[Cos[x], $MachinePrecision]), $MachinePrecision] / N[(x * x), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{1 - \cos x}{x \cdot x}
\end{array}

Sampling outcomes in binary64 precision:

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 7 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: 51.2% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \frac{1 - \cos x}{x \cdot x} \end{array} \]
(FPCore (x) :precision binary64 (/ (- 1.0 (cos x)) (* x x)))
double code(double x) {
	return (1.0 - cos(x)) / (x * x);
}
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(x)
use fmin_fmax_functions
    real(8), intent (in) :: x
    code = (1.0d0 - cos(x)) / (x * x)
end function
public static double code(double x) {
	return (1.0 - Math.cos(x)) / (x * x);
}
def code(x):
	return (1.0 - math.cos(x)) / (x * x)
function code(x)
	return Float64(Float64(1.0 - cos(x)) / Float64(x * x))
end
function tmp = code(x)
	tmp = (1.0 - cos(x)) / (x * x);
end
code[x_] := N[(N[(1.0 - N[Cos[x], $MachinePrecision]), $MachinePrecision] / N[(x * x), $MachinePrecision]), $MachinePrecision]
\begin{array}{l}

\\
\frac{1 - \cos x}{x \cdot x}
\end{array}

Alternative 1: 99.6% accurate, 0.9× speedup?

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;x\_m \leq 0.1:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-2.48015873015873 \cdot 10^{-5}, x\_m \cdot x\_m, 0.001388888888888889\right), x\_m \cdot x\_m, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1 - \cos x\_m}{x\_m}}{x\_m}\\ \end{array} \end{array} \]
x_m = (fabs.f64 x)
(FPCore (x_m)
 :precision binary64
 (if (<= x_m 0.1)
   (fma
    (fma
     (fma -2.48015873015873e-5 (* x_m x_m) 0.001388888888888889)
     (* x_m x_m)
     -0.041666666666666664)
    (* x_m x_m)
    0.5)
   (/ (/ (- 1.0 (cos x_m)) x_m) x_m)))
x_m = fabs(x);
double code(double x_m) {
	double tmp;
	if (x_m <= 0.1) {
		tmp = fma(fma(fma(-2.48015873015873e-5, (x_m * x_m), 0.001388888888888889), (x_m * x_m), -0.041666666666666664), (x_m * x_m), 0.5);
	} else {
		tmp = ((1.0 - cos(x_m)) / x_m) / x_m;
	}
	return tmp;
}
x_m = abs(x)
function code(x_m)
	tmp = 0.0
	if (x_m <= 0.1)
		tmp = fma(fma(fma(-2.48015873015873e-5, Float64(x_m * x_m), 0.001388888888888889), Float64(x_m * x_m), -0.041666666666666664), Float64(x_m * x_m), 0.5);
	else
		tmp = Float64(Float64(Float64(1.0 - cos(x_m)) / x_m) / x_m);
	end
	return tmp
end
x_m = N[Abs[x], $MachinePrecision]
code[x$95$m_] := If[LessEqual[x$95$m, 0.1], N[(N[(N[(-2.48015873015873e-5 * N[(x$95$m * x$95$m), $MachinePrecision] + 0.001388888888888889), $MachinePrecision] * N[(x$95$m * x$95$m), $MachinePrecision] + -0.041666666666666664), $MachinePrecision] * N[(x$95$m * x$95$m), $MachinePrecision] + 0.5), $MachinePrecision], N[(N[(N[(1.0 - N[Cos[x$95$m], $MachinePrecision]), $MachinePrecision] / x$95$m), $MachinePrecision] / x$95$m), $MachinePrecision]]
\begin{array}{l}
x_m = \left|x\right|

\\
\begin{array}{l}
\mathbf{if}\;x\_m \leq 0.1:\\
\;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-2.48015873015873 \cdot 10^{-5}, x\_m \cdot x\_m, 0.001388888888888889\right), x\_m \cdot x\_m, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{1 - \cos x\_m}{x\_m}}{x\_m}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if x < 0.10000000000000001

    1. Initial program 36.1%

      \[\frac{1 - \cos x}{x \cdot x} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \frac{1 - \cos x}{\color{blue}{x \cdot x}} \]
      2. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{1 - \cos x}{x \cdot x}} \]
      3. lift--.f64N/A

        \[\leadsto \frac{\color{blue}{1 - \cos x}}{x \cdot x} \]
      4. lift-cos.f64N/A

        \[\leadsto \frac{1 - \color{blue}{\cos x}}{x \cdot x} \]
      5. flip--N/A

        \[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}}{x \cdot x} \]
      6. pow2N/A

        \[\leadsto \frac{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}{\color{blue}{{x}^{2}}} \]
      7. associate-/l/N/A

        \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
      8. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
      9. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{1} - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      10. 1-sub-cosN/A

        \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      11. lower-*.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      12. lower-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      13. lower-sin.f64N/A

        \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      14. lower-*.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
      15. +-commutativeN/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
      16. lower-+.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
      17. lift-cos.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot {x}^{2}} \]
      18. pow2N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
      19. lift-*.f6470.1

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
    4. Applied rewrites70.1%

      \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
    5. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
      3. lift-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
      4. lift-sin.f64N/A

        \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
      5. lift-*.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
      6. lift-+.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot \left(x \cdot x\right)} \]
      7. lift-cos.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot \left(x \cdot x\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
      9. pow2N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{{x}^{2}}} \]
      10. *-commutativeN/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{{x}^{2} \cdot \left(\cos x + 1\right)}} \]
      11. times-fracN/A

        \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
      12. lower-*.f64N/A

        \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
      13. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}}} \cdot \frac{\sin x}{\cos x + 1} \]
      14. lift-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x}}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1} \]
      15. pow2N/A

        \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
      16. lift-*.f64N/A

        \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
      17. +-commutativeN/A

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \frac{\sin x}{\color{blue}{1 + \cos x}} \]
      18. hang-0p-tanN/A

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
      19. lower-tan.f64N/A

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
      20. lower-/.f6470.4

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \tan \color{blue}{\left(\frac{x}{2}\right)} \]
    6. Applied rewrites70.4%

      \[\leadsto \color{blue}{\frac{\sin x}{x \cdot x} \cdot \tan \left(\frac{x}{2}\right)} \]
    7. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right)} \]
    8. Step-by-step derivation
      1. lift-sin.f64N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      2. lift-sin.f64N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      3. pow2N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      4. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      5. pow2N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      6. hang-0p-tan-revN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      7. associate-*r/N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      8. 1-sub-cosN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      9. metadata-evalN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      10. flip--N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      11. associate-/l/N/A

        \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      12. +-commutativeN/A

        \[\leadsto {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) + \color{blue}{\frac{1}{2}} \]
      13. *-commutativeN/A

        \[\leadsto \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \cdot {x}^{2} + \frac{1}{2} \]
      14. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}, \color{blue}{{x}^{2}}, \frac{1}{2}\right) \]
    9. Applied rewrites66.1%

      \[\leadsto \color{blue}{\mathsf{fma}\left(0.001388888888888889 \cdot \left(x \cdot x\right) - 0.041666666666666664, x \cdot x, 0.5\right)} \]
    10. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{1}{2} + {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right)} \]
    11. Step-by-step derivation
      1. div-subN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) \]
      2. sub-divN/A

        \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) \]
      3. associate-/r*N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) \]
      4. +-commutativeN/A

        \[\leadsto {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) + \color{blue}{\frac{1}{2}} \]
      5. *-commutativeN/A

        \[\leadsto \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) \cdot {x}^{2} + \frac{1}{2} \]
      6. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}, \color{blue}{{x}^{2}}, \frac{1}{2}\right) \]
    12. Applied rewrites66.0%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-2.48015873015873 \cdot 10^{-5}, x \cdot x, 0.001388888888888889\right), x \cdot x, -0.041666666666666664\right), x \cdot x, 0.5\right)} \]

    if 0.10000000000000001 < x

    1. Initial program 99.5%

      \[\frac{1 - \cos x}{x \cdot x} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \frac{1 - \cos x}{\color{blue}{x \cdot x}} \]
      2. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{1 - \cos x}{x \cdot x}} \]
      3. lift--.f64N/A

        \[\leadsto \frac{\color{blue}{1 - \cos x}}{x \cdot x} \]
      4. lift-cos.f64N/A

        \[\leadsto \frac{1 - \color{blue}{\cos x}}{x \cdot x} \]
      5. associate-/r*N/A

        \[\leadsto \color{blue}{\frac{\frac{1 - \cos x}{x}}{x}} \]
      6. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\frac{1 - \cos x}{x}}{x}} \]
      7. lower-/.f64N/A

        \[\leadsto \frac{\color{blue}{\frac{1 - \cos x}{x}}}{x} \]
      8. lift-cos.f64N/A

        \[\leadsto \frac{\frac{1 - \color{blue}{\cos x}}{x}}{x} \]
      9. lift--.f6499.5

        \[\leadsto \frac{\frac{\color{blue}{1 - \cos x}}{x}}{x} \]
    4. Applied rewrites99.5%

      \[\leadsto \color{blue}{\frac{\frac{1 - \cos x}{x}}{x}} \]
  3. Recombined 2 regimes into one program.
  4. Final simplification73.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 0.1:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-2.48015873015873 \cdot 10^{-5}, x \cdot x, 0.001388888888888889\right), x \cdot x, -0.041666666666666664\right), x \cdot x, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{1 - \cos x}{x}}{x}\\ \end{array} \]
  5. Add Preprocessing

Alternative 2: 99.1% accurate, 1.0× speedup?

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;x\_m \leq 0.1:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-2.48015873015873 \cdot 10^{-5}, x\_m \cdot x\_m, 0.001388888888888889\right), x\_m \cdot x\_m, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - \cos x\_m}{x\_m \cdot x\_m}\\ \end{array} \end{array} \]
x_m = (fabs.f64 x)
(FPCore (x_m)
 :precision binary64
 (if (<= x_m 0.1)
   (fma
    (fma
     (fma -2.48015873015873e-5 (* x_m x_m) 0.001388888888888889)
     (* x_m x_m)
     -0.041666666666666664)
    (* x_m x_m)
    0.5)
   (/ (- 1.0 (cos x_m)) (* x_m x_m))))
x_m = fabs(x);
double code(double x_m) {
	double tmp;
	if (x_m <= 0.1) {
		tmp = fma(fma(fma(-2.48015873015873e-5, (x_m * x_m), 0.001388888888888889), (x_m * x_m), -0.041666666666666664), (x_m * x_m), 0.5);
	} else {
		tmp = (1.0 - cos(x_m)) / (x_m * x_m);
	}
	return tmp;
}
x_m = abs(x)
function code(x_m)
	tmp = 0.0
	if (x_m <= 0.1)
		tmp = fma(fma(fma(-2.48015873015873e-5, Float64(x_m * x_m), 0.001388888888888889), Float64(x_m * x_m), -0.041666666666666664), Float64(x_m * x_m), 0.5);
	else
		tmp = Float64(Float64(1.0 - cos(x_m)) / Float64(x_m * x_m));
	end
	return tmp
end
x_m = N[Abs[x], $MachinePrecision]
code[x$95$m_] := If[LessEqual[x$95$m, 0.1], N[(N[(N[(-2.48015873015873e-5 * N[(x$95$m * x$95$m), $MachinePrecision] + 0.001388888888888889), $MachinePrecision] * N[(x$95$m * x$95$m), $MachinePrecision] + -0.041666666666666664), $MachinePrecision] * N[(x$95$m * x$95$m), $MachinePrecision] + 0.5), $MachinePrecision], N[(N[(1.0 - N[Cos[x$95$m], $MachinePrecision]), $MachinePrecision] / N[(x$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
x_m = \left|x\right|

\\
\begin{array}{l}
\mathbf{if}\;x\_m \leq 0.1:\\
\;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-2.48015873015873 \cdot 10^{-5}, x\_m \cdot x\_m, 0.001388888888888889\right), x\_m \cdot x\_m, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{1 - \cos x\_m}{x\_m \cdot x\_m}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if x < 0.10000000000000001

    1. Initial program 36.1%

      \[\frac{1 - \cos x}{x \cdot x} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \frac{1 - \cos x}{\color{blue}{x \cdot x}} \]
      2. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{1 - \cos x}{x \cdot x}} \]
      3. lift--.f64N/A

        \[\leadsto \frac{\color{blue}{1 - \cos x}}{x \cdot x} \]
      4. lift-cos.f64N/A

        \[\leadsto \frac{1 - \color{blue}{\cos x}}{x \cdot x} \]
      5. flip--N/A

        \[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}}{x \cdot x} \]
      6. pow2N/A

        \[\leadsto \frac{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}{\color{blue}{{x}^{2}}} \]
      7. associate-/l/N/A

        \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
      8. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
      9. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{1} - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      10. 1-sub-cosN/A

        \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      11. lower-*.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      12. lower-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      13. lower-sin.f64N/A

        \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      14. lower-*.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
      15. +-commutativeN/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
      16. lower-+.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
      17. lift-cos.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot {x}^{2}} \]
      18. pow2N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
      19. lift-*.f6470.1

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
    4. Applied rewrites70.1%

      \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
    5. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
      3. lift-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
      4. lift-sin.f64N/A

        \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
      5. lift-*.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
      6. lift-+.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot \left(x \cdot x\right)} \]
      7. lift-cos.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot \left(x \cdot x\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
      9. pow2N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{{x}^{2}}} \]
      10. *-commutativeN/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{{x}^{2} \cdot \left(\cos x + 1\right)}} \]
      11. times-fracN/A

        \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
      12. lower-*.f64N/A

        \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
      13. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}}} \cdot \frac{\sin x}{\cos x + 1} \]
      14. lift-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x}}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1} \]
      15. pow2N/A

        \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
      16. lift-*.f64N/A

        \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
      17. +-commutativeN/A

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \frac{\sin x}{\color{blue}{1 + \cos x}} \]
      18. hang-0p-tanN/A

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
      19. lower-tan.f64N/A

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
      20. lower-/.f6470.4

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \tan \color{blue}{\left(\frac{x}{2}\right)} \]
    6. Applied rewrites70.4%

      \[\leadsto \color{blue}{\frac{\sin x}{x \cdot x} \cdot \tan \left(\frac{x}{2}\right)} \]
    7. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right)} \]
    8. Step-by-step derivation
      1. lift-sin.f64N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      2. lift-sin.f64N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      3. pow2N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      4. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      5. pow2N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      6. hang-0p-tan-revN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      7. associate-*r/N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      8. 1-sub-cosN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      9. metadata-evalN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      10. flip--N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      11. associate-/l/N/A

        \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      12. +-commutativeN/A

        \[\leadsto {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) + \color{blue}{\frac{1}{2}} \]
      13. *-commutativeN/A

        \[\leadsto \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \cdot {x}^{2} + \frac{1}{2} \]
      14. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}, \color{blue}{{x}^{2}}, \frac{1}{2}\right) \]
    9. Applied rewrites66.1%

      \[\leadsto \color{blue}{\mathsf{fma}\left(0.001388888888888889 \cdot \left(x \cdot x\right) - 0.041666666666666664, x \cdot x, 0.5\right)} \]
    10. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{1}{2} + {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right)} \]
    11. Step-by-step derivation
      1. div-subN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) \]
      2. sub-divN/A

        \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) \]
      3. associate-/r*N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) \]
      4. +-commutativeN/A

        \[\leadsto {x}^{2} \cdot \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) + \color{blue}{\frac{1}{2}} \]
      5. *-commutativeN/A

        \[\leadsto \left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}\right) \cdot {x}^{2} + \frac{1}{2} \]
      6. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \left(\frac{1}{720} + \frac{-1}{40320} \cdot {x}^{2}\right) - \frac{1}{24}, \color{blue}{{x}^{2}}, \frac{1}{2}\right) \]
    12. Applied rewrites66.0%

      \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-2.48015873015873 \cdot 10^{-5}, x \cdot x, 0.001388888888888889\right), x \cdot x, -0.041666666666666664\right), x \cdot x, 0.5\right)} \]

    if 0.10000000000000001 < x

    1. Initial program 99.5%

      \[\frac{1 - \cos x}{x \cdot x} \]
    2. Add Preprocessing
  3. Recombined 2 regimes into one program.
  4. Final simplification73.7%

    \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 0.1:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(\mathsf{fma}\left(-2.48015873015873 \cdot 10^{-5}, x \cdot x, 0.001388888888888889\right), x \cdot x, -0.041666666666666664\right), x \cdot x, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - \cos x}{x \cdot x}\\ \end{array} \]
  5. Add Preprocessing

Alternative 3: 76.4% accurate, 2.3× speedup?

\[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;x\_m \leq 2.45 \cdot 10^{+33}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(x\_m \cdot x\_m, 0.001388888888888889, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{-1}{x\_m} \cdot \frac{-1}{x\_m} - \frac{1}{x\_m \cdot x\_m}\\ \end{array} \end{array} \]
x_m = (fabs.f64 x)
(FPCore (x_m)
 :precision binary64
 (if (<= x_m 2.45e+33)
   (fma
    (fma (* x_m x_m) 0.001388888888888889 -0.041666666666666664)
    (* x_m x_m)
    0.5)
   (- (* (/ -1.0 x_m) (/ -1.0 x_m)) (/ 1.0 (* x_m x_m)))))
x_m = fabs(x);
double code(double x_m) {
	double tmp;
	if (x_m <= 2.45e+33) {
		tmp = fma(fma((x_m * x_m), 0.001388888888888889, -0.041666666666666664), (x_m * x_m), 0.5);
	} else {
		tmp = ((-1.0 / x_m) * (-1.0 / x_m)) - (1.0 / (x_m * x_m));
	}
	return tmp;
}
x_m = abs(x)
function code(x_m)
	tmp = 0.0
	if (x_m <= 2.45e+33)
		tmp = fma(fma(Float64(x_m * x_m), 0.001388888888888889, -0.041666666666666664), Float64(x_m * x_m), 0.5);
	else
		tmp = Float64(Float64(Float64(-1.0 / x_m) * Float64(-1.0 / x_m)) - Float64(1.0 / Float64(x_m * x_m)));
	end
	return tmp
end
x_m = N[Abs[x], $MachinePrecision]
code[x$95$m_] := If[LessEqual[x$95$m, 2.45e+33], N[(N[(N[(x$95$m * x$95$m), $MachinePrecision] * 0.001388888888888889 + -0.041666666666666664), $MachinePrecision] * N[(x$95$m * x$95$m), $MachinePrecision] + 0.5), $MachinePrecision], N[(N[(N[(-1.0 / x$95$m), $MachinePrecision] * N[(-1.0 / x$95$m), $MachinePrecision]), $MachinePrecision] - N[(1.0 / N[(x$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]
\begin{array}{l}
x_m = \left|x\right|

\\
\begin{array}{l}
\mathbf{if}\;x\_m \leq 2.45 \cdot 10^{+33}:\\
\;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(x\_m \cdot x\_m, 0.001388888888888889, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\

\mathbf{else}:\\
\;\;\;\;\frac{-1}{x\_m} \cdot \frac{-1}{x\_m} - \frac{1}{x\_m \cdot x\_m}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes
  2. if x < 2.45000000000000007e33

    1. Initial program 37.3%

      \[\frac{1 - \cos x}{x \cdot x} \]
    2. Add Preprocessing
    3. Step-by-step derivation
      1. lift-*.f64N/A

        \[\leadsto \frac{1 - \cos x}{\color{blue}{x \cdot x}} \]
      2. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{1 - \cos x}{x \cdot x}} \]
      3. lift--.f64N/A

        \[\leadsto \frac{\color{blue}{1 - \cos x}}{x \cdot x} \]
      4. lift-cos.f64N/A

        \[\leadsto \frac{1 - \color{blue}{\cos x}}{x \cdot x} \]
      5. flip--N/A

        \[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}}{x \cdot x} \]
      6. pow2N/A

        \[\leadsto \frac{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}{\color{blue}{{x}^{2}}} \]
      7. associate-/l/N/A

        \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
      8. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
      9. metadata-evalN/A

        \[\leadsto \frac{\color{blue}{1} - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      10. 1-sub-cosN/A

        \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      11. lower-*.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      12. lower-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      13. lower-sin.f64N/A

        \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
      14. lower-*.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
      15. +-commutativeN/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
      16. lower-+.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
      17. lift-cos.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot {x}^{2}} \]
      18. pow2N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
      19. lift-*.f6470.7

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
    4. Applied rewrites70.7%

      \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
    5. Step-by-step derivation
      1. lift-/.f64N/A

        \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
      2. lift-*.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
      3. lift-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
      4. lift-sin.f64N/A

        \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
      5. lift-*.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
      6. lift-+.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot \left(x \cdot x\right)} \]
      7. lift-cos.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot \left(x \cdot x\right)} \]
      8. lift-*.f64N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
      9. pow2N/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{{x}^{2}}} \]
      10. *-commutativeN/A

        \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{{x}^{2} \cdot \left(\cos x + 1\right)}} \]
      11. times-fracN/A

        \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
      12. lower-*.f64N/A

        \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
      13. lower-/.f64N/A

        \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}}} \cdot \frac{\sin x}{\cos x + 1} \]
      14. lift-sin.f64N/A

        \[\leadsto \frac{\color{blue}{\sin x}}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1} \]
      15. pow2N/A

        \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
      16. lift-*.f64N/A

        \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
      17. +-commutativeN/A

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \frac{\sin x}{\color{blue}{1 + \cos x}} \]
      18. hang-0p-tanN/A

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
      19. lower-tan.f64N/A

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
      20. lower-/.f6471.0

        \[\leadsto \frac{\sin x}{x \cdot x} \cdot \tan \color{blue}{\left(\frac{x}{2}\right)} \]
    6. Applied rewrites71.0%

      \[\leadsto \color{blue}{\frac{\sin x}{x \cdot x} \cdot \tan \left(\frac{x}{2}\right)} \]
    7. Taylor expanded in x around 0

      \[\leadsto \color{blue}{\frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right)} \]
    8. Step-by-step derivation
      1. lift-sin.f64N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      2. lift-sin.f64N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      3. pow2N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      4. associate-*l/N/A

        \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      5. pow2N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      6. hang-0p-tan-revN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      7. associate-*r/N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      8. 1-sub-cosN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      9. metadata-evalN/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      10. flip--N/A

        \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      11. associate-/l/N/A

        \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
      12. +-commutativeN/A

        \[\leadsto {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) + \color{blue}{\frac{1}{2}} \]
      13. *-commutativeN/A

        \[\leadsto \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \cdot {x}^{2} + \frac{1}{2} \]
      14. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}, \color{blue}{{x}^{2}}, \frac{1}{2}\right) \]
    9. Applied rewrites64.9%

      \[\leadsto \color{blue}{\mathsf{fma}\left(0.001388888888888889 \cdot \left(x \cdot x\right) - 0.041666666666666664, x \cdot x, 0.5\right)} \]
    10. Step-by-step derivation
      1. lift--.f64N/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot \left(x \cdot x\right) - \frac{1}{24}, \color{blue}{x} \cdot x, \frac{1}{2}\right) \]
      2. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot \left(x \cdot x\right) - \frac{1}{24}, x \cdot x, \frac{1}{2}\right) \]
      3. lift-*.f64N/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot \left(x \cdot x\right) - \frac{1}{24}, x \cdot x, \frac{1}{2}\right) \]
      4. pow2N/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}, x \cdot x, \frac{1}{2}\right) \]
      5. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24} \cdot 1, x \cdot x, \frac{1}{2}\right) \]
      6. fp-cancel-sub-sign-invN/A

        \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} + \left(\mathsf{neg}\left(\frac{1}{24}\right)\right) \cdot 1, \color{blue}{x} \cdot x, \frac{1}{2}\right) \]
      7. *-commutativeN/A

        \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \frac{1}{720} + \left(\mathsf{neg}\left(\frac{1}{24}\right)\right) \cdot 1, x \cdot x, \frac{1}{2}\right) \]
      8. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \frac{1}{720} + \frac{-1}{24} \cdot 1, x \cdot x, \frac{1}{2}\right) \]
      9. metadata-evalN/A

        \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \frac{1}{720} + \frac{-1}{24}, x \cdot x, \frac{1}{2}\right) \]
      10. lower-fma.f64N/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left({x}^{2}, \frac{1}{720}, \frac{-1}{24}\right), \color{blue}{x} \cdot x, \frac{1}{2}\right) \]
      11. pow2N/A

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, \frac{1}{720}, \frac{-1}{24}\right), x \cdot x, \frac{1}{2}\right) \]
      12. lift-*.f6464.9

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, 0.001388888888888889, -0.041666666666666664\right), x \cdot x, 0.5\right) \]
    11. Applied rewrites64.9%

      \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, 0.001388888888888889, -0.041666666666666664\right), \color{blue}{x \cdot x}, 0.5\right) \]

    if 2.45000000000000007e33 < x

    1. Initial program 99.5%

      \[\frac{1 - \cos x}{x \cdot x} \]
    2. Add Preprocessing
    3. Taylor expanded in x around 0

      \[\leadsto \frac{1 - \color{blue}{1}}{x \cdot x} \]
    4. Step-by-step derivation
      1. Applied rewrites55.5%

        \[\leadsto \frac{1 - \color{blue}{1}}{x \cdot x} \]
      2. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{1 - 1}{x \cdot x}} \]
        2. lift-*.f64N/A

          \[\leadsto \frac{1 - 1}{\color{blue}{x \cdot x}} \]
        3. pow2N/A

          \[\leadsto \frac{1 - 1}{\color{blue}{{x}^{2}}} \]
        4. lift--.f64N/A

          \[\leadsto \frac{\color{blue}{1 - 1}}{{x}^{2}} \]
        5. div-subN/A

          \[\leadsto \color{blue}{\frac{1}{{x}^{2}} - \frac{1}{{x}^{2}}} \]
        6. lower--.f64N/A

          \[\leadsto \color{blue}{\frac{1}{{x}^{2}} - \frac{1}{{x}^{2}}} \]
        7. pow-flipN/A

          \[\leadsto \color{blue}{{x}^{\left(\mathsf{neg}\left(2\right)\right)}} - \frac{1}{{x}^{2}} \]
        8. lower-pow.f64N/A

          \[\leadsto \color{blue}{{x}^{\left(\mathsf{neg}\left(2\right)\right)}} - \frac{1}{{x}^{2}} \]
        9. metadata-evalN/A

          \[\leadsto {x}^{\color{blue}{-2}} - \frac{1}{{x}^{2}} \]
        10. lower-/.f64N/A

          \[\leadsto {x}^{-2} - \color{blue}{\frac{1}{{x}^{2}}} \]
        11. pow2N/A

          \[\leadsto {x}^{-2} - \frac{1}{\color{blue}{x \cdot x}} \]
        12. lift-*.f6455.8

          \[\leadsto {x}^{-2} - \frac{1}{\color{blue}{x \cdot x}} \]
      3. Applied rewrites55.8%

        \[\leadsto \color{blue}{{x}^{-2} - \frac{1}{x \cdot x}} \]
      4. Step-by-step derivation
        1. lift-pow.f64N/A

          \[\leadsto \color{blue}{{x}^{-2}} - \frac{1}{x \cdot x} \]
        2. metadata-evalN/A

          \[\leadsto {x}^{\color{blue}{\left(\mathsf{neg}\left(2\right)\right)}} - \frac{1}{x \cdot x} \]
        3. pow-flipN/A

          \[\leadsto \color{blue}{\frac{1}{{x}^{2}}} - \frac{1}{x \cdot x} \]
        4. metadata-evalN/A

          \[\leadsto \frac{\color{blue}{1 \cdot 1}}{{x}^{2}} - \frac{1}{x \cdot x} \]
        5. pow2N/A

          \[\leadsto \frac{1 \cdot 1}{\color{blue}{x \cdot x}} - \frac{1}{x \cdot x} \]
        6. sqr-neg-revN/A

          \[\leadsto \frac{1 \cdot 1}{\color{blue}{\left(\mathsf{neg}\left(x\right)\right) \cdot \left(\mathsf{neg}\left(x\right)\right)}} - \frac{1}{x \cdot x} \]
        7. times-fracN/A

          \[\leadsto \color{blue}{\frac{1}{\mathsf{neg}\left(x\right)} \cdot \frac{1}{\mathsf{neg}\left(x\right)}} - \frac{1}{x \cdot x} \]
        8. lower-*.f64N/A

          \[\leadsto \color{blue}{\frac{1}{\mathsf{neg}\left(x\right)} \cdot \frac{1}{\mathsf{neg}\left(x\right)}} - \frac{1}{x \cdot x} \]
        9. metadata-evalN/A

          \[\leadsto \frac{\color{blue}{\mathsf{neg}\left(-1\right)}}{\mathsf{neg}\left(x\right)} \cdot \frac{1}{\mathsf{neg}\left(x\right)} - \frac{1}{x \cdot x} \]
        10. frac-2neg-revN/A

          \[\leadsto \color{blue}{\frac{-1}{x}} \cdot \frac{1}{\mathsf{neg}\left(x\right)} - \frac{1}{x \cdot x} \]
        11. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{-1}{x}} \cdot \frac{1}{\mathsf{neg}\left(x\right)} - \frac{1}{x \cdot x} \]
        12. metadata-evalN/A

          \[\leadsto \frac{-1}{x} \cdot \frac{\color{blue}{\mathsf{neg}\left(-1\right)}}{\mathsf{neg}\left(x\right)} - \frac{1}{x \cdot x} \]
        13. frac-2neg-revN/A

          \[\leadsto \frac{-1}{x} \cdot \color{blue}{\frac{-1}{x}} - \frac{1}{x \cdot x} \]
        14. lower-/.f6455.7

          \[\leadsto \frac{-1}{x} \cdot \color{blue}{\frac{-1}{x}} - \frac{1}{x \cdot x} \]
      5. Applied rewrites55.7%

        \[\leadsto \color{blue}{\frac{-1}{x} \cdot \frac{-1}{x}} - \frac{1}{x \cdot x} \]
    5. Recombined 2 regimes into one program.
    6. Add Preprocessing

    Alternative 4: 76.4% accurate, 2.4× speedup?

    \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;x\_m \leq 2.45 \cdot 10^{+33}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(x\_m \cdot x\_m, 0.001388888888888889, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;-\left(\frac{\frac{-1}{x\_m}}{x\_m} + \frac{1}{x\_m \cdot x\_m}\right)\\ \end{array} \end{array} \]
    x_m = (fabs.f64 x)
    (FPCore (x_m)
     :precision binary64
     (if (<= x_m 2.45e+33)
       (fma
        (fma (* x_m x_m) 0.001388888888888889 -0.041666666666666664)
        (* x_m x_m)
        0.5)
       (- (+ (/ (/ -1.0 x_m) x_m) (/ 1.0 (* x_m x_m))))))
    x_m = fabs(x);
    double code(double x_m) {
    	double tmp;
    	if (x_m <= 2.45e+33) {
    		tmp = fma(fma((x_m * x_m), 0.001388888888888889, -0.041666666666666664), (x_m * x_m), 0.5);
    	} else {
    		tmp = -(((-1.0 / x_m) / x_m) + (1.0 / (x_m * x_m)));
    	}
    	return tmp;
    }
    
    x_m = abs(x)
    function code(x_m)
    	tmp = 0.0
    	if (x_m <= 2.45e+33)
    		tmp = fma(fma(Float64(x_m * x_m), 0.001388888888888889, -0.041666666666666664), Float64(x_m * x_m), 0.5);
    	else
    		tmp = Float64(-Float64(Float64(Float64(-1.0 / x_m) / x_m) + Float64(1.0 / Float64(x_m * x_m))));
    	end
    	return tmp
    end
    
    x_m = N[Abs[x], $MachinePrecision]
    code[x$95$m_] := If[LessEqual[x$95$m, 2.45e+33], N[(N[(N[(x$95$m * x$95$m), $MachinePrecision] * 0.001388888888888889 + -0.041666666666666664), $MachinePrecision] * N[(x$95$m * x$95$m), $MachinePrecision] + 0.5), $MachinePrecision], (-N[(N[(N[(-1.0 / x$95$m), $MachinePrecision] / x$95$m), $MachinePrecision] + N[(1.0 / N[(x$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]), $MachinePrecision])]
    
    \begin{array}{l}
    x_m = \left|x\right|
    
    \\
    \begin{array}{l}
    \mathbf{if}\;x\_m \leq 2.45 \cdot 10^{+33}:\\
    \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(x\_m \cdot x\_m, 0.001388888888888889, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;-\left(\frac{\frac{-1}{x\_m}}{x\_m} + \frac{1}{x\_m \cdot x\_m}\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if x < 2.45000000000000007e33

      1. Initial program 37.3%

        \[\frac{1 - \cos x}{x \cdot x} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-*.f64N/A

          \[\leadsto \frac{1 - \cos x}{\color{blue}{x \cdot x}} \]
        2. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{1 - \cos x}{x \cdot x}} \]
        3. lift--.f64N/A

          \[\leadsto \frac{\color{blue}{1 - \cos x}}{x \cdot x} \]
        4. lift-cos.f64N/A

          \[\leadsto \frac{1 - \color{blue}{\cos x}}{x \cdot x} \]
        5. flip--N/A

          \[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}}{x \cdot x} \]
        6. pow2N/A

          \[\leadsto \frac{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}{\color{blue}{{x}^{2}}} \]
        7. associate-/l/N/A

          \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
        8. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
        9. metadata-evalN/A

          \[\leadsto \frac{\color{blue}{1} - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
        10. 1-sub-cosN/A

          \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
        11. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
        12. lower-sin.f64N/A

          \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
        13. lower-sin.f64N/A

          \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
        14. lower-*.f64N/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
        15. +-commutativeN/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
        16. lower-+.f64N/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
        17. lift-cos.f64N/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot {x}^{2}} \]
        18. pow2N/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
        19. lift-*.f6470.7

          \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
      4. Applied rewrites70.7%

        \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
      5. Step-by-step derivation
        1. lift-/.f64N/A

          \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
        2. lift-*.f64N/A

          \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
        3. lift-sin.f64N/A

          \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
        4. lift-sin.f64N/A

          \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
        5. lift-*.f64N/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
        6. lift-+.f64N/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot \left(x \cdot x\right)} \]
        7. lift-cos.f64N/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot \left(x \cdot x\right)} \]
        8. lift-*.f64N/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
        9. pow2N/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{{x}^{2}}} \]
        10. *-commutativeN/A

          \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{{x}^{2} \cdot \left(\cos x + 1\right)}} \]
        11. times-fracN/A

          \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
        12. lower-*.f64N/A

          \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
        13. lower-/.f64N/A

          \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}}} \cdot \frac{\sin x}{\cos x + 1} \]
        14. lift-sin.f64N/A

          \[\leadsto \frac{\color{blue}{\sin x}}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1} \]
        15. pow2N/A

          \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
        16. lift-*.f64N/A

          \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
        17. +-commutativeN/A

          \[\leadsto \frac{\sin x}{x \cdot x} \cdot \frac{\sin x}{\color{blue}{1 + \cos x}} \]
        18. hang-0p-tanN/A

          \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
        19. lower-tan.f64N/A

          \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
        20. lower-/.f6471.0

          \[\leadsto \frac{\sin x}{x \cdot x} \cdot \tan \color{blue}{\left(\frac{x}{2}\right)} \]
      6. Applied rewrites71.0%

        \[\leadsto \color{blue}{\frac{\sin x}{x \cdot x} \cdot \tan \left(\frac{x}{2}\right)} \]
      7. Taylor expanded in x around 0

        \[\leadsto \color{blue}{\frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right)} \]
      8. Step-by-step derivation
        1. lift-sin.f64N/A

          \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        2. lift-sin.f64N/A

          \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        3. pow2N/A

          \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        4. associate-*l/N/A

          \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        5. pow2N/A

          \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        6. hang-0p-tan-revN/A

          \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        7. associate-*r/N/A

          \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        8. 1-sub-cosN/A

          \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        9. metadata-evalN/A

          \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        10. flip--N/A

          \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        11. associate-/l/N/A

          \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
        12. +-commutativeN/A

          \[\leadsto {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) + \color{blue}{\frac{1}{2}} \]
        13. *-commutativeN/A

          \[\leadsto \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \cdot {x}^{2} + \frac{1}{2} \]
        14. lower-fma.f64N/A

          \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}, \color{blue}{{x}^{2}}, \frac{1}{2}\right) \]
      9. Applied rewrites64.9%

        \[\leadsto \color{blue}{\mathsf{fma}\left(0.001388888888888889 \cdot \left(x \cdot x\right) - 0.041666666666666664, x \cdot x, 0.5\right)} \]
      10. Step-by-step derivation
        1. lift--.f64N/A

          \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot \left(x \cdot x\right) - \frac{1}{24}, \color{blue}{x} \cdot x, \frac{1}{2}\right) \]
        2. lift-*.f64N/A

          \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot \left(x \cdot x\right) - \frac{1}{24}, x \cdot x, \frac{1}{2}\right) \]
        3. lift-*.f64N/A

          \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot \left(x \cdot x\right) - \frac{1}{24}, x \cdot x, \frac{1}{2}\right) \]
        4. pow2N/A

          \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}, x \cdot x, \frac{1}{2}\right) \]
        5. metadata-evalN/A

          \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24} \cdot 1, x \cdot x, \frac{1}{2}\right) \]
        6. fp-cancel-sub-sign-invN/A

          \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} + \left(\mathsf{neg}\left(\frac{1}{24}\right)\right) \cdot 1, \color{blue}{x} \cdot x, \frac{1}{2}\right) \]
        7. *-commutativeN/A

          \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \frac{1}{720} + \left(\mathsf{neg}\left(\frac{1}{24}\right)\right) \cdot 1, x \cdot x, \frac{1}{2}\right) \]
        8. metadata-evalN/A

          \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \frac{1}{720} + \frac{-1}{24} \cdot 1, x \cdot x, \frac{1}{2}\right) \]
        9. metadata-evalN/A

          \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \frac{1}{720} + \frac{-1}{24}, x \cdot x, \frac{1}{2}\right) \]
        10. lower-fma.f64N/A

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left({x}^{2}, \frac{1}{720}, \frac{-1}{24}\right), \color{blue}{x} \cdot x, \frac{1}{2}\right) \]
        11. pow2N/A

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, \frac{1}{720}, \frac{-1}{24}\right), x \cdot x, \frac{1}{2}\right) \]
        12. lift-*.f6464.9

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, 0.001388888888888889, -0.041666666666666664\right), x \cdot x, 0.5\right) \]
      11. Applied rewrites64.9%

        \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, 0.001388888888888889, -0.041666666666666664\right), \color{blue}{x \cdot x}, 0.5\right) \]

      if 2.45000000000000007e33 < x

      1. Initial program 99.5%

        \[\frac{1 - \cos x}{x \cdot x} \]
      2. Add Preprocessing
      3. Taylor expanded in x around 0

        \[\leadsto \frac{1 - \color{blue}{1}}{x \cdot x} \]
      4. Step-by-step derivation
        1. Applied rewrites55.5%

          \[\leadsto \frac{1 - \color{blue}{1}}{x \cdot x} \]
        2. Step-by-step derivation
          1. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{1 - 1}{x \cdot x}} \]
          2. lift-*.f64N/A

            \[\leadsto \frac{1 - 1}{\color{blue}{x \cdot x}} \]
          3. pow2N/A

            \[\leadsto \frac{1 - 1}{\color{blue}{{x}^{2}}} \]
          4. lift--.f64N/A

            \[\leadsto \frac{\color{blue}{1 - 1}}{{x}^{2}} \]
          5. div-subN/A

            \[\leadsto \color{blue}{\frac{1}{{x}^{2}} - \frac{1}{{x}^{2}}} \]
          6. lower--.f64N/A

            \[\leadsto \color{blue}{\frac{1}{{x}^{2}} - \frac{1}{{x}^{2}}} \]
          7. pow-flipN/A

            \[\leadsto \color{blue}{{x}^{\left(\mathsf{neg}\left(2\right)\right)}} - \frac{1}{{x}^{2}} \]
          8. lower-pow.f64N/A

            \[\leadsto \color{blue}{{x}^{\left(\mathsf{neg}\left(2\right)\right)}} - \frac{1}{{x}^{2}} \]
          9. metadata-evalN/A

            \[\leadsto {x}^{\color{blue}{-2}} - \frac{1}{{x}^{2}} \]
          10. lower-/.f64N/A

            \[\leadsto {x}^{-2} - \color{blue}{\frac{1}{{x}^{2}}} \]
          11. pow2N/A

            \[\leadsto {x}^{-2} - \frac{1}{\color{blue}{x \cdot x}} \]
          12. lift-*.f6455.8

            \[\leadsto {x}^{-2} - \frac{1}{\color{blue}{x \cdot x}} \]
        3. Applied rewrites55.8%

          \[\leadsto \color{blue}{{x}^{-2} - \frac{1}{x \cdot x}} \]
        4. Step-by-step derivation
          1. lift-pow.f64N/A

            \[\leadsto \color{blue}{{x}^{-2}} - \frac{1}{x \cdot x} \]
          2. metadata-evalN/A

            \[\leadsto {x}^{\color{blue}{\left(\mathsf{neg}\left(2\right)\right)}} - \frac{1}{x \cdot x} \]
          3. pow-flipN/A

            \[\leadsto \color{blue}{\frac{1}{{x}^{2}}} - \frac{1}{x \cdot x} \]
          4. pow2N/A

            \[\leadsto \frac{1}{\color{blue}{x \cdot x}} - \frac{1}{x \cdot x} \]
          5. associate-/r*N/A

            \[\leadsto \color{blue}{\frac{\frac{1}{x}}{x}} - \frac{1}{x \cdot x} \]
          6. frac-2negN/A

            \[\leadsto \color{blue}{\frac{\mathsf{neg}\left(\frac{1}{x}\right)}{\mathsf{neg}\left(x\right)}} - \frac{1}{x \cdot x} \]
          7. distribute-frac-neg2N/A

            \[\leadsto \frac{\color{blue}{\frac{1}{\mathsf{neg}\left(x\right)}}}{\mathsf{neg}\left(x\right)} - \frac{1}{x \cdot x} \]
          8. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{\frac{1}{\mathsf{neg}\left(x\right)}}{\mathsf{neg}\left(x\right)}} - \frac{1}{x \cdot x} \]
          9. metadata-evalN/A

            \[\leadsto \frac{\frac{\color{blue}{\mathsf{neg}\left(-1\right)}}{\mathsf{neg}\left(x\right)}}{\mathsf{neg}\left(x\right)} - \frac{1}{x \cdot x} \]
          10. frac-2neg-revN/A

            \[\leadsto \frac{\color{blue}{\frac{-1}{x}}}{\mathsf{neg}\left(x\right)} - \frac{1}{x \cdot x} \]
          11. lower-/.f64N/A

            \[\leadsto \frac{\color{blue}{\frac{-1}{x}}}{\mathsf{neg}\left(x\right)} - \frac{1}{x \cdot x} \]
          12. lift-neg.f6455.6

            \[\leadsto \frac{\frac{-1}{x}}{\color{blue}{-x}} - \frac{1}{x \cdot x} \]
        5. Applied rewrites55.6%

          \[\leadsto \color{blue}{\frac{\frac{-1}{x}}{-x}} - \frac{1}{x \cdot x} \]
      5. Recombined 2 regimes into one program.
      6. Final simplification62.9%

        \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 2.45 \cdot 10^{+33}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, 0.001388888888888889, -0.041666666666666664\right), x \cdot x, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;-\left(\frac{\frac{-1}{x}}{x} + \frac{1}{x \cdot x}\right)\\ \end{array} \]
      7. Add Preprocessing

      Alternative 5: 76.3% accurate, 4.1× speedup?

      \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;x\_m \leq 6.6 \cdot 10^{+38}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(x\_m \cdot x\_m, 0.001388888888888889, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - 1}{x\_m \cdot x\_m}\\ \end{array} \end{array} \]
      x_m = (fabs.f64 x)
      (FPCore (x_m)
       :precision binary64
       (if (<= x_m 6.6e+38)
         (fma
          (fma (* x_m x_m) 0.001388888888888889 -0.041666666666666664)
          (* x_m x_m)
          0.5)
         (/ (- 1.0 1.0) (* x_m x_m))))
      x_m = fabs(x);
      double code(double x_m) {
      	double tmp;
      	if (x_m <= 6.6e+38) {
      		tmp = fma(fma((x_m * x_m), 0.001388888888888889, -0.041666666666666664), (x_m * x_m), 0.5);
      	} else {
      		tmp = (1.0 - 1.0) / (x_m * x_m);
      	}
      	return tmp;
      }
      
      x_m = abs(x)
      function code(x_m)
      	tmp = 0.0
      	if (x_m <= 6.6e+38)
      		tmp = fma(fma(Float64(x_m * x_m), 0.001388888888888889, -0.041666666666666664), Float64(x_m * x_m), 0.5);
      	else
      		tmp = Float64(Float64(1.0 - 1.0) / Float64(x_m * x_m));
      	end
      	return tmp
      end
      
      x_m = N[Abs[x], $MachinePrecision]
      code[x$95$m_] := If[LessEqual[x$95$m, 6.6e+38], N[(N[(N[(x$95$m * x$95$m), $MachinePrecision] * 0.001388888888888889 + -0.041666666666666664), $MachinePrecision] * N[(x$95$m * x$95$m), $MachinePrecision] + 0.5), $MachinePrecision], N[(N[(1.0 - 1.0), $MachinePrecision] / N[(x$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]]
      
      \begin{array}{l}
      x_m = \left|x\right|
      
      \\
      \begin{array}{l}
      \mathbf{if}\;x\_m \leq 6.6 \cdot 10^{+38}:\\
      \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(x\_m \cdot x\_m, 0.001388888888888889, -0.041666666666666664\right), x\_m \cdot x\_m, 0.5\right)\\
      
      \mathbf{else}:\\
      \;\;\;\;\frac{1 - 1}{x\_m \cdot x\_m}\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if x < 6.5999999999999998e38

        1. Initial program 37.3%

          \[\frac{1 - \cos x}{x \cdot x} \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-*.f64N/A

            \[\leadsto \frac{1 - \cos x}{\color{blue}{x \cdot x}} \]
          2. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{1 - \cos x}{x \cdot x}} \]
          3. lift--.f64N/A

            \[\leadsto \frac{\color{blue}{1 - \cos x}}{x \cdot x} \]
          4. lift-cos.f64N/A

            \[\leadsto \frac{1 - \color{blue}{\cos x}}{x \cdot x} \]
          5. flip--N/A

            \[\leadsto \frac{\color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}}{x \cdot x} \]
          6. pow2N/A

            \[\leadsto \frac{\frac{1 \cdot 1 - \cos x \cdot \cos x}{1 + \cos x}}{\color{blue}{{x}^{2}}} \]
          7. associate-/l/N/A

            \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
          8. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{1 \cdot 1 - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
          9. metadata-evalN/A

            \[\leadsto \frac{\color{blue}{1} - \cos x \cdot \cos x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
          10. 1-sub-cosN/A

            \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
          11. lower-*.f64N/A

            \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
          12. lower-sin.f64N/A

            \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
          13. lower-sin.f64N/A

            \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(1 + \cos x\right) \cdot {x}^{2}} \]
          14. lower-*.f64N/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(1 + \cos x\right) \cdot {x}^{2}}} \]
          15. +-commutativeN/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
          16. lower-+.f64N/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot {x}^{2}} \]
          17. lift-cos.f64N/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot {x}^{2}} \]
          18. pow2N/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
          19. lift-*.f6470.7

            \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
        4. Applied rewrites70.7%

          \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
        5. Step-by-step derivation
          1. lift-/.f64N/A

            \[\leadsto \color{blue}{\frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
          2. lift-*.f64N/A

            \[\leadsto \frac{\color{blue}{\sin x \cdot \sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
          3. lift-sin.f64N/A

            \[\leadsto \frac{\color{blue}{\sin x} \cdot \sin x}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
          4. lift-sin.f64N/A

            \[\leadsto \frac{\sin x \cdot \color{blue}{\sin x}}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)} \]
          5. lift-*.f64N/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right) \cdot \left(x \cdot x\right)}} \]
          6. lift-+.f64N/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{\left(\cos x + 1\right)} \cdot \left(x \cdot x\right)} \]
          7. lift-cos.f64N/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\left(\color{blue}{\cos x} + 1\right) \cdot \left(x \cdot x\right)} \]
          8. lift-*.f64N/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{\left(x \cdot x\right)}} \]
          9. pow2N/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\left(\cos x + 1\right) \cdot \color{blue}{{x}^{2}}} \]
          10. *-commutativeN/A

            \[\leadsto \frac{\sin x \cdot \sin x}{\color{blue}{{x}^{2} \cdot \left(\cos x + 1\right)}} \]
          11. times-fracN/A

            \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
          12. lower-*.f64N/A

            \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1}} \]
          13. lower-/.f64N/A

            \[\leadsto \color{blue}{\frac{\sin x}{{x}^{2}}} \cdot \frac{\sin x}{\cos x + 1} \]
          14. lift-sin.f64N/A

            \[\leadsto \frac{\color{blue}{\sin x}}{{x}^{2}} \cdot \frac{\sin x}{\cos x + 1} \]
          15. pow2N/A

            \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
          16. lift-*.f64N/A

            \[\leadsto \frac{\sin x}{\color{blue}{x \cdot x}} \cdot \frac{\sin x}{\cos x + 1} \]
          17. +-commutativeN/A

            \[\leadsto \frac{\sin x}{x \cdot x} \cdot \frac{\sin x}{\color{blue}{1 + \cos x}} \]
          18. hang-0p-tanN/A

            \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
          19. lower-tan.f64N/A

            \[\leadsto \frac{\sin x}{x \cdot x} \cdot \color{blue}{\tan \left(\frac{x}{2}\right)} \]
          20. lower-/.f6471.0

            \[\leadsto \frac{\sin x}{x \cdot x} \cdot \tan \color{blue}{\left(\frac{x}{2}\right)} \]
        6. Applied rewrites71.0%

          \[\leadsto \color{blue}{\frac{\sin x}{x \cdot x} \cdot \tan \left(\frac{x}{2}\right)} \]
        7. Taylor expanded in x around 0

          \[\leadsto \color{blue}{\frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right)} \]
        8. Step-by-step derivation
          1. lift-sin.f64N/A

            \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          2. lift-sin.f64N/A

            \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          3. pow2N/A

            \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          4. associate-*l/N/A

            \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          5. pow2N/A

            \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          6. hang-0p-tan-revN/A

            \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          7. associate-*r/N/A

            \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          8. 1-sub-cosN/A

            \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          9. metadata-evalN/A

            \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          10. flip--N/A

            \[\leadsto \frac{1}{2} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          11. associate-/l/N/A

            \[\leadsto \color{blue}{\frac{1}{2}} + {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \]
          12. +-commutativeN/A

            \[\leadsto {x}^{2} \cdot \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) + \color{blue}{\frac{1}{2}} \]
          13. *-commutativeN/A

            \[\leadsto \left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}\right) \cdot {x}^{2} + \frac{1}{2} \]
          14. lower-fma.f64N/A

            \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}, \color{blue}{{x}^{2}}, \frac{1}{2}\right) \]
        9. Applied rewrites64.9%

          \[\leadsto \color{blue}{\mathsf{fma}\left(0.001388888888888889 \cdot \left(x \cdot x\right) - 0.041666666666666664, x \cdot x, 0.5\right)} \]
        10. Step-by-step derivation
          1. lift--.f64N/A

            \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot \left(x \cdot x\right) - \frac{1}{24}, \color{blue}{x} \cdot x, \frac{1}{2}\right) \]
          2. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot \left(x \cdot x\right) - \frac{1}{24}, x \cdot x, \frac{1}{2}\right) \]
          3. lift-*.f64N/A

            \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot \left(x \cdot x\right) - \frac{1}{24}, x \cdot x, \frac{1}{2}\right) \]
          4. pow2N/A

            \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24}, x \cdot x, \frac{1}{2}\right) \]
          5. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} - \frac{1}{24} \cdot 1, x \cdot x, \frac{1}{2}\right) \]
          6. fp-cancel-sub-sign-invN/A

            \[\leadsto \mathsf{fma}\left(\frac{1}{720} \cdot {x}^{2} + \left(\mathsf{neg}\left(\frac{1}{24}\right)\right) \cdot 1, \color{blue}{x} \cdot x, \frac{1}{2}\right) \]
          7. *-commutativeN/A

            \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \frac{1}{720} + \left(\mathsf{neg}\left(\frac{1}{24}\right)\right) \cdot 1, x \cdot x, \frac{1}{2}\right) \]
          8. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \frac{1}{720} + \frac{-1}{24} \cdot 1, x \cdot x, \frac{1}{2}\right) \]
          9. metadata-evalN/A

            \[\leadsto \mathsf{fma}\left({x}^{2} \cdot \frac{1}{720} + \frac{-1}{24}, x \cdot x, \frac{1}{2}\right) \]
          10. lower-fma.f64N/A

            \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left({x}^{2}, \frac{1}{720}, \frac{-1}{24}\right), \color{blue}{x} \cdot x, \frac{1}{2}\right) \]
          11. pow2N/A

            \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, \frac{1}{720}, \frac{-1}{24}\right), x \cdot x, \frac{1}{2}\right) \]
          12. lift-*.f6464.9

            \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, 0.001388888888888889, -0.041666666666666664\right), x \cdot x, 0.5\right) \]
        11. Applied rewrites64.9%

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(x \cdot x, 0.001388888888888889, -0.041666666666666664\right), \color{blue}{x \cdot x}, 0.5\right) \]

        if 6.5999999999999998e38 < x

        1. Initial program 99.5%

          \[\frac{1 - \cos x}{x \cdot x} \]
        2. Add Preprocessing
        3. Taylor expanded in x around 0

          \[\leadsto \frac{1 - \color{blue}{1}}{x \cdot x} \]
        4. Step-by-step derivation
          1. Applied rewrites55.5%

            \[\leadsto \frac{1 - \color{blue}{1}}{x \cdot x} \]
        5. Recombined 2 regimes into one program.
        6. Add Preprocessing

        Alternative 6: 76.0% accurate, 4.6× speedup?

        \[\begin{array}{l} x_m = \left|x\right| \\ \begin{array}{l} \mathbf{if}\;x\_m \leq 3.5:\\ \;\;\;\;\mathsf{fma}\left(x\_m \cdot x\_m, -0.041666666666666664, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - 1}{x\_m \cdot x\_m}\\ \end{array} \end{array} \]
        x_m = (fabs.f64 x)
        (FPCore (x_m)
         :precision binary64
         (if (<= x_m 3.5)
           (fma (* x_m x_m) -0.041666666666666664 0.5)
           (/ (- 1.0 1.0) (* x_m x_m))))
        x_m = fabs(x);
        double code(double x_m) {
        	double tmp;
        	if (x_m <= 3.5) {
        		tmp = fma((x_m * x_m), -0.041666666666666664, 0.5);
        	} else {
        		tmp = (1.0 - 1.0) / (x_m * x_m);
        	}
        	return tmp;
        }
        
        x_m = abs(x)
        function code(x_m)
        	tmp = 0.0
        	if (x_m <= 3.5)
        		tmp = fma(Float64(x_m * x_m), -0.041666666666666664, 0.5);
        	else
        		tmp = Float64(Float64(1.0 - 1.0) / Float64(x_m * x_m));
        	end
        	return tmp
        end
        
        x_m = N[Abs[x], $MachinePrecision]
        code[x$95$m_] := If[LessEqual[x$95$m, 3.5], N[(N[(x$95$m * x$95$m), $MachinePrecision] * -0.041666666666666664 + 0.5), $MachinePrecision], N[(N[(1.0 - 1.0), $MachinePrecision] / N[(x$95$m * x$95$m), $MachinePrecision]), $MachinePrecision]]
        
        \begin{array}{l}
        x_m = \left|x\right|
        
        \\
        \begin{array}{l}
        \mathbf{if}\;x\_m \leq 3.5:\\
        \;\;\;\;\mathsf{fma}\left(x\_m \cdot x\_m, -0.041666666666666664, 0.5\right)\\
        
        \mathbf{else}:\\
        \;\;\;\;\frac{1 - 1}{x\_m \cdot x\_m}\\
        
        
        \end{array}
        \end{array}
        
        Derivation
        1. Split input into 2 regimes
        2. if x < 3.5

          1. Initial program 36.1%

            \[\frac{1 - \cos x}{x \cdot x} \]
          2. Add Preprocessing
          3. Taylor expanded in x around 0

            \[\leadsto \color{blue}{\frac{1}{2} + \frac{-1}{24} \cdot {x}^{2}} \]
          4. Step-by-step derivation
            1. +-commutativeN/A

              \[\leadsto \frac{-1}{24} \cdot {x}^{2} + \color{blue}{\frac{1}{2}} \]
            2. *-commutativeN/A

              \[\leadsto {x}^{2} \cdot \frac{-1}{24} + \frac{1}{2} \]
            3. lower-fma.f64N/A

              \[\leadsto \mathsf{fma}\left({x}^{2}, \color{blue}{\frac{-1}{24}}, \frac{1}{2}\right) \]
            4. pow2N/A

              \[\leadsto \mathsf{fma}\left(x \cdot x, \frac{-1}{24}, \frac{1}{2}\right) \]
            5. lift-*.f6465.8

              \[\leadsto \mathsf{fma}\left(x \cdot x, -0.041666666666666664, 0.5\right) \]
          5. Applied rewrites65.8%

            \[\leadsto \color{blue}{\mathsf{fma}\left(x \cdot x, -0.041666666666666664, 0.5\right)} \]

          if 3.5 < x

          1. Initial program 99.5%

            \[\frac{1 - \cos x}{x \cdot x} \]
          2. Add Preprocessing
          3. Taylor expanded in x around 0

            \[\leadsto \frac{1 - \color{blue}{1}}{x \cdot x} \]
          4. Step-by-step derivation
            1. Applied rewrites52.0%

              \[\leadsto \frac{1 - \color{blue}{1}}{x \cdot x} \]
          5. Recombined 2 regimes into one program.
          6. Final simplification62.6%

            \[\leadsto \begin{array}{l} \mathbf{if}\;x \leq 3.5:\\ \;\;\;\;\mathsf{fma}\left(x \cdot x, -0.041666666666666664, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{1 - 1}{x \cdot x}\\ \end{array} \]
          7. Add Preprocessing

          Alternative 7: 51.2% accurate, 120.0× speedup?

          \[\begin{array}{l} x_m = \left|x\right| \\ 0.5 \end{array} \]
          x_m = (fabs.f64 x)
          (FPCore (x_m) :precision binary64 0.5)
          x_m = fabs(x);
          double code(double x_m) {
          	return 0.5;
          }
          
          x_m =     private
          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(x_m)
          use fmin_fmax_functions
              real(8), intent (in) :: x_m
              code = 0.5d0
          end function
          
          x_m = Math.abs(x);
          public static double code(double x_m) {
          	return 0.5;
          }
          
          x_m = math.fabs(x)
          def code(x_m):
          	return 0.5
          
          x_m = abs(x)
          function code(x_m)
          	return 0.5
          end
          
          x_m = abs(x);
          function tmp = code(x_m)
          	tmp = 0.5;
          end
          
          x_m = N[Abs[x], $MachinePrecision]
          code[x$95$m_] := 0.5
          
          \begin{array}{l}
          x_m = \left|x\right|
          
          \\
          0.5
          \end{array}
          
          Derivation
          1. Initial program 50.7%

            \[\frac{1 - \cos x}{x \cdot x} \]
          2. Add Preprocessing
          3. Taylor expanded in x around 0

            \[\leadsto \color{blue}{\frac{1}{2}} \]
          4. Step-by-step derivation
            1. Applied rewrites51.8%

              \[\leadsto \color{blue}{0.5} \]
            2. Final simplification51.8%

              \[\leadsto 0.5 \]
            3. Add Preprocessing

            Reproduce

            ?
            herbie shell --seed 2025064 
            (FPCore (x)
              :name "cos2 (problem 3.4.1)"
              :precision binary64
              (/ (- 1.0 (cos x)) (* x x)))