Kahan p13 Example 2

Percentage Accurate: 99.9% → 100.0%
Time: 8.8s
Alternatives: 9
Speedup: 2.0×

Specification

?
\[\begin{array}{l} \\ \begin{array}{l} t_1 := 2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\\ t_2 := t\_1 \cdot t\_1\\ \frac{1 + t\_2}{2 + t\_2} \end{array} \end{array} \]
(FPCore (t)
 :precision binary64
 (let* ((t_1 (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))))) (t_2 (* t_1 t_1)))
   (/ (+ 1.0 t_2) (+ 2.0 t_2))))
double code(double t) {
	double t_1 = 2.0 - ((2.0 / t) / (1.0 + (1.0 / t)));
	double t_2 = t_1 * t_1;
	return (1.0 + t_2) / (2.0 + t_2);
}
real(8) function code(t)
    real(8), intent (in) :: t
    real(8) :: t_1
    real(8) :: t_2
    t_1 = 2.0d0 - ((2.0d0 / t) / (1.0d0 + (1.0d0 / t)))
    t_2 = t_1 * t_1
    code = (1.0d0 + t_2) / (2.0d0 + t_2)
end function
public static double code(double t) {
	double t_1 = 2.0 - ((2.0 / t) / (1.0 + (1.0 / t)));
	double t_2 = t_1 * t_1;
	return (1.0 + t_2) / (2.0 + t_2);
}
def code(t):
	t_1 = 2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))
	t_2 = t_1 * t_1
	return (1.0 + t_2) / (2.0 + t_2)
function code(t)
	t_1 = Float64(2.0 - Float64(Float64(2.0 / t) / Float64(1.0 + Float64(1.0 / t))))
	t_2 = Float64(t_1 * t_1)
	return Float64(Float64(1.0 + t_2) / Float64(2.0 + t_2))
end
function tmp = code(t)
	t_1 = 2.0 - ((2.0 / t) / (1.0 + (1.0 / t)));
	t_2 = t_1 * t_1;
	tmp = (1.0 + t_2) / (2.0 + t_2);
end
code[t_] := Block[{t$95$1 = N[(2.0 - N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[(1.0 / t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(t$95$1 * t$95$1), $MachinePrecision]}, N[(N[(1.0 + t$95$2), $MachinePrecision] / N[(2.0 + t$95$2), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := 2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\\
t_2 := t\_1 \cdot t\_1\\
\frac{1 + t\_2}{2 + t\_2}
\end{array}
\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 9 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: 99.9% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := 2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\\ t_2 := t\_1 \cdot t\_1\\ \frac{1 + t\_2}{2 + t\_2} \end{array} \end{array} \]
(FPCore (t)
 :precision binary64
 (let* ((t_1 (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))))) (t_2 (* t_1 t_1)))
   (/ (+ 1.0 t_2) (+ 2.0 t_2))))
double code(double t) {
	double t_1 = 2.0 - ((2.0 / t) / (1.0 + (1.0 / t)));
	double t_2 = t_1 * t_1;
	return (1.0 + t_2) / (2.0 + t_2);
}
real(8) function code(t)
    real(8), intent (in) :: t
    real(8) :: t_1
    real(8) :: t_2
    t_1 = 2.0d0 - ((2.0d0 / t) / (1.0d0 + (1.0d0 / t)))
    t_2 = t_1 * t_1
    code = (1.0d0 + t_2) / (2.0d0 + t_2)
end function
public static double code(double t) {
	double t_1 = 2.0 - ((2.0 / t) / (1.0 + (1.0 / t)));
	double t_2 = t_1 * t_1;
	return (1.0 + t_2) / (2.0 + t_2);
}
def code(t):
	t_1 = 2.0 - ((2.0 / t) / (1.0 + (1.0 / t)))
	t_2 = t_1 * t_1
	return (1.0 + t_2) / (2.0 + t_2)
function code(t)
	t_1 = Float64(2.0 - Float64(Float64(2.0 / t) / Float64(1.0 + Float64(1.0 / t))))
	t_2 = Float64(t_1 * t_1)
	return Float64(Float64(1.0 + t_2) / Float64(2.0 + t_2))
end
function tmp = code(t)
	t_1 = 2.0 - ((2.0 / t) / (1.0 + (1.0 / t)));
	t_2 = t_1 * t_1;
	tmp = (1.0 + t_2) / (2.0 + t_2);
end
code[t_] := Block[{t$95$1 = N[(2.0 - N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[(1.0 / t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(t$95$1 * t$95$1), $MachinePrecision]}, N[(N[(1.0 + t$95$2), $MachinePrecision] / N[(2.0 + t$95$2), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := 2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\\
t_2 := t\_1 \cdot t\_1\\
\frac{1 + t\_2}{2 + t\_2}
\end{array}
\end{array}

Alternative 1: 100.0% accurate, 2.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := \frac{-2}{1 + t} + 2\\ t_2 := 2 + \frac{-2}{t + 1}\\ \frac{\mathsf{fma}\left(t\_1, t\_1, 1\right)}{\mathsf{fma}\left(t\_2, t\_2, 2\right)} \end{array} \end{array} \]
(FPCore (t)
 :precision binary64
 (let* ((t_1 (+ (/ -2.0 (+ 1.0 t)) 2.0)) (t_2 (+ 2.0 (/ -2.0 (+ t 1.0)))))
   (/ (fma t_1 t_1 1.0) (fma t_2 t_2 2.0))))
double code(double t) {
	double t_1 = (-2.0 / (1.0 + t)) + 2.0;
	double t_2 = 2.0 + (-2.0 / (t + 1.0));
	return fma(t_1, t_1, 1.0) / fma(t_2, t_2, 2.0);
}
function code(t)
	t_1 = Float64(Float64(-2.0 / Float64(1.0 + t)) + 2.0)
	t_2 = Float64(2.0 + Float64(-2.0 / Float64(t + 1.0)))
	return Float64(fma(t_1, t_1, 1.0) / fma(t_2, t_2, 2.0))
end
code[t_] := Block[{t$95$1 = N[(N[(-2.0 / N[(1.0 + t), $MachinePrecision]), $MachinePrecision] + 2.0), $MachinePrecision]}, Block[{t$95$2 = N[(2.0 + N[(-2.0 / N[(t + 1.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[(N[(t$95$1 * t$95$1 + 1.0), $MachinePrecision] / N[(t$95$2 * t$95$2 + 2.0), $MachinePrecision]), $MachinePrecision]]]
\begin{array}{l}

\\
\begin{array}{l}
t_1 := \frac{-2}{1 + t} + 2\\
t_2 := 2 + \frac{-2}{t + 1}\\
\frac{\mathsf{fma}\left(t\_1, t\_1, 1\right)}{\mathsf{fma}\left(t\_2, t\_2, 2\right)}
\end{array}
\end{array}
Derivation
  1. Initial program 100.0%

    \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
  2. Add Preprocessing
  3. Step-by-step derivation
    1. lift-+.f64N/A

      \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
    2. +-commutativeN/A

      \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
    3. flip-+N/A

      \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
    4. div-invN/A

      \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
    5. lower-*.f64N/A

      \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
  4. Applied rewrites100.0%

    \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
  5. Applied rewrites100.0%

    \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
  6. Step-by-step derivation
    1. Applied rewrites100.0%

      \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{2 + \color{blue}{\left(\frac{-2}{1 + t} + 2\right) \cdot \left(\frac{-2}{1 + t} + 2\right)}} \]
    2. Step-by-step derivation
      1. lift-+.f64N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\color{blue}{2 + \left(\frac{-2}{1 + t} + 2\right) \cdot \left(\frac{-2}{1 + t} + 2\right)}} \]
      2. +-commutativeN/A

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

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\color{blue}{\left(\frac{-2}{1 + t} + 2\right) \cdot \left(\frac{-2}{1 + t} + 2\right)} + 2} \]
      4. lower-fma.f64100.0

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\color{blue}{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 2\right)}} \]
      5. lift-+.f64N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(\color{blue}{\frac{-2}{1 + t} + 2}, \frac{-2}{1 + t} + 2, 2\right)} \]
      6. +-commutativeN/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(\color{blue}{2 + \frac{-2}{1 + t}}, \frac{-2}{1 + t} + 2, 2\right)} \]
      7. lower-+.f64100.0

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(\color{blue}{2 + \frac{-2}{1 + t}}, \frac{-2}{1 + t} + 2, 2\right)} \]
      8. lift-+.f64N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(2 + \frac{-2}{\color{blue}{1 + t}}, \frac{-2}{1 + t} + 2, 2\right)} \]
      9. +-commutativeN/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(2 + \frac{-2}{\color{blue}{t + 1}}, \frac{-2}{1 + t} + 2, 2\right)} \]
      10. lower-+.f64100.0

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(2 + \frac{-2}{\color{blue}{t + 1}}, \frac{-2}{1 + t} + 2, 2\right)} \]
      11. lift-+.f64N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(2 + \frac{-2}{t + 1}, \color{blue}{\frac{-2}{1 + t} + 2}, 2\right)} \]
      12. +-commutativeN/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(2 + \frac{-2}{t + 1}, \color{blue}{2 + \frac{-2}{1 + t}}, 2\right)} \]
      13. lower-+.f64100.0

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(2 + \frac{-2}{t + 1}, \color{blue}{2 + \frac{-2}{1 + t}}, 2\right)} \]
      14. lift-+.f64N/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(2 + \frac{-2}{t + 1}, 2 + \frac{-2}{\color{blue}{1 + t}}, 2\right)} \]
      15. +-commutativeN/A

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(2 + \frac{-2}{t + 1}, 2 + \frac{-2}{\color{blue}{t + 1}}, 2\right)} \]
      16. lower-+.f64100.0

        \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\mathsf{fma}\left(2 + \frac{-2}{t + 1}, 2 + \frac{-2}{\color{blue}{t + 1}}, 2\right)} \]
    3. Applied rewrites100.0%

      \[\leadsto \frac{\mathsf{fma}\left(\frac{-2}{1 + t} + 2, \frac{-2}{1 + t} + 2, 1\right)}{\color{blue}{\mathsf{fma}\left(2 + \frac{-2}{t + 1}, 2 + \frac{-2}{t + 1}, 2\right)}} \]
    4. Add Preprocessing

    Alternative 2: 99.0% accurate, 1.1× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)\\ \end{array} \end{array} \]
    (FPCore (t)
     :precision binary64
     (if (<= (/ (/ 2.0 t) (+ 1.0 (pow t -1.0))) 1e-11)
       (-
        0.8333333333333334
        (/
         (-
          0.2222222222222222
          (/ (+ (/ 0.04938271604938271 t) 0.037037037037037035) t))
         t))
       (fma (fma (- t 2.0) t 1.0) (* t t) 0.5)))
    double code(double t) {
    	double tmp;
    	if (((2.0 / t) / (1.0 + pow(t, -1.0))) <= 1e-11) {
    		tmp = 0.8333333333333334 - ((0.2222222222222222 - (((0.04938271604938271 / t) + 0.037037037037037035) / t)) / t);
    	} else {
    		tmp = fma(fma((t - 2.0), t, 1.0), (t * t), 0.5);
    	}
    	return tmp;
    }
    
    function code(t)
    	tmp = 0.0
    	if (Float64(Float64(2.0 / t) / Float64(1.0 + (t ^ -1.0))) <= 1e-11)
    		tmp = Float64(0.8333333333333334 - Float64(Float64(0.2222222222222222 - Float64(Float64(Float64(0.04938271604938271 / t) + 0.037037037037037035) / t)) / t));
    	else
    		tmp = fma(fma(Float64(t - 2.0), t, 1.0), Float64(t * t), 0.5);
    	end
    	return tmp
    end
    
    code[t_] := If[LessEqual[N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[Power[t, -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 1e-11], N[(0.8333333333333334 - N[(N[(0.2222222222222222 - N[(N[(N[(0.04938271604938271 / t), $MachinePrecision] + 0.037037037037037035), $MachinePrecision] / t), $MachinePrecision]), $MachinePrecision] / t), $MachinePrecision]), $MachinePrecision], N[(N[(N[(t - 2.0), $MachinePrecision] * t + 1.0), $MachinePrecision] * N[(t * t), $MachinePrecision] + 0.5), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\
    \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\
    
    \mathbf{else}:\\
    \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t))) < 9.99999999999999939e-12

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around -inf

        \[\leadsto \color{blue}{\frac{5}{6} + -1 \cdot \frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}} \]
      6. Step-by-step derivation
        1. mul-1-negN/A

          \[\leadsto \frac{5}{6} + \color{blue}{\left(\mathsf{neg}\left(\frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}\right)\right)} \]
        2. unsub-negN/A

          \[\leadsto \color{blue}{\frac{5}{6} - \frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}} \]
        3. lower--.f64N/A

          \[\leadsto \color{blue}{\frac{5}{6} - \frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}} \]
        4. lower-/.f64N/A

          \[\leadsto \frac{5}{6} - \color{blue}{\frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}} \]
        5. mul-1-negN/A

          \[\leadsto \frac{5}{6} - \frac{\frac{2}{9} + \color{blue}{\left(\mathsf{neg}\left(\frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}\right)\right)}}{t} \]
        6. unsub-negN/A

          \[\leadsto \frac{5}{6} - \frac{\color{blue}{\frac{2}{9} - \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}}{t} \]
        7. lower--.f64N/A

          \[\leadsto \frac{5}{6} - \frac{\color{blue}{\frac{2}{9} - \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}}{t} \]
        8. lower-/.f64N/A

          \[\leadsto \frac{5}{6} - \frac{\frac{2}{9} - \color{blue}{\frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}}{t} \]
        9. +-commutativeN/A

          \[\leadsto \frac{5}{6} - \frac{\frac{2}{9} - \frac{\color{blue}{\frac{4}{81} \cdot \frac{1}{t} + \frac{1}{27}}}{t}}{t} \]
        10. lower-+.f64N/A

          \[\leadsto \frac{5}{6} - \frac{\frac{2}{9} - \frac{\color{blue}{\frac{4}{81} \cdot \frac{1}{t} + \frac{1}{27}}}{t}}{t} \]
        11. associate-*r/N/A

          \[\leadsto \frac{5}{6} - \frac{\frac{2}{9} - \frac{\color{blue}{\frac{\frac{4}{81} \cdot 1}{t}} + \frac{1}{27}}{t}}{t} \]
        12. metadata-evalN/A

          \[\leadsto \frac{5}{6} - \frac{\frac{2}{9} - \frac{\frac{\color{blue}{\frac{4}{81}}}{t} + \frac{1}{27}}{t}}{t} \]
        13. lower-/.f6499.7

          \[\leadsto 0.8333333333333334 - \frac{0.2222222222222222 - \frac{\color{blue}{\frac{0.04938271604938271}{t}} + 0.037037037037037035}{t}}{t} \]
      7. Applied rewrites99.7%

        \[\leadsto \color{blue}{0.8333333333333334 - \frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}} \]

      if 9.99999999999999939e-12 < (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around 0

        \[\leadsto \color{blue}{\frac{1}{2} + {t}^{2} \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

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

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(1 + t \cdot \left(t - 2\right), {t}^{2}, \frac{1}{2}\right)} \]
        4. +-commutativeN/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{t \cdot \left(t - 2\right) + 1}, {t}^{2}, \frac{1}{2}\right) \]
        5. *-commutativeN/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left(t - 2\right) \cdot t} + 1, {t}^{2}, \frac{1}{2}\right) \]
        6. lower-fma.f64N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(t - 2, t, 1\right)}, {t}^{2}, \frac{1}{2}\right) \]
        7. lower--.f64N/A

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{t - 2}, t, 1\right), {t}^{2}, \frac{1}{2}\right) \]
        8. unpow2N/A

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), \color{blue}{t \cdot t}, \frac{1}{2}\right) \]
        9. lower-*.f64100.0

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), \color{blue}{t \cdot t}, 0.5\right) \]
      7. Applied rewrites100.0%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification99.8%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)\\ \end{array} \]
    5. Add Preprocessing

    Alternative 3: 98.9% accurate, 1.1× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{0.037037037037037035}{t}}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)\\ \end{array} \end{array} \]
    (FPCore (t)
     :precision binary64
     (if (<= (/ (/ 2.0 t) (+ 1.0 (pow t -1.0))) 1e-11)
       (-
        0.8333333333333334
        (/ (- 0.2222222222222222 (/ 0.037037037037037035 t)) t))
       (fma (fma (- t 2.0) t 1.0) (* t t) 0.5)))
    double code(double t) {
    	double tmp;
    	if (((2.0 / t) / (1.0 + pow(t, -1.0))) <= 1e-11) {
    		tmp = 0.8333333333333334 - ((0.2222222222222222 - (0.037037037037037035 / t)) / t);
    	} else {
    		tmp = fma(fma((t - 2.0), t, 1.0), (t * t), 0.5);
    	}
    	return tmp;
    }
    
    function code(t)
    	tmp = 0.0
    	if (Float64(Float64(2.0 / t) / Float64(1.0 + (t ^ -1.0))) <= 1e-11)
    		tmp = Float64(0.8333333333333334 - Float64(Float64(0.2222222222222222 - Float64(0.037037037037037035 / t)) / t));
    	else
    		tmp = fma(fma(Float64(t - 2.0), t, 1.0), Float64(t * t), 0.5);
    	end
    	return tmp
    end
    
    code[t_] := If[LessEqual[N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[Power[t, -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 1e-11], N[(0.8333333333333334 - N[(N[(0.2222222222222222 - N[(0.037037037037037035 / t), $MachinePrecision]), $MachinePrecision] / t), $MachinePrecision]), $MachinePrecision], N[(N[(N[(t - 2.0), $MachinePrecision] * t + 1.0), $MachinePrecision] * N[(t * t), $MachinePrecision] + 0.5), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\
    \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{0.037037037037037035}{t}}{t}\\
    
    \mathbf{else}:\\
    \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t))) < 9.99999999999999939e-12

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around inf

        \[\leadsto \color{blue}{\left(\frac{5}{6} + \frac{\frac{1}{27}}{{t}^{2}}\right) - \frac{2}{9} \cdot \frac{1}{t}} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \color{blue}{\left(\frac{\frac{1}{27}}{{t}^{2}} + \frac{5}{6}\right)} - \frac{2}{9} \cdot \frac{1}{t} \]
        2. associate--l+N/A

          \[\leadsto \color{blue}{\frac{\frac{1}{27}}{{t}^{2}} + \left(\frac{5}{6} - \frac{2}{9} \cdot \frac{1}{t}\right)} \]
        3. +-commutativeN/A

          \[\leadsto \color{blue}{\left(\frac{5}{6} - \frac{2}{9} \cdot \frac{1}{t}\right) + \frac{\frac{1}{27}}{{t}^{2}}} \]
        4. associate--r-N/A

          \[\leadsto \color{blue}{\frac{5}{6} - \left(\frac{2}{9} \cdot \frac{1}{t} - \frac{\frac{1}{27}}{{t}^{2}}\right)} \]
        5. associate-*r/N/A

          \[\leadsto \frac{5}{6} - \left(\color{blue}{\frac{\frac{2}{9} \cdot 1}{t}} - \frac{\frac{1}{27}}{{t}^{2}}\right) \]
        6. metadata-evalN/A

          \[\leadsto \frac{5}{6} - \left(\frac{\color{blue}{\frac{2}{9}}}{t} - \frac{\frac{1}{27}}{{t}^{2}}\right) \]
        7. unpow2N/A

          \[\leadsto \frac{5}{6} - \left(\frac{\frac{2}{9}}{t} - \frac{\frac{1}{27}}{\color{blue}{t \cdot t}}\right) \]
        8. associate-/r*N/A

          \[\leadsto \frac{5}{6} - \left(\frac{\frac{2}{9}}{t} - \color{blue}{\frac{\frac{\frac{1}{27}}{t}}{t}}\right) \]
        9. metadata-evalN/A

          \[\leadsto \frac{5}{6} - \left(\frac{\frac{2}{9}}{t} - \frac{\frac{\color{blue}{\frac{1}{27} \cdot 1}}{t}}{t}\right) \]
        10. associate-*r/N/A

          \[\leadsto \frac{5}{6} - \left(\frac{\frac{2}{9}}{t} - \frac{\color{blue}{\frac{1}{27} \cdot \frac{1}{t}}}{t}\right) \]
        11. div-subN/A

          \[\leadsto \frac{5}{6} - \color{blue}{\frac{\frac{2}{9} - \frac{1}{27} \cdot \frac{1}{t}}{t}} \]
        12. lower--.f64N/A

          \[\leadsto \color{blue}{\frac{5}{6} - \frac{\frac{2}{9} - \frac{1}{27} \cdot \frac{1}{t}}{t}} \]
        13. lower-/.f64N/A

          \[\leadsto \frac{5}{6} - \color{blue}{\frac{\frac{2}{9} - \frac{1}{27} \cdot \frac{1}{t}}{t}} \]
        14. lower--.f64N/A

          \[\leadsto \frac{5}{6} - \frac{\color{blue}{\frac{2}{9} - \frac{1}{27} \cdot \frac{1}{t}}}{t} \]
        15. associate-*r/N/A

          \[\leadsto \frac{5}{6} - \frac{\frac{2}{9} - \color{blue}{\frac{\frac{1}{27} \cdot 1}{t}}}{t} \]
        16. metadata-evalN/A

          \[\leadsto \frac{5}{6} - \frac{\frac{2}{9} - \frac{\color{blue}{\frac{1}{27}}}{t}}{t} \]
        17. lower-/.f6499.5

          \[\leadsto 0.8333333333333334 - \frac{0.2222222222222222 - \color{blue}{\frac{0.037037037037037035}{t}}}{t} \]
      7. Applied rewrites99.5%

        \[\leadsto \color{blue}{0.8333333333333334 - \frac{0.2222222222222222 - \frac{0.037037037037037035}{t}}{t}} \]

      if 9.99999999999999939e-12 < (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around 0

        \[\leadsto \color{blue}{\frac{1}{2} + {t}^{2} \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

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

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(1 + t \cdot \left(t - 2\right), {t}^{2}, \frac{1}{2}\right)} \]
        4. +-commutativeN/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{t \cdot \left(t - 2\right) + 1}, {t}^{2}, \frac{1}{2}\right) \]
        5. *-commutativeN/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left(t - 2\right) \cdot t} + 1, {t}^{2}, \frac{1}{2}\right) \]
        6. lower-fma.f64N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(t - 2, t, 1\right)}, {t}^{2}, \frac{1}{2}\right) \]
        7. lower--.f64N/A

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{t - 2}, t, 1\right), {t}^{2}, \frac{1}{2}\right) \]
        8. unpow2N/A

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), \color{blue}{t \cdot t}, \frac{1}{2}\right) \]
        9. lower-*.f64100.0

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), \color{blue}{t \cdot t}, 0.5\right) \]
      7. Applied rewrites100.0%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification99.7%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{0.037037037037037035}{t}}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)\\ \end{array} \]
    5. Add Preprocessing

    Alternative 4: 98.9% accurate, 1.2× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)\\ \end{array} \end{array} \]
    (FPCore (t)
     :precision binary64
     (if (<= (/ (/ 2.0 t) (+ 1.0 (pow t -1.0))) 1e-11)
       (- 0.8333333333333334 (/ 0.2222222222222222 t))
       (fma (fma (- t 2.0) t 1.0) (* t t) 0.5)))
    double code(double t) {
    	double tmp;
    	if (((2.0 / t) / (1.0 + pow(t, -1.0))) <= 1e-11) {
    		tmp = 0.8333333333333334 - (0.2222222222222222 / t);
    	} else {
    		tmp = fma(fma((t - 2.0), t, 1.0), (t * t), 0.5);
    	}
    	return tmp;
    }
    
    function code(t)
    	tmp = 0.0
    	if (Float64(Float64(2.0 / t) / Float64(1.0 + (t ^ -1.0))) <= 1e-11)
    		tmp = Float64(0.8333333333333334 - Float64(0.2222222222222222 / t));
    	else
    		tmp = fma(fma(Float64(t - 2.0), t, 1.0), Float64(t * t), 0.5);
    	end
    	return tmp
    end
    
    code[t_] := If[LessEqual[N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[Power[t, -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 1e-11], N[(0.8333333333333334 - N[(0.2222222222222222 / t), $MachinePrecision]), $MachinePrecision], N[(N[(N[(t - 2.0), $MachinePrecision] * t + 1.0), $MachinePrecision] * N[(t * t), $MachinePrecision] + 0.5), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\
    \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\
    
    \mathbf{else}:\\
    \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t))) < 9.99999999999999939e-12

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around inf

        \[\leadsto \color{blue}{\frac{5}{6} - \frac{2}{9} \cdot \frac{1}{t}} \]
      6. Step-by-step derivation
        1. lower--.f64N/A

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

          \[\leadsto \frac{5}{6} - \color{blue}{\frac{\frac{2}{9} \cdot 1}{t}} \]
        3. metadata-evalN/A

          \[\leadsto \frac{5}{6} - \frac{\color{blue}{\frac{2}{9}}}{t} \]
        4. lower-/.f6499.3

          \[\leadsto 0.8333333333333334 - \color{blue}{\frac{0.2222222222222222}{t}} \]
      7. Applied rewrites99.3%

        \[\leadsto \color{blue}{0.8333333333333334 - \frac{0.2222222222222222}{t}} \]

      if 9.99999999999999939e-12 < (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around 0

        \[\leadsto \color{blue}{\frac{1}{2} + {t}^{2} \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

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

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(1 + t \cdot \left(t - 2\right), {t}^{2}, \frac{1}{2}\right)} \]
        4. +-commutativeN/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{t \cdot \left(t - 2\right) + 1}, {t}^{2}, \frac{1}{2}\right) \]
        5. *-commutativeN/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\left(t - 2\right) \cdot t} + 1, {t}^{2}, \frac{1}{2}\right) \]
        6. lower-fma.f64N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(t - 2, t, 1\right)}, {t}^{2}, \frac{1}{2}\right) \]
        7. lower--.f64N/A

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(\color{blue}{t - 2}, t, 1\right), {t}^{2}, \frac{1}{2}\right) \]
        8. unpow2N/A

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), \color{blue}{t \cdot t}, \frac{1}{2}\right) \]
        9. lower-*.f64100.0

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), \color{blue}{t \cdot t}, 0.5\right) \]
      7. Applied rewrites100.0%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification99.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(t - 2, t, 1\right), t \cdot t, 0.5\right)\\ \end{array} \]
    5. Add Preprocessing

    Alternative 5: 98.8% accurate, 1.2× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, t, 1\right), t \cdot t, 0.5\right)\\ \end{array} \end{array} \]
    (FPCore (t)
     :precision binary64
     (if (<= (/ (/ 2.0 t) (+ 1.0 (pow t -1.0))) 1e-11)
       (- 0.8333333333333334 (/ 0.2222222222222222 t))
       (fma (fma -2.0 t 1.0) (* t t) 0.5)))
    double code(double t) {
    	double tmp;
    	if (((2.0 / t) / (1.0 + pow(t, -1.0))) <= 1e-11) {
    		tmp = 0.8333333333333334 - (0.2222222222222222 / t);
    	} else {
    		tmp = fma(fma(-2.0, t, 1.0), (t * t), 0.5);
    	}
    	return tmp;
    }
    
    function code(t)
    	tmp = 0.0
    	if (Float64(Float64(2.0 / t) / Float64(1.0 + (t ^ -1.0))) <= 1e-11)
    		tmp = Float64(0.8333333333333334 - Float64(0.2222222222222222 / t));
    	else
    		tmp = fma(fma(-2.0, t, 1.0), Float64(t * t), 0.5);
    	end
    	return tmp
    end
    
    code[t_] := If[LessEqual[N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[Power[t, -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 1e-11], N[(0.8333333333333334 - N[(0.2222222222222222 / t), $MachinePrecision]), $MachinePrecision], N[(N[(-2.0 * t + 1.0), $MachinePrecision] * N[(t * t), $MachinePrecision] + 0.5), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\
    \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\
    
    \mathbf{else}:\\
    \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, t, 1\right), t \cdot t, 0.5\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t))) < 9.99999999999999939e-12

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around inf

        \[\leadsto \color{blue}{\frac{5}{6} - \frac{2}{9} \cdot \frac{1}{t}} \]
      6. Step-by-step derivation
        1. lower--.f64N/A

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

          \[\leadsto \frac{5}{6} - \color{blue}{\frac{\frac{2}{9} \cdot 1}{t}} \]
        3. metadata-evalN/A

          \[\leadsto \frac{5}{6} - \frac{\color{blue}{\frac{2}{9}}}{t} \]
        4. lower-/.f6499.3

          \[\leadsto 0.8333333333333334 - \color{blue}{\frac{0.2222222222222222}{t}} \]
      7. Applied rewrites99.3%

        \[\leadsto \color{blue}{0.8333333333333334 - \frac{0.2222222222222222}{t}} \]

      if 9.99999999999999939e-12 < (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around 0

        \[\leadsto \color{blue}{\frac{1}{2} + {t}^{2} \cdot \left(1 + -2 \cdot t\right)} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

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

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

          \[\leadsto \color{blue}{\mathsf{fma}\left(1 + -2 \cdot t, {t}^{2}, \frac{1}{2}\right)} \]
        4. +-commutativeN/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{-2 \cdot t + 1}, {t}^{2}, \frac{1}{2}\right) \]
        5. lower-fma.f64N/A

          \[\leadsto \mathsf{fma}\left(\color{blue}{\mathsf{fma}\left(-2, t, 1\right)}, {t}^{2}, \frac{1}{2}\right) \]
        6. unpow2N/A

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, t, 1\right), \color{blue}{t \cdot t}, \frac{1}{2}\right) \]
        7. lower-*.f6499.9

          \[\leadsto \mathsf{fma}\left(\mathsf{fma}\left(-2, t, 1\right), \color{blue}{t \cdot t}, 0.5\right) \]
      7. Applied rewrites99.9%

        \[\leadsto \color{blue}{\mathsf{fma}\left(\mathsf{fma}\left(-2, t, 1\right), t \cdot t, 0.5\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification99.6%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\mathsf{fma}\left(-2, t, 1\right), t \cdot t, 0.5\right)\\ \end{array} \]
    5. Add Preprocessing

    Alternative 6: 98.7% accurate, 1.3× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t, t, 0.5\right)\\ \end{array} \end{array} \]
    (FPCore (t)
     :precision binary64
     (if (<= (/ (/ 2.0 t) (+ 1.0 (pow t -1.0))) 1e-11)
       (- 0.8333333333333334 (/ 0.2222222222222222 t))
       (fma t t 0.5)))
    double code(double t) {
    	double tmp;
    	if (((2.0 / t) / (1.0 + pow(t, -1.0))) <= 1e-11) {
    		tmp = 0.8333333333333334 - (0.2222222222222222 / t);
    	} else {
    		tmp = fma(t, t, 0.5);
    	}
    	return tmp;
    }
    
    function code(t)
    	tmp = 0.0
    	if (Float64(Float64(2.0 / t) / Float64(1.0 + (t ^ -1.0))) <= 1e-11)
    		tmp = Float64(0.8333333333333334 - Float64(0.2222222222222222 / t));
    	else
    		tmp = fma(t, t, 0.5);
    	end
    	return tmp
    end
    
    code[t_] := If[LessEqual[N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[Power[t, -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 1e-11], N[(0.8333333333333334 - N[(0.2222222222222222 / t), $MachinePrecision]), $MachinePrecision], N[(t * t + 0.5), $MachinePrecision]]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\
    \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\
    
    \mathbf{else}:\\
    \;\;\;\;\mathsf{fma}\left(t, t, 0.5\right)\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t))) < 9.99999999999999939e-12

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around inf

        \[\leadsto \color{blue}{\frac{5}{6} - \frac{2}{9} \cdot \frac{1}{t}} \]
      6. Step-by-step derivation
        1. lower--.f64N/A

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

          \[\leadsto \frac{5}{6} - \color{blue}{\frac{\frac{2}{9} \cdot 1}{t}} \]
        3. metadata-evalN/A

          \[\leadsto \frac{5}{6} - \frac{\color{blue}{\frac{2}{9}}}{t} \]
        4. lower-/.f6499.3

          \[\leadsto 0.8333333333333334 - \color{blue}{\frac{0.2222222222222222}{t}} \]
      7. Applied rewrites99.3%

        \[\leadsto \color{blue}{0.8333333333333334 - \frac{0.2222222222222222}{t}} \]

      if 9.99999999999999939e-12 < (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around 0

        \[\leadsto \color{blue}{\frac{1}{2} + {t}^{2}} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \color{blue}{{t}^{2} + \frac{1}{2}} \]
        2. unpow2N/A

          \[\leadsto \color{blue}{t \cdot t} + \frac{1}{2} \]
        3. lower-fma.f6499.7

          \[\leadsto \color{blue}{\mathsf{fma}\left(t, t, 0.5\right)} \]
      7. Applied rewrites99.7%

        \[\leadsto \color{blue}{\mathsf{fma}\left(t, t, 0.5\right)} \]
    3. Recombined 2 regimes into one program.
    4. Final simplification99.5%

      \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 10^{-11}:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t, t, 0.5\right)\\ \end{array} \]
    5. Add Preprocessing

    Alternative 7: 98.2% accurate, 1.3× speedup?

    \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;2 - \frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 5 \cdot 10^{-11}:\\ \;\;\;\;\mathsf{fma}\left(t, t, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;0.8333333333333334\\ \end{array} \end{array} \]
    (FPCore (t)
     :precision binary64
     (if (<= (- 2.0 (/ (/ 2.0 t) (+ 1.0 (pow t -1.0)))) 5e-11)
       (fma t t 0.5)
       0.8333333333333334))
    double code(double t) {
    	double tmp;
    	if ((2.0 - ((2.0 / t) / (1.0 + pow(t, -1.0)))) <= 5e-11) {
    		tmp = fma(t, t, 0.5);
    	} else {
    		tmp = 0.8333333333333334;
    	}
    	return tmp;
    }
    
    function code(t)
    	tmp = 0.0
    	if (Float64(2.0 - Float64(Float64(2.0 / t) / Float64(1.0 + (t ^ -1.0)))) <= 5e-11)
    		tmp = fma(t, t, 0.5);
    	else
    		tmp = 0.8333333333333334;
    	end
    	return tmp
    end
    
    code[t_] := If[LessEqual[N[(2.0 - N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[Power[t, -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 5e-11], N[(t * t + 0.5), $MachinePrecision], 0.8333333333333334]
    
    \begin{array}{l}
    
    \\
    \begin{array}{l}
    \mathbf{if}\;2 - \frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 5 \cdot 10^{-11}:\\
    \;\;\;\;\mathsf{fma}\left(t, t, 0.5\right)\\
    
    \mathbf{else}:\\
    \;\;\;\;0.8333333333333334\\
    
    
    \end{array}
    \end{array}
    
    Derivation
    1. Split input into 2 regimes
    2. if (-.f64 #s(literal 2 binary64) (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))) < 5.00000000000000018e-11

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around 0

        \[\leadsto \color{blue}{\frac{1}{2} + {t}^{2}} \]
      6. Step-by-step derivation
        1. +-commutativeN/A

          \[\leadsto \color{blue}{{t}^{2} + \frac{1}{2}} \]
        2. unpow2N/A

          \[\leadsto \color{blue}{t \cdot t} + \frac{1}{2} \]
        3. lower-fma.f6499.7

          \[\leadsto \color{blue}{\mathsf{fma}\left(t, t, 0.5\right)} \]
      7. Applied rewrites99.7%

        \[\leadsto \color{blue}{\mathsf{fma}\left(t, t, 0.5\right)} \]

      if 5.00000000000000018e-11 < (-.f64 #s(literal 2 binary64) (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t))))

      1. Initial program 100.0%

        \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      2. Add Preprocessing
      3. Step-by-step derivation
        1. lift-+.f64N/A

          \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. +-commutativeN/A

          \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        3. flip-+N/A

          \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. div-invN/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. lower-*.f64N/A

          \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      4. Applied rewrites100.0%

        \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
      5. Taylor expanded in t around inf

        \[\leadsto \color{blue}{\frac{5}{6}} \]
      6. Step-by-step derivation
        1. Applied rewrites98.2%

          \[\leadsto \color{blue}{0.8333333333333334} \]
      7. Recombined 2 regimes into one program.
      8. Final simplification99.0%

        \[\leadsto \begin{array}{l} \mathbf{if}\;2 - \frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 5 \cdot 10^{-11}:\\ \;\;\;\;\mathsf{fma}\left(t, t, 0.5\right)\\ \mathbf{else}:\\ \;\;\;\;0.8333333333333334\\ \end{array} \]
      9. Add Preprocessing

      Alternative 8: 98.6% accurate, 1.4× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;2 - \frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 1:\\ \;\;\;\;0.5\\ \mathbf{else}:\\ \;\;\;\;0.8333333333333334\\ \end{array} \end{array} \]
      (FPCore (t)
       :precision binary64
       (if (<= (- 2.0 (/ (/ 2.0 t) (+ 1.0 (pow t -1.0)))) 1.0)
         0.5
         0.8333333333333334))
      double code(double t) {
      	double tmp;
      	if ((2.0 - ((2.0 / t) / (1.0 + pow(t, -1.0)))) <= 1.0) {
      		tmp = 0.5;
      	} else {
      		tmp = 0.8333333333333334;
      	}
      	return tmp;
      }
      
      real(8) function code(t)
          real(8), intent (in) :: t
          real(8) :: tmp
          if ((2.0d0 - ((2.0d0 / t) / (1.0d0 + (t ** (-1.0d0))))) <= 1.0d0) then
              tmp = 0.5d0
          else
              tmp = 0.8333333333333334d0
          end if
          code = tmp
      end function
      
      public static double code(double t) {
      	double tmp;
      	if ((2.0 - ((2.0 / t) / (1.0 + Math.pow(t, -1.0)))) <= 1.0) {
      		tmp = 0.5;
      	} else {
      		tmp = 0.8333333333333334;
      	}
      	return tmp;
      }
      
      def code(t):
      	tmp = 0
      	if (2.0 - ((2.0 / t) / (1.0 + math.pow(t, -1.0)))) <= 1.0:
      		tmp = 0.5
      	else:
      		tmp = 0.8333333333333334
      	return tmp
      
      function code(t)
      	tmp = 0.0
      	if (Float64(2.0 - Float64(Float64(2.0 / t) / Float64(1.0 + (t ^ -1.0)))) <= 1.0)
      		tmp = 0.5;
      	else
      		tmp = 0.8333333333333334;
      	end
      	return tmp
      end
      
      function tmp_2 = code(t)
      	tmp = 0.0;
      	if ((2.0 - ((2.0 / t) / (1.0 + (t ^ -1.0)))) <= 1.0)
      		tmp = 0.5;
      	else
      		tmp = 0.8333333333333334;
      	end
      	tmp_2 = tmp;
      end
      
      code[t_] := If[LessEqual[N[(2.0 - N[(N[(2.0 / t), $MachinePrecision] / N[(1.0 + N[Power[t, -1.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], 1.0], 0.5, 0.8333333333333334]
      
      \begin{array}{l}
      
      \\
      \begin{array}{l}
      \mathbf{if}\;2 - \frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 1:\\
      \;\;\;\;0.5\\
      
      \mathbf{else}:\\
      \;\;\;\;0.8333333333333334\\
      
      
      \end{array}
      \end{array}
      
      Derivation
      1. Split input into 2 regimes
      2. if (-.f64 #s(literal 2 binary64) (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t)))) < 1

        1. Initial program 100.0%

          \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        2. Add Preprocessing
        3. Step-by-step derivation
          1. lift-+.f64N/A

            \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          2. +-commutativeN/A

            \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          3. flip-+N/A

            \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          4. div-invN/A

            \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          5. lower-*.f64N/A

            \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        4. Applied rewrites100.0%

          \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
        5. Taylor expanded in t around 0

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

            \[\leadsto \color{blue}{0.5} \]

          if 1 < (-.f64 #s(literal 2 binary64) (/.f64 (/.f64 #s(literal 2 binary64) t) (+.f64 #s(literal 1 binary64) (/.f64 #s(literal 1 binary64) t))))

          1. Initial program 100.0%

            \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-+.f64N/A

              \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
            2. +-commutativeN/A

              \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
            3. flip-+N/A

              \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
            4. div-invN/A

              \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
            5. lower-*.f64N/A

              \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          4. Applied rewrites100.0%

            \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          5. Taylor expanded in t around inf

            \[\leadsto \color{blue}{\frac{5}{6}} \]
          6. Step-by-step derivation
            1. Applied rewrites98.2%

              \[\leadsto \color{blue}{0.8333333333333334} \]
          7. Recombined 2 regimes into one program.
          8. Final simplification98.8%

            \[\leadsto \begin{array}{l} \mathbf{if}\;2 - \frac{\frac{2}{t}}{1 + {t}^{-1}} \leq 1:\\ \;\;\;\;0.5\\ \mathbf{else}:\\ \;\;\;\;0.8333333333333334\\ \end{array} \]
          9. Add Preprocessing

          Alternative 9: 59.8% accurate, 184.0× speedup?

          \[\begin{array}{l} \\ 0.5 \end{array} \]
          (FPCore (t) :precision binary64 0.5)
          double code(double t) {
          	return 0.5;
          }
          
          real(8) function code(t)
              real(8), intent (in) :: t
              code = 0.5d0
          end function
          
          public static double code(double t) {
          	return 0.5;
          }
          
          def code(t):
          	return 0.5
          
          function code(t)
          	return 0.5
          end
          
          function tmp = code(t)
          	tmp = 0.5;
          end
          
          code[t_] := 0.5
          
          \begin{array}{l}
          
          \\
          0.5
          \end{array}
          
          Derivation
          1. Initial program 100.0%

            \[\frac{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          2. Add Preprocessing
          3. Step-by-step derivation
            1. lift-+.f64N/A

              \[\leadsto \frac{\color{blue}{1 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
            2. +-commutativeN/A

              \[\leadsto \frac{\color{blue}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) + 1}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
            3. flip-+N/A

              \[\leadsto \frac{\color{blue}{\frac{\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
            4. div-invN/A

              \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
            5. lower-*.f64N/A

              \[\leadsto \frac{\color{blue}{\left(\left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) \cdot \left(\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)\right) - 1 \cdot 1\right) \cdot \frac{1}{\left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          4. Applied rewrites100.0%

            \[\leadsto \frac{\color{blue}{\left({\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{4} - 1\right) \cdot \frac{1}{{\left(2 - \frac{2}{\mathsf{fma}\left({t}^{-1}, t, t\right)}\right)}^{2} - 1}}}{2 + \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right) \cdot \left(2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\right)} \]
          5. Taylor expanded in t around 0

            \[\leadsto \color{blue}{\frac{1}{2}} \]
          6. Step-by-step derivation
            1. Applied rewrites58.6%

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

            Reproduce

            ?
            herbie shell --seed 2024317 
            (FPCore (t)
              :name "Kahan p13 Example 2"
              :precision binary64
              (/ (+ 1.0 (* (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))) (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))))) (+ 2.0 (* (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))) (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))))))))