Kahan p13 Example 3

Percentage Accurate: 99.8% → 99.9%
Time: 4.9s
Alternatives: 14
Speedup: 1.8×

Specification

?
\[\begin{array}{l} \\ \begin{array}{l} t_1 := 2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\\ 1 - \frac{1}{2 + t\_1 \cdot t\_1} \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (let* ((t_1 (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))))))
   (- 1.0 (/ 1.0 (+ 2.0 (* t_1 t_1))))))
float code(float t) {
	float t_1 = 2.0f - ((2.0f / t) / (1.0f + (1.0f / t)));
	return 1.0f - (1.0f / (2.0f + (t_1 * t_1)));
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: t_1
    t_1 = 2.0e0 - ((2.0e0 / t) / (1.0e0 + (1.0e0 / t)))
    code = 1.0e0 - (1.0e0 / (2.0e0 + (t_1 * t_1)))
end function

function code(t)
	t_1 = Float32(Float32(2.0) - Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))))
	return Float32(Float32(1.0) - Float32(Float32(1.0) / Float32(Float32(2.0) + Float32(t_1 * t_1))))
end

function tmp = code(t)
	t_1 = single(2.0) - ((single(2.0) / t) / (single(1.0) + (single(1.0) / t)));
	tmp = single(1.0) - (single(1.0) / (single(2.0) + (t_1 * t_1)));
end

\begin{array}{l}

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

Sampling outcomes in binary32 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 14 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.8% accurate, 1.0× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := 2 - \frac{\frac{2}{t}}{1 + \frac{1}{t}}\\ 1 - \frac{1}{2 + t\_1 \cdot t\_1} \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (let* ((t_1 (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))))))
   (- 1.0 (/ 1.0 (+ 2.0 (* t_1 t_1))))))
float code(float t) {
	float t_1 = 2.0f - ((2.0f / t) / (1.0f + (1.0f / t)));
	return 1.0f - (1.0f / (2.0f + (t_1 * t_1)));
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: t_1
    t_1 = 2.0e0 - ((2.0e0 / t) / (1.0e0 + (1.0e0 / t)))
    code = 1.0e0 - (1.0e0 / (2.0e0 + (t_1 * t_1)))
end function

function code(t)
	t_1 = Float32(Float32(2.0) - Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))))
	return Float32(Float32(1.0) - Float32(Float32(1.0) / Float32(Float32(2.0) + Float32(t_1 * t_1))))
end

function tmp = code(t)
	t_1 = single(2.0) - ((single(2.0) / t) / (single(1.0) + (single(1.0) / t)));
	tmp = single(1.0) - (single(1.0) / (single(2.0) + (t_1 * t_1)));
end

\begin{array}{l}

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

Alternative 1: 99.9% accurate, 1.8× speedup?

\[\begin{array}{l} \\ \begin{array}{l} t_1 := 2 + \frac{-2}{1 + t}\\ 1 - \frac{1}{t\_1 \cdot t\_1 + 2} \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (let* ((t_1 (+ 2.0 (/ -2.0 (+ 1.0 t))))) (- 1.0 (/ 1.0 (+ (* t_1 t_1) 2.0)))))
float code(float t) {
	float t_1 = 2.0f + (-2.0f / (1.0f + t));
	return 1.0f - (1.0f / ((t_1 * t_1) + 2.0f));
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: t_1
    t_1 = 2.0e0 + ((-2.0e0) / (1.0e0 + t))
    code = 1.0e0 - (1.0e0 / ((t_1 * t_1) + 2.0e0))
end function

function code(t)
	t_1 = Float32(Float32(2.0) + Float32(Float32(-2.0) / Float32(Float32(1.0) + t)))
	return Float32(Float32(1.0) - Float32(Float32(1.0) / Float32(Float32(t_1 * t_1) + Float32(2.0))))
end

function tmp = code(t)
	t_1 = single(2.0) + (single(-2.0) / (single(1.0) + t));
	tmp = single(1.0) - (single(1.0) / ((t_1 * t_1) + single(2.0)));
end

\begin{array}{l}

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

  1. Initial program 99.2%

    \[1 - \frac{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)} \]
  2. Add Preprocessing
  3. Step-by-step derivation

    1. lift-+.f32N/A

      \[\leadsto 1 - \frac{1}{\color{blue}{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 1 - \frac{1}{\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) + 2}} \]

    3. lower-+.f3299.2

      \[\leadsto 1 - \frac{1}{\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) + 2}} \]

  4. Applied rewrites99.9%

    \[\leadsto 1 - \color{blue}{\frac{1}{\left(2 + \frac{-2}{1 + t}\right) \cdot \left(2 + \frac{-2}{1 + t}\right) + 2}} \]
  5. Add Preprocessing

Alternative 2: 98.4% accurate, 1.1× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;1 - \left(\frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t} + 0.16666666666666666\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \frac{1}{2 + \left(\left(\left(\left(-16 \cdot t + 12\right) \cdot t - 8\right) \cdot t + 4\right) \cdot t\right) \cdot t}\\ \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (-
    1.0
    (+
     (/
      (-
       0.2222222222222222
       (/ (+ (/ 0.04938271604938271 t) 0.037037037037037035) t))
      t)
     0.16666666666666666))
   (-
    1.0
    (/
     1.0
     (+ 2.0 (* (* (+ (* (- (* (+ (* -16.0 t) 12.0) t) 8.0) t) 4.0) t) t))))))
float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 1.0f - (((0.2222222222222222f - (((0.04938271604938271f / t) + 0.037037037037037035f) / t)) / t) + 0.16666666666666666f);
	} else {
		tmp = 1.0f - (1.0f / (2.0f + ((((((((-16.0f * t) + 12.0f) * t) - 8.0f) * t) + 4.0f) * t) * t)));
	}
	return tmp;
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 1.0e0 - (((0.2222222222222222e0 - (((0.04938271604938271e0 / t) + 0.037037037037037035e0) / t)) / t) + 0.16666666666666666e0)
    else
        tmp = 1.0e0 - (1.0e0 / (2.0e0 + (((((((((-16.0e0) * t) + 12.0e0) * t) - 8.0e0) * t) + 4.0e0) * t) * t)))
    end if
    code = tmp
end function

function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(1.0) - Float32(Float32(Float32(Float32(0.2222222222222222) - Float32(Float32(Float32(Float32(0.04938271604938271) / t) + Float32(0.037037037037037035)) / t)) / t) + Float32(0.16666666666666666)));
	else
		tmp = Float32(Float32(1.0) - Float32(Float32(1.0) / Float32(Float32(2.0) + Float32(Float32(Float32(Float32(Float32(Float32(Float32(Float32(Float32(-16.0) * t) + Float32(12.0)) * t) - Float32(8.0)) * t) + Float32(4.0)) * t) * t))));
	end
	return tmp
end

function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(1.0) - (((single(0.2222222222222222) - (((single(0.04938271604938271) / t) + single(0.037037037037037035)) / t)) / t) + single(0.16666666666666666));
	else
		tmp = single(1.0) - (single(1.0) / (single(2.0) + ((((((((single(-16.0) * t) + single(12.0)) * t) - single(8.0)) * t) + single(4.0)) * t) * t)));
	end
	tmp_2 = tmp;
end

\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;1 - \left(\frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t} + 0.16666666666666666\right)\\

\mathbf{else}:\\
\;\;\;\;1 - \frac{1}{2 + \left(\left(\left(\left(-16 \cdot t + 12\right) \cdot t - 8\right) \cdot t + 4\right) \cdot t\right) \cdot t}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

    1. Initial program 99.8%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around inf

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

      1. +-commutativeN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\left(\frac{2}{9} \cdot \frac{1}{t} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{{t}^{2}}\right)}\right) \]

      2. unpow2N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\frac{2}{9} \cdot \frac{1}{t} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{\color{blue}{t \cdot t}}\right)\right) \]

      3. associate-/r*N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\frac{2}{9} \cdot \frac{1}{t} + -1 \cdot \color{blue}{\frac{\frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}}\right)\right) \]

      4. associate-/l*N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\frac{2}{9} \cdot \frac{1}{t} + \color{blue}{\frac{-1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}}\right)\right) \]

      5. associate-*r/N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\color{blue}{\frac{\frac{2}{9} \cdot 1}{t}} + \frac{-1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}\right)\right) \]

      6. metadata-evalN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\frac{\color{blue}{\frac{2}{9}}}{t} + \frac{-1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}\right)\right) \]

      7. div-addN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}}\right) \]

      8. *-rgt-identityN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t} \cdot 1}\right) \]

      9. metadata-evalN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t} \cdot \color{blue}{\left(-1 \cdot -1\right)}\right) \]

      10. associate-*l*N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\left(\frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t} \cdot -1\right) \cdot -1}\right) \]

      11. *-commutativeN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\left(-1 \cdot \frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}\right)} \cdot -1\right) \]

      12. mul-1-negN/A

        \[\leadsto 1 - \left(\frac{1}{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)} \cdot -1\right) \]

    5. Applied rewrites98.9%

      \[\leadsto 1 - \color{blue}{\left(\frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t} + 0.16666666666666666\right)} \]

    if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

    1. Initial program 98.5%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around 0

      \[\leadsto 1 - \frac{1}{2 + \color{blue}{{t}^{2} \cdot \left(4 + t \cdot \left(t \cdot \left(12 + -16 \cdot t\right) - 8\right)\right)}} \]
    4. Step-by-step derivation

      1. unpow2N/A

        \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(t \cdot t\right)} \cdot \left(4 + t \cdot \left(t \cdot \left(12 + -16 \cdot t\right) - 8\right)\right)} \]

      2. associate-*l*N/A

        \[\leadsto 1 - \frac{1}{2 + \color{blue}{t \cdot \left(t \cdot \left(4 + t \cdot \left(t \cdot \left(12 + -16 \cdot t\right) - 8\right)\right)\right)}} \]

      3. *-commutativeN/A

        \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(t \cdot \left(4 + t \cdot \left(t \cdot \left(12 + -16 \cdot t\right) - 8\right)\right)\right) \cdot t}} \]

      4. lower-*.f32N/A

        \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(t \cdot \left(4 + t \cdot \left(t \cdot \left(12 + -16 \cdot t\right) - 8\right)\right)\right) \cdot t}} \]

    5. Applied rewrites97.6%

      \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(\left(\left(\left(-16 \cdot t + 12\right) \cdot t - 8\right) \cdot t + 4\right) \cdot t\right) \cdot t}} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 3: 98.3% accurate, 1.1× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;1 - \left(\frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t} + 0.16666666666666666\right)\\ \mathbf{else}:\\ \;\;\;\;1 - \frac{1}{2 + \left(\left(\left(12 \cdot t - 8\right) \cdot t + 4\right) \cdot t\right) \cdot t}\\ \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (-
    1.0
    (+
     (/
      (-
       0.2222222222222222
       (/ (+ (/ 0.04938271604938271 t) 0.037037037037037035) t))
      t)
     0.16666666666666666))
   (- 1.0 (/ 1.0 (+ 2.0 (* (* (+ (* (- (* 12.0 t) 8.0) t) 4.0) t) t))))))
float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 1.0f - (((0.2222222222222222f - (((0.04938271604938271f / t) + 0.037037037037037035f) / t)) / t) + 0.16666666666666666f);
	} else {
		tmp = 1.0f - (1.0f / (2.0f + ((((((12.0f * t) - 8.0f) * t) + 4.0f) * t) * t)));
	}
	return tmp;
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 1.0e0 - (((0.2222222222222222e0 - (((0.04938271604938271e0 / t) + 0.037037037037037035e0) / t)) / t) + 0.16666666666666666e0)
    else
        tmp = 1.0e0 - (1.0e0 / (2.0e0 + ((((((12.0e0 * t) - 8.0e0) * t) + 4.0e0) * t) * t)))
    end if
    code = tmp
end function

function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(1.0) - Float32(Float32(Float32(Float32(0.2222222222222222) - Float32(Float32(Float32(Float32(0.04938271604938271) / t) + Float32(0.037037037037037035)) / t)) / t) + Float32(0.16666666666666666)));
	else
		tmp = Float32(Float32(1.0) - Float32(Float32(1.0) / Float32(Float32(2.0) + Float32(Float32(Float32(Float32(Float32(Float32(Float32(12.0) * t) - Float32(8.0)) * t) + Float32(4.0)) * t) * t))));
	end
	return tmp
end

function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(1.0) - (((single(0.2222222222222222) - (((single(0.04938271604938271) / t) + single(0.037037037037037035)) / t)) / t) + single(0.16666666666666666));
	else
		tmp = single(1.0) - (single(1.0) / (single(2.0) + ((((((single(12.0) * t) - single(8.0)) * t) + single(4.0)) * t) * t)));
	end
	tmp_2 = tmp;
end

\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;1 - \left(\frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t} + 0.16666666666666666\right)\\

\mathbf{else}:\\
\;\;\;\;1 - \frac{1}{2 + \left(\left(\left(12 \cdot t - 8\right) \cdot t + 4\right) \cdot t\right) \cdot t}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

    1. Initial program 99.8%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around inf

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

      1. +-commutativeN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\left(\frac{2}{9} \cdot \frac{1}{t} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{{t}^{2}}\right)}\right) \]

      2. unpow2N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\frac{2}{9} \cdot \frac{1}{t} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{\color{blue}{t \cdot t}}\right)\right) \]

      3. associate-/r*N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\frac{2}{9} \cdot \frac{1}{t} + -1 \cdot \color{blue}{\frac{\frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}}\right)\right) \]

      4. associate-/l*N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\frac{2}{9} \cdot \frac{1}{t} + \color{blue}{\frac{-1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}}\right)\right) \]

      5. associate-*r/N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\color{blue}{\frac{\frac{2}{9} \cdot 1}{t}} + \frac{-1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}\right)\right) \]

      6. metadata-evalN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \left(\frac{\color{blue}{\frac{2}{9}}}{t} + \frac{-1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}\right)\right) \]

      7. div-addN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}}\right) \]

      8. *-rgt-identityN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t} \cdot 1}\right) \]

      9. metadata-evalN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t} \cdot \color{blue}{\left(-1 \cdot -1\right)}\right) \]

      10. associate-*l*N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\left(\frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t} \cdot -1\right) \cdot -1}\right) \]

      11. *-commutativeN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\left(-1 \cdot \frac{\frac{2}{9} + -1 \cdot \frac{\frac{1}{27} + \frac{4}{81} \cdot \frac{1}{t}}{t}}{t}\right)} \cdot -1\right) \]

      12. mul-1-negN/A

        \[\leadsto 1 - \left(\frac{1}{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)} \cdot -1\right) \]

    5. Applied rewrites98.9%

      \[\leadsto 1 - \color{blue}{\left(\frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t} + 0.16666666666666666\right)} \]

    if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

    1. Initial program 98.5%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around 0

      \[\leadsto 1 - \frac{1}{2 + \color{blue}{{t}^{2} \cdot \left(4 + t \cdot \left(12 \cdot t - 8\right)\right)}} \]
    4. Step-by-step derivation

      1. *-commutativeN/A

        \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(4 + t \cdot \left(12 \cdot t - 8\right)\right) \cdot {t}^{2}}} \]

      2. unpow2N/A

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

      3. associate-*r*N/A

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

      4. lower-*.f32N/A

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

      5. lower-*.f32N/A

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

      6. +-commutativeN/A

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

      7. lower-+.f32N/A

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

      8. *-commutativeN/A

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

      9. lower-*.f32N/A

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

      10. lower--.f32N/A

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

      11. lower-*.f3297.2

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

    5. Applied rewrites97.2%

      \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(\left(\left(12 \cdot t - 8\right) \cdot t + 4\right) \cdot t\right) \cdot t}} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 4: 98.3% accurate, 1.2× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\ \mathbf{else}:\\ \;\;\;\;1 - \frac{1}{2 + \left(\left(\left(12 \cdot t - 8\right) \cdot t + 4\right) \cdot t\right) \cdot t}\\ \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (-
    0.8333333333333334
    (/
     (-
      0.2222222222222222
      (/ (+ (/ 0.04938271604938271 t) 0.037037037037037035) t))
     t))
   (- 1.0 (/ 1.0 (+ 2.0 (* (* (+ (* (- (* 12.0 t) 8.0) t) 4.0) t) t))))))
float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 0.8333333333333334f - ((0.2222222222222222f - (((0.04938271604938271f / t) + 0.037037037037037035f) / t)) / t);
	} else {
		tmp = 1.0f - (1.0f / (2.0f + ((((((12.0f * t) - 8.0f) * t) + 4.0f) * t) * t)));
	}
	return tmp;
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 0.8333333333333334e0 - ((0.2222222222222222e0 - (((0.04938271604938271e0 / t) + 0.037037037037037035e0) / t)) / t)
    else
        tmp = 1.0e0 - (1.0e0 / (2.0e0 + ((((((12.0e0 * t) - 8.0e0) * t) + 4.0e0) * t) * t)))
    end if
    code = tmp
end function

function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(0.8333333333333334) - Float32(Float32(Float32(0.2222222222222222) - Float32(Float32(Float32(Float32(0.04938271604938271) / t) + Float32(0.037037037037037035)) / t)) / t));
	else
		tmp = Float32(Float32(1.0) - Float32(Float32(1.0) / Float32(Float32(2.0) + Float32(Float32(Float32(Float32(Float32(Float32(Float32(12.0) * t) - Float32(8.0)) * t) + Float32(4.0)) * t) * t))));
	end
	return tmp
end

function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(0.8333333333333334) - ((single(0.2222222222222222) - (((single(0.04938271604938271) / t) + single(0.037037037037037035)) / t)) / t);
	else
		tmp = single(1.0) - (single(1.0) / (single(2.0) + ((((((single(12.0) * t) - single(8.0)) * t) + single(4.0)) * t) * t)));
	end
	tmp_2 = tmp;
end

\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\

\mathbf{else}:\\
\;\;\;\;1 - \frac{1}{2 + \left(\left(\left(12 \cdot t - 8\right) \cdot t + 4\right) \cdot t\right) \cdot t}\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

    1. Initial program 99.8%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around inf

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

    5. Applied rewrites98.9%

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

    if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

    1. Initial program 98.5%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around 0

      \[\leadsto 1 - \frac{1}{2 + \color{blue}{{t}^{2} \cdot \left(4 + t \cdot \left(12 \cdot t - 8\right)\right)}} \]
    4. Step-by-step derivation

      1. *-commutativeN/A

        \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(4 + t \cdot \left(12 \cdot t - 8\right)\right) \cdot {t}^{2}}} \]

      2. unpow2N/A

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

      3. associate-*r*N/A

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

      4. lower-*.f32N/A

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

      5. lower-*.f32N/A

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

      6. +-commutativeN/A

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

      7. lower-+.f32N/A

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

      8. *-commutativeN/A

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

      9. lower-*.f32N/A

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

      10. lower--.f32N/A

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

      11. lower-*.f3297.2

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

    5. Applied rewrites97.2%

      \[\leadsto 1 - \frac{1}{2 + \color{blue}{\left(\left(\left(12 \cdot t - 8\right) \cdot t + 4\right) \cdot t\right) \cdot t}} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 5: 98.2% accurate, 1.2× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\ \mathbf{else}:\\ \;\;\;\;0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t\\ \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (-
    0.8333333333333334
    (/
     (-
      0.2222222222222222
      (/ (+ (/ 0.04938271604938271 t) 0.037037037037037035) t))
     t))
   (- 0.5 (* (* (- -1.0 (* (- t 2.0) t)) t) t))))
float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 0.8333333333333334f - ((0.2222222222222222f - (((0.04938271604938271f / t) + 0.037037037037037035f) / t)) / t);
	} else {
		tmp = 0.5f - (((-1.0f - ((t - 2.0f) * t)) * t) * t);
	}
	return tmp;
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 0.8333333333333334e0 - ((0.2222222222222222e0 - (((0.04938271604938271e0 / t) + 0.037037037037037035e0) / t)) / t)
    else
        tmp = 0.5e0 - ((((-1.0e0) - ((t - 2.0e0) * t)) * t) * t)
    end if
    code = tmp
end function

function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(0.8333333333333334) - Float32(Float32(Float32(0.2222222222222222) - Float32(Float32(Float32(Float32(0.04938271604938271) / t) + Float32(0.037037037037037035)) / t)) / t));
	else
		tmp = Float32(Float32(0.5) - Float32(Float32(Float32(Float32(-1.0) - Float32(Float32(t - Float32(2.0)) * t)) * t) * t));
	end
	return tmp
end

function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(0.8333333333333334) - ((single(0.2222222222222222) - (((single(0.04938271604938271) / t) + single(0.037037037037037035)) / t)) / t);
	else
		tmp = single(0.5) - (((single(-1.0) - ((t - single(2.0)) * t)) * t) * t);
	end
	tmp_2 = tmp;
end

\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\

\mathbf{else}:\\
\;\;\;\;0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

    1. Initial program 99.8%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around inf

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

    5. Applied rewrites98.9%

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

    if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

    1. Initial program 98.5%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around 0

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

      1. fp-cancel-sign-sub-invN/A

        \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]

      2. lower--.f32N/A

        \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]

      3. distribute-lft-neg-outN/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left({t}^{2} \cdot \left(1 + t \cdot \left(t - 2\right)\right)\right)\right)} \]

      4. *-commutativeN/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(1 + t \cdot \left(t - 2\right)\right) \cdot {t}^{2}}\right)\right) \]

      5. unpow2N/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot \color{blue}{\left(t \cdot t\right)}\right)\right) \]

      6. associate-*r*N/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right) \cdot t}\right)\right) \]

      7. distribute-lft-neg-inN/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right)\right) \cdot t} \]

      8. lower-*.f32N/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right)\right) \cdot t} \]

    5. Applied rewrites97.1%

      \[\leadsto \color{blue}{0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 6: 98.0% accurate, 1.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;1 - \left(0.16666666666666666 - \frac{\frac{0.037037037037037035}{t} - 0.2222222222222222}{t}\right)\\ \mathbf{else}:\\ \;\;\;\;0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t\\ \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (-
    1.0
    (-
     0.16666666666666666
     (/ (- (/ 0.037037037037037035 t) 0.2222222222222222) t)))
   (- 0.5 (* (* (- -1.0 (* (- t 2.0) t)) t) t))))
float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 1.0f - (0.16666666666666666f - (((0.037037037037037035f / t) - 0.2222222222222222f) / t));
	} else {
		tmp = 0.5f - (((-1.0f - ((t - 2.0f) * t)) * t) * t);
	}
	return tmp;
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 1.0e0 - (0.16666666666666666e0 - (((0.037037037037037035e0 / t) - 0.2222222222222222e0) / t))
    else
        tmp = 0.5e0 - ((((-1.0e0) - ((t - 2.0e0) * t)) * t) * t)
    end if
    code = tmp
end function

function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(1.0) - Float32(Float32(0.16666666666666666) - Float32(Float32(Float32(Float32(0.037037037037037035) / t) - Float32(0.2222222222222222)) / t)));
	else
		tmp = Float32(Float32(0.5) - Float32(Float32(Float32(Float32(-1.0) - Float32(Float32(t - Float32(2.0)) * t)) * t) * t));
	end
	return tmp
end

function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(1.0) - (single(0.16666666666666666) - (((single(0.037037037037037035) / t) - single(0.2222222222222222)) / t));
	else
		tmp = single(0.5) - (((single(-1.0) - ((t - single(2.0)) * t)) * t) * t);
	end
	tmp_2 = tmp;
end

\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;1 - \left(0.16666666666666666 - \frac{\frac{0.037037037037037035}{t} - 0.2222222222222222}{t}\right)\\

\mathbf{else}:\\
\;\;\;\;0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

    1. Initial program 99.8%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around inf

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

      1. fp-cancel-sign-sub-invN/A

        \[\leadsto 1 - \left(\color{blue}{\left(\frac{1}{6} - \left(\mathsf{neg}\left(\frac{2}{9}\right)\right) \cdot \frac{1}{t}\right)} - \frac{\frac{1}{27}}{{t}^{2}}\right) \]

      2. associate--l-N/A

        \[\leadsto 1 - \color{blue}{\left(\frac{1}{6} - \left(\left(\mathsf{neg}\left(\frac{2}{9}\right)\right) \cdot \frac{1}{t} + \frac{\frac{1}{27}}{{t}^{2}}\right)\right)} \]

      3. +-commutativeN/A

        \[\leadsto 1 - \left(\frac{1}{6} - \color{blue}{\left(\frac{\frac{1}{27}}{{t}^{2}} + \left(\mathsf{neg}\left(\frac{2}{9}\right)\right) \cdot \frac{1}{t}\right)}\right) \]

      4. unpow2N/A

        \[\leadsto 1 - \left(\frac{1}{6} - \left(\frac{\frac{1}{27}}{\color{blue}{t \cdot t}} + \left(\mathsf{neg}\left(\frac{2}{9}\right)\right) \cdot \frac{1}{t}\right)\right) \]

      5. associate-/r*N/A

        \[\leadsto 1 - \left(\frac{1}{6} - \left(\color{blue}{\frac{\frac{\frac{1}{27}}{t}}{t}} + \left(\mathsf{neg}\left(\frac{2}{9}\right)\right) \cdot \frac{1}{t}\right)\right) \]

      6. metadata-evalN/A

        \[\leadsto 1 - \left(\frac{1}{6} - \left(\frac{\frac{\color{blue}{\frac{1}{27} \cdot 1}}{t}}{t} + \left(\mathsf{neg}\left(\frac{2}{9}\right)\right) \cdot \frac{1}{t}\right)\right) \]

      7. associate-*r/N/A

        \[\leadsto 1 - \left(\frac{1}{6} - \left(\frac{\color{blue}{\frac{1}{27} \cdot \frac{1}{t}}}{t} + \left(\mathsf{neg}\left(\frac{2}{9}\right)\right) \cdot \frac{1}{t}\right)\right) \]

      8. fp-cancel-sub-sign-invN/A

        \[\leadsto 1 - \left(\frac{1}{6} - \color{blue}{\left(\frac{\frac{1}{27} \cdot \frac{1}{t}}{t} - \frac{2}{9} \cdot \frac{1}{t}\right)}\right) \]

      9. associate-*r/N/A

        \[\leadsto 1 - \left(\frac{1}{6} - \left(\frac{\frac{1}{27} \cdot \frac{1}{t}}{t} - \color{blue}{\frac{\frac{2}{9} \cdot 1}{t}}\right)\right) \]

      10. metadata-evalN/A

        \[\leadsto 1 - \left(\frac{1}{6} - \left(\frac{\frac{1}{27} \cdot \frac{1}{t}}{t} - \frac{\color{blue}{\frac{2}{9}}}{t}\right)\right) \]

      11. div-subN/A

        \[\leadsto 1 - \left(\frac{1}{6} - \color{blue}{\frac{\frac{1}{27} \cdot \frac{1}{t} - \frac{2}{9}}{t}}\right) \]

      12. lower--.f32N/A

        \[\leadsto 1 - \color{blue}{\left(\frac{1}{6} - \frac{\frac{1}{27} \cdot \frac{1}{t} - \frac{2}{9}}{t}\right)} \]

      13. lower-/.f32N/A

        \[\leadsto 1 - \left(\frac{1}{6} - \color{blue}{\frac{\frac{1}{27} \cdot \frac{1}{t} - \frac{2}{9}}{t}}\right) \]

      14. lower--.f32N/A

        \[\leadsto 1 - \left(\frac{1}{6} - \frac{\color{blue}{\frac{1}{27} \cdot \frac{1}{t} - \frac{2}{9}}}{t}\right) \]

      15. associate-*r/N/A

        \[\leadsto 1 - \left(\frac{1}{6} - \frac{\color{blue}{\frac{\frac{1}{27} \cdot 1}{t}} - \frac{2}{9}}{t}\right) \]

      16. metadata-evalN/A

        \[\leadsto 1 - \left(\frac{1}{6} - \frac{\frac{\color{blue}{\frac{1}{27}}}{t} - \frac{2}{9}}{t}\right) \]

      17. lower-/.f3298.3

        \[\leadsto 1 - \left(0.16666666666666666 - \frac{\color{blue}{\frac{0.037037037037037035}{t}} - 0.2222222222222222}{t}\right) \]

    5. Applied rewrites98.3%

      \[\leadsto 1 - \color{blue}{\left(0.16666666666666666 - \frac{\frac{0.037037037037037035}{t} - 0.2222222222222222}{t}\right)} \]

    if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

    1. Initial program 98.5%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around 0

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

      1. fp-cancel-sign-sub-invN/A

        \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]

      2. lower--.f32N/A

        \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]

      3. distribute-lft-neg-outN/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left({t}^{2} \cdot \left(1 + t \cdot \left(t - 2\right)\right)\right)\right)} \]

      4. *-commutativeN/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(1 + t \cdot \left(t - 2\right)\right) \cdot {t}^{2}}\right)\right) \]

      5. unpow2N/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot \color{blue}{\left(t \cdot t\right)}\right)\right) \]

      6. associate-*r*N/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right) \cdot t}\right)\right) \]

      7. distribute-lft-neg-inN/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right)\right) \cdot t} \]

      8. lower-*.f32N/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right)\right) \cdot t} \]

    5. Applied rewrites97.1%

      \[\leadsto \color{blue}{0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 7: 98.0% accurate, 1.4× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{0.037037037037037035}{t}}{t}\\ \mathbf{else}:\\ \;\;\;\;0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t\\ \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (-
    0.8333333333333334
    (/ (- 0.2222222222222222 (/ 0.037037037037037035 t)) t))
   (- 0.5 (* (* (- -1.0 (* (- t 2.0) t)) t) t))))
float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 0.8333333333333334f - ((0.2222222222222222f - (0.037037037037037035f / t)) / t);
	} else {
		tmp = 0.5f - (((-1.0f - ((t - 2.0f) * t)) * t) * t);
	}
	return tmp;
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 0.8333333333333334e0 - ((0.2222222222222222e0 - (0.037037037037037035e0 / t)) / t)
    else
        tmp = 0.5e0 - ((((-1.0e0) - ((t - 2.0e0) * t)) * t) * t)
    end if
    code = tmp
end function

function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(0.8333333333333334) - Float32(Float32(Float32(0.2222222222222222) - Float32(Float32(0.037037037037037035) / t)) / t));
	else
		tmp = Float32(Float32(0.5) - Float32(Float32(Float32(Float32(-1.0) - Float32(Float32(t - Float32(2.0)) * t)) * t) * t));
	end
	return tmp
end

function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(0.8333333333333334) - ((single(0.2222222222222222) - (single(0.037037037037037035) / t)) / t);
	else
		tmp = single(0.5) - (((single(-1.0) - ((t - single(2.0)) * t)) * t) * t);
	end
	tmp_2 = tmp;
end

\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;0.8333333333333334 - \frac{0.2222222222222222 - \frac{0.037037037037037035}{t}}{t}\\

\mathbf{else}:\\
\;\;\;\;0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

    1. Initial program 99.8%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. 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}} \]

    5. Applied rewrites98.3%

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

    if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

    1. Initial program 98.5%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around 0

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

      1. fp-cancel-sign-sub-invN/A

        \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]

      2. lower--.f32N/A

        \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]

      3. distribute-lft-neg-outN/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left({t}^{2} \cdot \left(1 + t \cdot \left(t - 2\right)\right)\right)\right)} \]

      4. *-commutativeN/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(1 + t \cdot \left(t - 2\right)\right) \cdot {t}^{2}}\right)\right) \]

      5. unpow2N/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot \color{blue}{\left(t \cdot t\right)}\right)\right) \]

      6. associate-*r*N/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right) \cdot t}\right)\right) \]

      7. distribute-lft-neg-inN/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right)\right) \cdot t} \]

      8. lower-*.f32N/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right)\right) \cdot t} \]

    5. Applied rewrites97.1%

      \[\leadsto \color{blue}{0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 8: 97.7% accurate, 1.5× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;1 - \left(0.16666666666666666 + \frac{0.2222222222222222}{t}\right)\\ \mathbf{else}:\\ \;\;\;\;0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t\\ \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (- 1.0 (+ 0.16666666666666666 (/ 0.2222222222222222 t)))
   (- 0.5 (* (* (- -1.0 (* (- t 2.0) t)) t) t))))
float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 1.0f - (0.16666666666666666f + (0.2222222222222222f / t));
	} else {
		tmp = 0.5f - (((-1.0f - ((t - 2.0f) * t)) * t) * t);
	}
	return tmp;
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 1.0e0 - (0.16666666666666666e0 + (0.2222222222222222e0 / t))
    else
        tmp = 0.5e0 - ((((-1.0e0) - ((t - 2.0e0) * t)) * t) * t)
    end if
    code = tmp
end function

function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(1.0) - Float32(Float32(0.16666666666666666) + Float32(Float32(0.2222222222222222) / t)));
	else
		tmp = Float32(Float32(0.5) - Float32(Float32(Float32(Float32(-1.0) - Float32(Float32(t - Float32(2.0)) * t)) * t) * t));
	end
	return tmp
end

function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(1.0) - (single(0.16666666666666666) + (single(0.2222222222222222) / t));
	else
		tmp = single(0.5) - (((single(-1.0) - ((t - single(2.0)) * t)) * t) * t);
	end
	tmp_2 = tmp;
end

\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;1 - \left(0.16666666666666666 + \frac{0.2222222222222222}{t}\right)\\

\mathbf{else}:\\
\;\;\;\;0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

    1. Initial program 99.8%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around inf

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

      1. lower-+.f32N/A

        \[\leadsto 1 - \color{blue}{\left(\frac{1}{6} + \frac{2}{9} \cdot \frac{1}{t}\right)} \]

      2. associate-*r/N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\frac{\frac{2}{9} \cdot 1}{t}}\right) \]

      3. metadata-evalN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \frac{\color{blue}{\frac{2}{9}}}{t}\right) \]

      4. lower-/.f3297.5

        \[\leadsto 1 - \left(0.16666666666666666 + \color{blue}{\frac{0.2222222222222222}{t}}\right) \]

    5. Applied rewrites97.5%

      \[\leadsto 1 - \color{blue}{\left(0.16666666666666666 + \frac{0.2222222222222222}{t}\right)} \]

    if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

    1. Initial program 98.5%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around 0

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

      1. fp-cancel-sign-sub-invN/A

        \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]

      2. lower--.f32N/A

        \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + t \cdot \left(t - 2\right)\right)} \]

      3. distribute-lft-neg-outN/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left({t}^{2} \cdot \left(1 + t \cdot \left(t - 2\right)\right)\right)\right)} \]

      4. *-commutativeN/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(1 + t \cdot \left(t - 2\right)\right) \cdot {t}^{2}}\right)\right) \]

      5. unpow2N/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot \color{blue}{\left(t \cdot t\right)}\right)\right) \]

      6. associate-*r*N/A

        \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right) \cdot t}\right)\right) \]

      7. distribute-lft-neg-inN/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right)\right) \cdot t} \]

      8. lower-*.f32N/A

        \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + t \cdot \left(t - 2\right)\right) \cdot t\right)\right) \cdot t} \]

    5. Applied rewrites97.1%

      \[\leadsto \color{blue}{0.5 - \left(\left(-1 - \left(t - 2\right) \cdot t\right) \cdot t\right) \cdot t} \]
  3. Recombined 2 regimes into one program.
  4. Add Preprocessing

Alternative 9: 97.5% accurate, 1.6× speedup?

\[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;1 - \left(0.16666666666666666 + \frac{0.2222222222222222}{t}\right)\\ \mathbf{else}:\\ \;\;\;\;0.5 - \left(\left(t + t\right) + -1\right) \cdot \left(t \cdot t\right)\\ \end{array} \end{array} \]
(FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (- 1.0 (+ 0.16666666666666666 (/ 0.2222222222222222 t)))
   (- 0.5 (* (+ (+ t t) -1.0) (* t t)))))
float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 1.0f - (0.16666666666666666f + (0.2222222222222222f / t));
	} else {
		tmp = 0.5f - (((t + t) + -1.0f) * (t * t));
	}
	return tmp;
}

real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 1.0e0 - (0.16666666666666666e0 + (0.2222222222222222e0 / t))
    else
        tmp = 0.5e0 - (((t + t) + (-1.0e0)) * (t * t))
    end if
    code = tmp
end function

function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(1.0) - Float32(Float32(0.16666666666666666) + Float32(Float32(0.2222222222222222) / t)));
	else
		tmp = Float32(Float32(0.5) - Float32(Float32(Float32(t + t) + Float32(-1.0)) * Float32(t * t)));
	end
	return tmp
end

function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(1.0) - (single(0.16666666666666666) + (single(0.2222222222222222) / t));
	else
		tmp = single(0.5) - (((t + t) + single(-1.0)) * (t * t));
	end
	tmp_2 = tmp;
end

\begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;1 - \left(0.16666666666666666 + \frac{0.2222222222222222}{t}\right)\\

\mathbf{else}:\\
\;\;\;\;0.5 - \left(\left(t + t\right) + -1\right) \cdot \left(t \cdot t\right)\\


\end{array}
\end{array}
Derivation
  1. Split input into 2 regimes

  2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

    1. Initial program 99.8%

      \[1 - \frac{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)} \]
    2. Add Preprocessing

    3. Taylor expanded in t around inf

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

      1. lower-+.f32N/A

        \[\leadsto 1 - \color{blue}{\left(\frac{1}{6} + \frac{2}{9} \cdot \frac{1}{t}\right)} \]

      2. associate-*r/N/A

        \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\frac{\frac{2}{9} \cdot 1}{t}}\right) \]

      3. metadata-evalN/A

        \[\leadsto 1 - \left(\frac{1}{6} + \frac{\color{blue}{\frac{2}{9}}}{t}\right) \]

      4. lower-/.f3297.5

        \[\leadsto 1 - \left(0.16666666666666666 + \color{blue}{\frac{0.2222222222222222}{t}}\right) \]

    5. Applied rewrites97.5%

      \[\leadsto 1 - \color{blue}{\left(0.16666666666666666 + \frac{0.2222222222222222}{t}\right)} \]

    if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

    1. Initial program 98.5%

      \[1 - \frac{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)} \]
    2. Add Preprocessing
    3. Step-by-step derivation

      1. lift-+.f32N/A

        \[\leadsto 1 - \frac{1}{\color{blue}{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 1 - \frac{1}{\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) + 2}} \]

      3. lower-+.f3298.5

        \[\leadsto 1 - \frac{1}{\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) + 2}} \]

    4. Applied rewrites99.9%

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

    5. Taylor expanded in t around inf

      \[\leadsto \color{blue}{\frac{5}{6}} \]
    6. Step-by-step derivation

      1. Applied rewrites30.0%

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

      2. Taylor expanded in t around 0

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

        1. fp-cancel-sign-sub-invN/A

          \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + -2 \cdot t\right)} \]

        2. lower--.f32N/A

          \[\leadsto \color{blue}{\frac{1}{2} - \left(\mathsf{neg}\left({t}^{2}\right)\right) \cdot \left(1 + -2 \cdot t\right)} \]

        3. distribute-lft-neg-outN/A

          \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left({t}^{2} \cdot \left(1 + -2 \cdot t\right)\right)\right)} \]

        4. *-commutativeN/A

          \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(1 + -2 \cdot t\right) \cdot {t}^{2}}\right)\right) \]

        5. distribute-lft-neg-inN/A

          \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + -2 \cdot t\right)\right)\right) \cdot {t}^{2}} \]

        6. lower-*.f32N/A

          \[\leadsto \frac{1}{2} - \color{blue}{\left(\mathsf{neg}\left(\left(1 + -2 \cdot t\right)\right)\right) \cdot {t}^{2}} \]

        7. +-commutativeN/A

          \[\leadsto \frac{1}{2} - \left(\mathsf{neg}\left(\color{blue}{\left(-2 \cdot t + 1\right)}\right)\right) \cdot {t}^{2} \]

        8. distribute-neg-inN/A

          \[\leadsto \frac{1}{2} - \color{blue}{\left(\left(\mathsf{neg}\left(-2 \cdot t\right)\right) + \left(\mathsf{neg}\left(1\right)\right)\right)} \cdot {t}^{2} \]

        9. distribute-lft-neg-inN/A

          \[\leadsto \frac{1}{2} - \left(\color{blue}{\left(\mathsf{neg}\left(-2\right)\right) \cdot t} + \left(\mathsf{neg}\left(1\right)\right)\right) \cdot {t}^{2} \]

        10. metadata-evalN/A

          \[\leadsto \frac{1}{2} - \left(\color{blue}{2} \cdot t + \left(\mathsf{neg}\left(1\right)\right)\right) \cdot {t}^{2} \]

        11. metadata-evalN/A

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

        12. lower-+.f32N/A

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

        13. lower-*.f32N/A

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

        14. unpow2N/A

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

        15. lower-*.f3297.1

          \[\leadsto 0.5 - \left(2 \cdot t + -1\right) \cdot \color{blue}{\left(t \cdot t\right)} \]

      4. Applied rewrites97.1%

        \[\leadsto \color{blue}{0.5 - \left(2 \cdot t + -1\right) \cdot \left(t \cdot t\right)} \]
      5. Step-by-step derivation

        1. Applied rewrites97.1%

          \[\leadsto 0.5 - \left(\left(t + t\right) + -1\right) \cdot \left(t \cdot t\right) \]
      6. Recombined 2 regimes into one program.
      7. Add Preprocessing

      Alternative 10: 97.2% accurate, 1.7× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;1 - \left(0.16666666666666666 + \frac{0.2222222222222222}{t}\right)\\ \mathbf{else}:\\ \;\;\;\;t \cdot t + 0.5\\ \end{array} \end{array} \]
      (FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (- 1.0 (+ 0.16666666666666666 (/ 0.2222222222222222 t)))
   (+ (* t t) 0.5)))
      float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 1.0f - (0.16666666666666666f + (0.2222222222222222f / t));
	} else {
		tmp = (t * t) + 0.5f;
	}
	return tmp;
}

      real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 1.0e0 - (0.16666666666666666e0 + (0.2222222222222222e0 / t))
    else
        tmp = (t * t) + 0.5e0
    end if
    code = tmp
end function

      function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(1.0) - Float32(Float32(0.16666666666666666) + Float32(Float32(0.2222222222222222) / t)));
	else
		tmp = Float32(Float32(t * t) + Float32(0.5));
	end
	return tmp
end

      function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(1.0) - (single(0.16666666666666666) + (single(0.2222222222222222) / t));
	else
		tmp = (t * t) + single(0.5);
	end
	tmp_2 = tmp;
end

      \begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;1 - \left(0.16666666666666666 + \frac{0.2222222222222222}{t}\right)\\

\mathbf{else}:\\
\;\;\;\;t \cdot t + 0.5\\


\end{array}
\end{array}
      Derivation
      1. Split input into 2 regimes

      2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

        1. Initial program 99.8%

          \[1 - \frac{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)} \]
        2. Add Preprocessing

        3. Taylor expanded in t around inf

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

          1. lower-+.f32N/A

            \[\leadsto 1 - \color{blue}{\left(\frac{1}{6} + \frac{2}{9} \cdot \frac{1}{t}\right)} \]

          2. associate-*r/N/A

            \[\leadsto 1 - \left(\frac{1}{6} + \color{blue}{\frac{\frac{2}{9} \cdot 1}{t}}\right) \]

          3. metadata-evalN/A

            \[\leadsto 1 - \left(\frac{1}{6} + \frac{\color{blue}{\frac{2}{9}}}{t}\right) \]

          4. lower-/.f3297.5

            \[\leadsto 1 - \left(0.16666666666666666 + \color{blue}{\frac{0.2222222222222222}{t}}\right) \]

        5. Applied rewrites97.5%

          \[\leadsto 1 - \color{blue}{\left(0.16666666666666666 + \frac{0.2222222222222222}{t}\right)} \]

        if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

        1. Initial program 98.5%

          \[1 - \frac{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)} \]
        2. Add Preprocessing

        3. Taylor expanded in t around 0

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

          1. +-commutativeN/A

            \[\leadsto \color{blue}{{t}^{2} + \frac{1}{2}} \]

          2. lower-+.f32N/A

            \[\leadsto \color{blue}{{t}^{2} + \frac{1}{2}} \]

          3. unpow2N/A

            \[\leadsto \color{blue}{t \cdot t} + \frac{1}{2} \]

          4. lower-*.f3295.7

            \[\leadsto \color{blue}{t \cdot t} + 0.5 \]

        5. Applied rewrites95.7%

          \[\leadsto \color{blue}{t \cdot t + 0.5} \]
      3. Recombined 2 regimes into one program.
      4. Add Preprocessing

      Alternative 11: 97.2% accurate, 1.8× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\ \mathbf{else}:\\ \;\;\;\;t \cdot t + 0.5\\ \end{array} \end{array} \]
      (FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   (- 0.8333333333333334 (/ 0.2222222222222222 t))
   (+ (* t t) 0.5)))
      float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 0.8333333333333334f - (0.2222222222222222f / t);
	} else {
		tmp = (t * t) + 0.5f;
	}
	return tmp;
}

      real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 0.8333333333333334e0 - (0.2222222222222222e0 / t)
    else
        tmp = (t * t) + 0.5e0
    end if
    code = tmp
end function

      function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(Float32(0.8333333333333334) - Float32(Float32(0.2222222222222222) / t));
	else
		tmp = Float32(Float32(t * t) + Float32(0.5));
	end
	return tmp
end

      function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(0.8333333333333334) - (single(0.2222222222222222) / t);
	else
		tmp = (t * t) + single(0.5);
	end
	tmp_2 = tmp;
end

      \begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;0.8333333333333334 - \frac{0.2222222222222222}{t}\\

\mathbf{else}:\\
\;\;\;\;t \cdot t + 0.5\\


\end{array}
\end{array}
      Derivation
      1. Split input into 2 regimes

      2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

        1. Initial program 99.8%

          \[1 - \frac{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)} \]
        2. Add Preprocessing

        3. Taylor expanded in t around inf

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

          1. lower--.f32N/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-/.f3297.4

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

        5. Applied rewrites97.4%

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

        if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

        1. Initial program 98.5%

          \[1 - \frac{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)} \]
        2. Add Preprocessing

        3. Taylor expanded in t around 0

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

          1. +-commutativeN/A

            \[\leadsto \color{blue}{{t}^{2} + \frac{1}{2}} \]

          2. lower-+.f32N/A

            \[\leadsto \color{blue}{{t}^{2} + \frac{1}{2}} \]

          3. unpow2N/A

            \[\leadsto \color{blue}{t \cdot t} + \frac{1}{2} \]

          4. lower-*.f3295.7

            \[\leadsto \color{blue}{t \cdot t} + 0.5 \]

        5. Applied rewrites95.7%

          \[\leadsto \color{blue}{t \cdot t + 0.5} \]
      3. Recombined 2 regimes into one program.
      4. Add Preprocessing

      Alternative 12: 95.3% accurate, 2.0× speedup?

      \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;0.8333333333333334\\ \mathbf{else}:\\ \;\;\;\;t \cdot t + 0.5\\ \end{array} \end{array} \]
      (FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5)
   0.8333333333333334
   (+ (* t t) 0.5)))
      float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 0.8333333333333334f;
	} else {
		tmp = (t * t) + 0.5f;
	}
	return tmp;
}

      real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 0.8333333333333334e0
    else
        tmp = (t * t) + 0.5e0
    end if
    code = tmp
end function

      function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(0.8333333333333334);
	else
		tmp = Float32(Float32(t * t) + Float32(0.5));
	end
	return tmp
end

      function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(0.8333333333333334);
	else
		tmp = (t * t) + single(0.5);
	end
	tmp_2 = tmp;
end

      \begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;0.8333333333333334\\

\mathbf{else}:\\
\;\;\;\;t \cdot t + 0.5\\


\end{array}
\end{array}
      Derivation
      1. Split input into 2 regimes

      2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

        1. Initial program 99.8%

          \[1 - \frac{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)} \]
        2. Add Preprocessing

        3. Taylor expanded in t around inf

          \[\leadsto \color{blue}{\frac{5}{6}} \]
        4. Step-by-step derivation

          1. Applied rewrites94.1%

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

          if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

          1. Initial program 98.5%

            \[1 - \frac{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)} \]
          2. Add Preprocessing

          3. Taylor expanded in t around 0

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

            1. +-commutativeN/A

              \[\leadsto \color{blue}{{t}^{2} + \frac{1}{2}} \]

            2. lower-+.f32N/A

              \[\leadsto \color{blue}{{t}^{2} + \frac{1}{2}} \]

            3. unpow2N/A

              \[\leadsto \color{blue}{t \cdot t} + \frac{1}{2} \]

            4. lower-*.f3295.7

              \[\leadsto \color{blue}{t \cdot t} + 0.5 \]

          5. Applied rewrites95.7%

            \[\leadsto \color{blue}{t \cdot t + 0.5} \]
        5. Recombined 2 regimes into one program.
        6. Add Preprocessing

        Alternative 13: 94.8% accurate, 2.3× speedup?

        \[\begin{array}{l} \\ \begin{array}{l} \mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\ \;\;\;\;0.8333333333333334\\ \mathbf{else}:\\ \;\;\;\;0.5\\ \end{array} \end{array} \]
        (FPCore (t)
 :precision binary32
 (if (<= (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t))) 0.5) 0.8333333333333334 0.5))
        float code(float t) {
	float tmp;
	if (((2.0f / t) / (1.0f + (1.0f / t))) <= 0.5f) {
		tmp = 0.8333333333333334f;
	} else {
		tmp = 0.5f;
	}
	return tmp;
}

        real(4) function code(t)
    real(4), intent (in) :: t
    real(4) :: tmp
    if (((2.0e0 / t) / (1.0e0 + (1.0e0 / t))) <= 0.5e0) then
        tmp = 0.8333333333333334e0
    else
        tmp = 0.5e0
    end if
    code = tmp
end function

        function code(t)
	tmp = Float32(0.0)
	if (Float32(Float32(Float32(2.0) / t) / Float32(Float32(1.0) + Float32(Float32(1.0) / t))) <= Float32(0.5))
		tmp = Float32(0.8333333333333334);
	else
		tmp = Float32(0.5);
	end
	return tmp
end

        function tmp_2 = code(t)
	tmp = single(0.0);
	if (((single(2.0) / t) / (single(1.0) + (single(1.0) / t))) <= single(0.5))
		tmp = single(0.8333333333333334);
	else
		tmp = single(0.5);
	end
	tmp_2 = tmp;
end

        \begin{array}{l}

\\
\begin{array}{l}
\mathbf{if}\;\frac{\frac{2}{t}}{1 + \frac{1}{t}} \leq 0.5:\\
\;\;\;\;0.8333333333333334\\

\mathbf{else}:\\
\;\;\;\;0.5\\


\end{array}
\end{array}
        Derivation
        1. Split input into 2 regimes

        2. if (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t))) < 0.5

          1. Initial program 99.8%

            \[1 - \frac{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)} \]
          2. Add Preprocessing

          3. Taylor expanded in t around inf

            \[\leadsto \color{blue}{\frac{5}{6}} \]
          4. Step-by-step derivation

            1. Applied rewrites94.1%

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

            if 0.5 < (/.f32 (/.f32 #s(literal 2 binary32) t) (+.f32 #s(literal 1 binary32) (/.f32 #s(literal 1 binary32) t)))

            1. Initial program 98.5%

              \[1 - \frac{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)} \]
            2. Add Preprocessing

            3. Taylor expanded in t around 0

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

              1. Applied rewrites94.3%

                \[\leadsto \color{blue}{0.5} \]
            5. Recombined 2 regimes into one program.
            6. Add Preprocessing

            Alternative 14: 62.7% accurate, 101.0× speedup?

            \[\begin{array}{l} \\ 0.5 \end{array} \]
            (FPCore (t) :precision binary32 0.5)
            float code(float t) {
	return 0.5f;
}

            real(4) function code(t)
    real(4), intent (in) :: t
    code = 0.5e0
end function

            function code(t)
	return Float32(0.5)
end

            function tmp = code(t)
	tmp = single(0.5);
end

            \begin{array}{l}

\\
0.5
\end{array}
            Derivation

            1. Initial program 99.2%

              \[1 - \frac{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)} \]
            2. Add Preprocessing

            3. Taylor expanded in t around 0

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

              1. Applied rewrites59.4%

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

              Reproduce

              ?
              herbie shell --seed 2024341 
(FPCore (t)
  :name "Kahan p13 Example 3"
  :precision binary32
  (- 1.0 (/ 1.0 (+ 2.0 (* (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))) (- 2.0 (/ (/ 2.0 t) (+ 1.0 (/ 1.0 t)))))))))