Average Error: 54.0 → 10.3
Time: 24.7s
Precision: binary64
Cost: 43140
\[\left(\alpha > -1 \land \beta > -1\right) \land i > 1\]
\[ \begin{array}{c}[alpha, beta] = \mathsf{sort}([alpha, beta])\\ \end{array} \]
\[\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]
\[\begin{array}{l} t_0 := \left(\beta + \alpha\right) \cdot 2\\ t_1 := \left(\beta + \alpha\right) + 2 \cdot i\\ t_2 := \frac{\beta + \alpha}{i}\\ t_3 := {\left(\beta + \alpha\right)}^{2}\\ \mathbf{if}\;\beta \leq 1.5 \cdot 10^{+85}:\\ \;\;\;\;\left(0.0625 + 0.0625 \cdot \left(\frac{t_3 + \beta \cdot \alpha}{i \cdot i} + \frac{t_0}{i}\right)\right) - \mathsf{fma}\left(0.125, t_2, \mathsf{fma}\left(2, \frac{0.0625 \cdot t_0 + \left(\beta + \alpha\right) \cdot -0.125}{\frac{i \cdot i}{\beta + \alpha}}, 0.00390625 \cdot \frac{\mathsf{fma}\left(4, t_3 + -1, t_3 \cdot 20\right)}{i \cdot i}\right)\right)\\ \mathbf{elif}\;\beta \leq 1.2 \cdot 10^{+127}:\\ \;\;\;\;\frac{\frac{i \cdot i}{\frac{{\left(\beta + 2 \cdot i\right)}^{2}}{{\left(\beta + i\right)}^{2}}}}{-1 + t_1 \cdot t_1}\\ \mathbf{elif}\;\beta \leq 1.55 \cdot 10^{+154}:\\ \;\;\;\;\mathsf{fma}\left(\beta \cdot 0.125, \frac{1}{i}, 0.0625\right) + t_2 \cdot -0.125\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]
(FPCore (alpha beta i)
 :precision binary64
 (/
  (/
   (* (* i (+ (+ alpha beta) i)) (+ (* beta alpha) (* i (+ (+ alpha beta) i))))
   (* (+ (+ alpha beta) (* 2.0 i)) (+ (+ alpha beta) (* 2.0 i))))
  (- (* (+ (+ alpha beta) (* 2.0 i)) (+ (+ alpha beta) (* 2.0 i))) 1.0)))
(FPCore (alpha beta i)
 :precision binary64
 (let* ((t_0 (* (+ beta alpha) 2.0))
        (t_1 (+ (+ beta alpha) (* 2.0 i)))
        (t_2 (/ (+ beta alpha) i))
        (t_3 (pow (+ beta alpha) 2.0)))
   (if (<= beta 1.5e+85)
     (-
      (+ 0.0625 (* 0.0625 (+ (/ (+ t_3 (* beta alpha)) (* i i)) (/ t_0 i))))
      (fma
       0.125
       t_2
       (fma
        2.0
        (/
         (+ (* 0.0625 t_0) (* (+ beta alpha) -0.125))
         (/ (* i i) (+ beta alpha)))
        (* 0.00390625 (/ (fma 4.0 (+ t_3 -1.0) (* t_3 20.0)) (* i i))))))
     (if (<= beta 1.2e+127)
       (/
        (/ (* i i) (/ (pow (+ beta (* 2.0 i)) 2.0) (pow (+ beta i) 2.0)))
        (+ -1.0 (* t_1 t_1)))
       (if (<= beta 1.55e+154)
         (+ (fma (* beta 0.125) (/ 1.0 i) 0.0625) (* t_2 -0.125))
         (/ (/ (+ alpha i) beta) (/ beta i)))))))
double code(double alpha, double beta, double i) {
	return (((i * ((alpha + beta) + i)) * ((beta * alpha) + (i * ((alpha + beta) + i)))) / (((alpha + beta) + (2.0 * i)) * ((alpha + beta) + (2.0 * i)))) / ((((alpha + beta) + (2.0 * i)) * ((alpha + beta) + (2.0 * i))) - 1.0);
}
double code(double alpha, double beta, double i) {
	double t_0 = (beta + alpha) * 2.0;
	double t_1 = (beta + alpha) + (2.0 * i);
	double t_2 = (beta + alpha) / i;
	double t_3 = pow((beta + alpha), 2.0);
	double tmp;
	if (beta <= 1.5e+85) {
		tmp = (0.0625 + (0.0625 * (((t_3 + (beta * alpha)) / (i * i)) + (t_0 / i)))) - fma(0.125, t_2, fma(2.0, (((0.0625 * t_0) + ((beta + alpha) * -0.125)) / ((i * i) / (beta + alpha))), (0.00390625 * (fma(4.0, (t_3 + -1.0), (t_3 * 20.0)) / (i * i)))));
	} else if (beta <= 1.2e+127) {
		tmp = ((i * i) / (pow((beta + (2.0 * i)), 2.0) / pow((beta + i), 2.0))) / (-1.0 + (t_1 * t_1));
	} else if (beta <= 1.55e+154) {
		tmp = fma((beta * 0.125), (1.0 / i), 0.0625) + (t_2 * -0.125);
	} else {
		tmp = ((alpha + i) / beta) / (beta / i);
	}
	return tmp;
}
function code(alpha, beta, i)
	return Float64(Float64(Float64(Float64(i * Float64(Float64(alpha + beta) + i)) * Float64(Float64(beta * alpha) + Float64(i * Float64(Float64(alpha + beta) + i)))) / Float64(Float64(Float64(alpha + beta) + Float64(2.0 * i)) * Float64(Float64(alpha + beta) + Float64(2.0 * i)))) / Float64(Float64(Float64(Float64(alpha + beta) + Float64(2.0 * i)) * Float64(Float64(alpha + beta) + Float64(2.0 * i))) - 1.0))
end
function code(alpha, beta, i)
	t_0 = Float64(Float64(beta + alpha) * 2.0)
	t_1 = Float64(Float64(beta + alpha) + Float64(2.0 * i))
	t_2 = Float64(Float64(beta + alpha) / i)
	t_3 = Float64(beta + alpha) ^ 2.0
	tmp = 0.0
	if (beta <= 1.5e+85)
		tmp = Float64(Float64(0.0625 + Float64(0.0625 * Float64(Float64(Float64(t_3 + Float64(beta * alpha)) / Float64(i * i)) + Float64(t_0 / i)))) - fma(0.125, t_2, fma(2.0, Float64(Float64(Float64(0.0625 * t_0) + Float64(Float64(beta + alpha) * -0.125)) / Float64(Float64(i * i) / Float64(beta + alpha))), Float64(0.00390625 * Float64(fma(4.0, Float64(t_3 + -1.0), Float64(t_3 * 20.0)) / Float64(i * i))))));
	elseif (beta <= 1.2e+127)
		tmp = Float64(Float64(Float64(i * i) / Float64((Float64(beta + Float64(2.0 * i)) ^ 2.0) / (Float64(beta + i) ^ 2.0))) / Float64(-1.0 + Float64(t_1 * t_1)));
	elseif (beta <= 1.55e+154)
		tmp = Float64(fma(Float64(beta * 0.125), Float64(1.0 / i), 0.0625) + Float64(t_2 * -0.125));
	else
		tmp = Float64(Float64(Float64(alpha + i) / beta) / Float64(beta / i));
	end
	return tmp
end
code[alpha_, beta_, i_] := N[(N[(N[(N[(i * N[(N[(alpha + beta), $MachinePrecision] + i), $MachinePrecision]), $MachinePrecision] * N[(N[(beta * alpha), $MachinePrecision] + N[(i * N[(N[(alpha + beta), $MachinePrecision] + i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[(N[(alpha + beta), $MachinePrecision] + N[(2.0 * i), $MachinePrecision]), $MachinePrecision] * N[(N[(alpha + beta), $MachinePrecision] + N[(2.0 * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(N[(N[(N[(alpha + beta), $MachinePrecision] + N[(2.0 * i), $MachinePrecision]), $MachinePrecision] * N[(N[(alpha + beta), $MachinePrecision] + N[(2.0 * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - 1.0), $MachinePrecision]), $MachinePrecision]
code[alpha_, beta_, i_] := Block[{t$95$0 = N[(N[(beta + alpha), $MachinePrecision] * 2.0), $MachinePrecision]}, Block[{t$95$1 = N[(N[(beta + alpha), $MachinePrecision] + N[(2.0 * i), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(N[(beta + alpha), $MachinePrecision] / i), $MachinePrecision]}, Block[{t$95$3 = N[Power[N[(beta + alpha), $MachinePrecision], 2.0], $MachinePrecision]}, If[LessEqual[beta, 1.5e+85], N[(N[(0.0625 + N[(0.0625 * N[(N[(N[(t$95$3 + N[(beta * alpha), $MachinePrecision]), $MachinePrecision] / N[(i * i), $MachinePrecision]), $MachinePrecision] + N[(t$95$0 / i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] - N[(0.125 * t$95$2 + N[(2.0 * N[(N[(N[(0.0625 * t$95$0), $MachinePrecision] + N[(N[(beta + alpha), $MachinePrecision] * -0.125), $MachinePrecision]), $MachinePrecision] / N[(N[(i * i), $MachinePrecision] / N[(beta + alpha), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(0.00390625 * N[(N[(4.0 * N[(t$95$3 + -1.0), $MachinePrecision] + N[(t$95$3 * 20.0), $MachinePrecision]), $MachinePrecision] / N[(i * i), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[beta, 1.2e+127], N[(N[(N[(i * i), $MachinePrecision] / N[(N[Power[N[(beta + N[(2.0 * i), $MachinePrecision]), $MachinePrecision], 2.0], $MachinePrecision] / N[Power[N[(beta + i), $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(-1.0 + N[(t$95$1 * t$95$1), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], If[LessEqual[beta, 1.55e+154], N[(N[(N[(beta * 0.125), $MachinePrecision] * N[(1.0 / i), $MachinePrecision] + 0.0625), $MachinePrecision] + N[(t$95$2 * -0.125), $MachinePrecision]), $MachinePrecision], N[(N[(N[(alpha + i), $MachinePrecision] / beta), $MachinePrecision] / N[(beta / i), $MachinePrecision]), $MachinePrecision]]]]]]]]
\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1}
\begin{array}{l}
t_0 := \left(\beta + \alpha\right) \cdot 2\\
t_1 := \left(\beta + \alpha\right) + 2 \cdot i\\
t_2 := \frac{\beta + \alpha}{i}\\
t_3 := {\left(\beta + \alpha\right)}^{2}\\
\mathbf{if}\;\beta \leq 1.5 \cdot 10^{+85}:\\
\;\;\;\;\left(0.0625 + 0.0625 \cdot \left(\frac{t_3 + \beta \cdot \alpha}{i \cdot i} + \frac{t_0}{i}\right)\right) - \mathsf{fma}\left(0.125, t_2, \mathsf{fma}\left(2, \frac{0.0625 \cdot t_0 + \left(\beta + \alpha\right) \cdot -0.125}{\frac{i \cdot i}{\beta + \alpha}}, 0.00390625 \cdot \frac{\mathsf{fma}\left(4, t_3 + -1, t_3 \cdot 20\right)}{i \cdot i}\right)\right)\\

\mathbf{elif}\;\beta \leq 1.2 \cdot 10^{+127}:\\
\;\;\;\;\frac{\frac{i \cdot i}{\frac{{\left(\beta + 2 \cdot i\right)}^{2}}{{\left(\beta + i\right)}^{2}}}}{-1 + t_1 \cdot t_1}\\

\mathbf{elif}\;\beta \leq 1.55 \cdot 10^{+154}:\\
\;\;\;\;\mathsf{fma}\left(\beta \cdot 0.125, \frac{1}{i}, 0.0625\right) + t_2 \cdot -0.125\\

\mathbf{else}:\\
\;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\


\end{array}

Error

Derivation

  1. Split input into 4 regimes
  2. if beta < 1.5e85

    1. Initial program 47.9

      \[\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]
    2. Simplified48.2

      \[\leadsto \color{blue}{\frac{\left(i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) \cdot \mathsf{fma}\left(\beta, \alpha, i \cdot \left(i + \left(\alpha + \beta\right)\right)\right)}{\mathsf{fma}\left(\alpha + \left(\beta + i \cdot 2\right), \alpha + \left(\beta + i \cdot 2\right), -1\right) \cdot \left(\left(\alpha + \left(\beta + i \cdot 2\right)\right) \cdot \left(\alpha + \left(\beta + i \cdot 2\right)\right)\right)}} \]
      Proof
      (/.f64 (*.f64 (*.f64 i (+.f64 i (+.f64 alpha beta))) (fma.f64 beta alpha (*.f64 i (+.f64 i (+.f64 alpha beta))))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) i))) (fma.f64 beta alpha (*.f64 i (+.f64 i (+.f64 alpha beta))))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (fma.f64 beta alpha (*.f64 i (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) i))))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (Rewrite<= *-commutative_binary64 (*.f64 2 i)))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 alpha (+.f64 beta (Rewrite<= *-commutative_binary64 (*.f64 2 i)))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= metadata-eval (neg.f64 1))) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 alpha (+.f64 beta (Rewrite<= *-commutative_binary64 (*.f64 2 i)))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 alpha (+.f64 beta (Rewrite<= *-commutative_binary64 (*.f64 2 i))))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1))): 4 points increase in error, 12 points decrease in error
    3. Taylor expanded in i around inf 2.1

      \[\leadsto \color{blue}{\left(0.0625 + \left(0.0625 \cdot \frac{{\left(\beta + \alpha\right)}^{2} + \beta \cdot \alpha}{{i}^{2}} + 0.0625 \cdot \frac{2 \cdot \beta + 2 \cdot \alpha}{i}\right)\right) - \left(0.125 \cdot \frac{\beta + \alpha}{i} + \left(2 \cdot \frac{\left(0.0625 \cdot \left(2 \cdot \alpha + 2 \cdot \beta\right) - 0.125 \cdot \left(\beta + \alpha\right)\right) \cdot \left(\beta + \alpha\right)}{{i}^{2}} + 0.00390625 \cdot \frac{4 \cdot \left({\left(\beta + \alpha\right)}^{2} - 1\right) + \left(16 \cdot {\left(\beta + \alpha\right)}^{2} + 4 \cdot {\left(\beta + \alpha\right)}^{2}\right)}{{i}^{2}}\right)\right)} \]
    4. Simplified2.1

      \[\leadsto \color{blue}{\left(0.0625 + 0.0625 \cdot \left(\frac{{\left(\beta + \alpha\right)}^{2} + \beta \cdot \alpha}{i \cdot i} + \frac{2 \cdot \left(\beta + \alpha\right)}{i}\right)\right) - \mathsf{fma}\left(0.125, \frac{\beta + \alpha}{i}, \mathsf{fma}\left(2, \frac{0.0625 \cdot \left(2 \cdot \left(\beta + \alpha\right)\right) + -0.125 \cdot \left(\beta + \alpha\right)}{\frac{i \cdot i}{\beta + \alpha}}, 0.00390625 \cdot \frac{\mathsf{fma}\left(4, {\left(\beta + \alpha\right)}^{2} + -1, {\left(\beta + \alpha\right)}^{2} \cdot 20\right)}{i \cdot i}\right)\right)} \]
      Proof
      (-.f64 (+.f64 1/16 (*.f64 1/16 (+.f64 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (*.f64 i i)) (/.f64 (*.f64 2 (+.f64 beta alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (+.f64 (*.f64 1/16 (*.f64 2 (+.f64 beta alpha))) (*.f64 -1/8 (+.f64 beta alpha))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (*.f64 1/16 (+.f64 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (Rewrite<= unpow2_binary64 (pow.f64 i 2))) (/.f64 (*.f64 2 (+.f64 beta alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (+.f64 (*.f64 1/16 (*.f64 2 (+.f64 beta alpha))) (*.f64 -1/8 (+.f64 beta alpha))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (*.f64 1/16 (+.f64 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2)) (/.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (+.f64 (*.f64 1/16 (*.f64 2 (+.f64 beta alpha))) (*.f64 -1/8 (+.f64 beta alpha))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i))))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (+.f64 (*.f64 1/16 (*.f64 2 (+.f64 beta alpha))) (*.f64 -1/8 (+.f64 beta alpha))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (+.f64 (*.f64 1/16 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)))) (*.f64 -1/8 (+.f64 beta alpha))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (+.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 (Rewrite<= metadata-eval (neg.f64 1/8)) (+.f64 beta alpha))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha))) (*.f64 1/8 (+.f64 beta alpha)))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (Rewrite=> fma-neg_binary64 (fma.f64 1/16 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) (neg.f64 (*.f64 1/8 (+.f64 beta alpha))))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (fma.f64 1/16 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (neg.f64 (*.f64 1/8 (+.f64 beta alpha)))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha)))) (/.f64 (*.f64 i i) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 i 2)) (+.f64 beta alpha))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) -1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (pow.f64 i 2)) (*.f64 1/256 (/.f64 (fma.f64 4 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (Rewrite<= metadata-eval (neg.f64 1))) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (pow.f64 i 2)) (*.f64 1/256 (/.f64 (fma.f64 4 (Rewrite<= sub-neg_binary64 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (*.f64 (pow.f64 (+.f64 beta alpha) 2) 20)) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (pow.f64 i 2)) (*.f64 1/256 (/.f64 (fma.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1) (*.f64 (pow.f64 (+.f64 beta alpha) 2) (Rewrite<= metadata-eval (+.f64 16 4)))) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (pow.f64 i 2)) (*.f64 1/256 (/.f64 (fma.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (pow.f64 (+.f64 beta alpha) 2))))) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (pow.f64 i 2)) (*.f64 1/256 (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (pow.f64 (+.f64 beta alpha) 2))))) (*.f64 i i)))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (fma.f64 2 (/.f64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (pow.f64 i 2)) (*.f64 1/256 (/.f64 (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)))) (Rewrite<= unpow2_binary64 (pow.f64 i 2))))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (fma.f64 1/8 (/.f64 (+.f64 beta alpha) i) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 (/.f64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/256 (/.f64 (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)))) (pow.f64 i 2))))))): 0 points increase in error, 0 points decrease in error
      (-.f64 (+.f64 1/16 (+.f64 (*.f64 1/16 (/.f64 (+.f64 (pow.f64 (+.f64 beta alpha) 2) (*.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/16 (/.f64 (+.f64 (*.f64 2 beta) (*.f64 2 alpha)) i)))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 1/8 (/.f64 (+.f64 beta alpha) i)) (+.f64 (*.f64 2 (/.f64 (*.f64 (-.f64 (*.f64 1/16 (+.f64 (*.f64 2 alpha) (*.f64 2 beta))) (*.f64 1/8 (+.f64 beta alpha))) (+.f64 beta alpha)) (pow.f64 i 2))) (*.f64 1/256 (/.f64 (+.f64 (*.f64 4 (-.f64 (pow.f64 (+.f64 beta alpha) 2) 1)) (+.f64 (*.f64 16 (pow.f64 (+.f64 beta alpha) 2)) (*.f64 4 (pow.f64 (+.f64 beta alpha) 2)))) (pow.f64 i 2))))))): 0 points increase in error, 0 points decrease in error

    if 1.5e85 < beta < 1.2000000000000001e127

    1. Initial program 55.4

      \[\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]
    2. Applied egg-rr32.5

      \[\leadsto \frac{\color{blue}{\mathsf{fma}\left(i, i + \left(\alpha + \beta\right), \alpha \cdot \beta\right) \cdot \left(\left(i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) \cdot {\left(\mathsf{fma}\left(i, 2, \alpha + \beta\right)\right)}^{-2}\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]
    3. Taylor expanded in alpha around 0 56.3

      \[\leadsto \frac{\color{blue}{\frac{{i}^{2} \cdot {\left(\beta + i\right)}^{2}}{{\left(\beta + 2 \cdot i\right)}^{2}}}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]
    4. Simplified34.3

      \[\leadsto \frac{\color{blue}{\frac{i \cdot i}{\frac{{\left(\beta + i \cdot 2\right)}^{2}}{{\left(i + \beta\right)}^{2}}}}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]
      Proof
      (/.f64 (*.f64 i i) (/.f64 (pow.f64 (+.f64 beta (*.f64 i 2)) 2) (pow.f64 (+.f64 i beta) 2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 i 2)) (/.f64 (pow.f64 (+.f64 beta (*.f64 i 2)) 2) (pow.f64 (+.f64 i beta) 2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (pow.f64 i 2) (/.f64 (pow.f64 (+.f64 beta (Rewrite<= *-commutative_binary64 (*.f64 2 i))) 2) (pow.f64 (+.f64 i beta) 2))): 0 points increase in error, 0 points decrease in error
      (/.f64 (pow.f64 i 2) (/.f64 (pow.f64 (+.f64 beta (*.f64 2 i)) 2) (pow.f64 (Rewrite<= +-commutative_binary64 (+.f64 beta i)) 2))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 i 2) (pow.f64 (+.f64 beta i) 2)) (pow.f64 (+.f64 beta (*.f64 2 i)) 2))): 49 points increase in error, 1 points decrease in error

    if 1.2000000000000001e127 < beta < 1.5500000000000001e154

    1. Initial program 61.0

      \[\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]
    2. Simplified31.7

      \[\leadsto \color{blue}{\frac{i}{\mathsf{fma}\left(\beta + \mathsf{fma}\left(i, 2, \alpha\right), \beta + \mathsf{fma}\left(i, 2, \alpha\right), -1\right)} \cdot \frac{\mathsf{fma}\left(i, i + \left(\alpha + \beta\right), \alpha \cdot \beta\right)}{\frac{\left(\beta + \mathsf{fma}\left(i, 2, \alpha\right)\right) \cdot \left(\beta + \mathsf{fma}\left(i, 2, \alpha\right)\right)}{i + \left(\alpha + \beta\right)}}} \]
      Proof
      (*.f64 (/.f64 i (fma.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (+.f64 beta (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i 2) alpha))) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (+.f64 beta (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 i)) alpha)) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 beta (*.f64 2 i)) alpha)) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta (*.f64 2 i)))) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 beta (fma.f64 i 2 alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 beta (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i 2) alpha))) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 beta (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 i)) alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 beta (*.f64 2 i)) alpha)) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta (*.f64 2 i)))) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) -1)) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= metadata-eval (neg.f64 1)))) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1))) (/.f64 (fma.f64 i (+.f64 i (+.f64 alpha beta)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (fma.f64 i (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) i)) (*.f64 alpha beta)) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (fma.f64 i (+.f64 (+.f64 alpha beta) i) (Rewrite<= *-commutative_binary64 (*.f64 beta alpha))) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (*.f64 beta alpha))) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (/.f64 (*.f64 (+.f64 beta (fma.f64 i 2 alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 beta (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i 2) alpha))) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 beta (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 i)) alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 beta (*.f64 2 i)) alpha)) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta (*.f64 2 i)))) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 beta (fma.f64 i 2 alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 beta (Rewrite<= fma-def_binary64 (+.f64 (*.f64 i 2) alpha)))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 beta (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 2 i)) alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 beta (*.f64 2 i)) alpha))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta (*.f64 2 i))))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (+.f64 i (+.f64 alpha beta))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (/.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) i))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))) (+.f64 (+.f64 alpha beta) i)) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))))): 48 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 i (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (+.f64 alpha beta) i) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))))) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= times-frac_binary64 (/.f64 (*.f64 i (*.f64 (+.f64 (+.f64 alpha beta) i) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))))): 30 points increase in error, 8 points decrease in error
      (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))))): 0 points increase in error, 8 points decrease in error
      (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1))): 4 points increase in error, 12 points decrease in error
    3. Taylor expanded in i around inf 28.1

      \[\leadsto \color{blue}{\left(0.0625 + 0.0625 \cdot \frac{2 \cdot \beta + 2 \cdot \alpha}{i}\right) - 0.125 \cdot \frac{\beta + \alpha}{i}} \]
    4. Taylor expanded in alpha around 0 28.1

      \[\leadsto \color{blue}{\left(0.0625 + 0.125 \cdot \frac{\beta}{i}\right)} - 0.125 \cdot \frac{\beta + \alpha}{i} \]
    5. Applied egg-rr28.3

      \[\leadsto \color{blue}{\mathsf{fma}\left(0.125 \cdot \beta, \frac{1}{i}, 0.0625\right)} - 0.125 \cdot \frac{\beta + \alpha}{i} \]

    if 1.5500000000000001e154 < beta

    1. Initial program 64.0

      \[\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1} \]
    2. Simplified64.0

      \[\leadsto \color{blue}{\frac{\left(i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) \cdot \mathsf{fma}\left(\beta, \alpha, i \cdot \left(i + \left(\alpha + \beta\right)\right)\right)}{\mathsf{fma}\left(\alpha + \left(\beta + i \cdot 2\right), \alpha + \left(\beta + i \cdot 2\right), -1\right) \cdot \left(\left(\alpha + \left(\beta + i \cdot 2\right)\right) \cdot \left(\alpha + \left(\beta + i \cdot 2\right)\right)\right)}} \]
      Proof
      (/.f64 (*.f64 (*.f64 i (+.f64 i (+.f64 alpha beta))) (fma.f64 beta alpha (*.f64 i (+.f64 i (+.f64 alpha beta))))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) i))) (fma.f64 beta alpha (*.f64 i (+.f64 i (+.f64 alpha beta))))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (fma.f64 beta alpha (*.f64 i (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) i))))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i))))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (+.f64 alpha (+.f64 beta (Rewrite<= *-commutative_binary64 (*.f64 2 i)))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 alpha (+.f64 beta (*.f64 i 2))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 alpha (+.f64 beta (Rewrite<= *-commutative_binary64 (*.f64 2 i)))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) -1) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (fma.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= metadata-eval (neg.f64 1))) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (Rewrite<= fma-neg_binary64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1)) (*.f64 (+.f64 alpha (+.f64 beta (*.f64 i 2))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 alpha (+.f64 beta (Rewrite<= *-commutative_binary64 (*.f64 2 i)))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i))) (+.f64 alpha (+.f64 beta (*.f64 i 2)))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 alpha (+.f64 beta (Rewrite<= *-commutative_binary64 (*.f64 2 i))))))): 0 points increase in error, 0 points decrease in error
      (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (*.f64 (*.f64 i (+.f64 (+.f64 alpha beta) i)) (+.f64 (*.f64 beta alpha) (*.f64 i (+.f64 (+.f64 alpha beta) i)))) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i)))) (-.f64 (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 i)) (+.f64 (+.f64 alpha beta) (*.f64 2 i))) 1))): 4 points increase in error, 12 points decrease in error
    3. Taylor expanded in beta around inf 49.9

      \[\leadsto \color{blue}{\frac{\left(i + \alpha\right) \cdot i}{{\beta}^{2}}} \]
    4. Simplified48.7

      \[\leadsto \color{blue}{\frac{i + \alpha}{\frac{\beta \cdot \beta}{i}}} \]
      Proof
      (/.f64 (+.f64 i alpha) (/.f64 (*.f64 beta beta) i)): 0 points increase in error, 0 points decrease in error
      (/.f64 (+.f64 i alpha) (/.f64 (Rewrite<= unpow2_binary64 (pow.f64 beta 2)) i)): 0 points increase in error, 0 points decrease in error
      (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 i alpha) i) (pow.f64 beta 2))): 65 points increase in error, 5 points decrease in error
    5. Applied egg-rr36.3

      \[\leadsto \frac{i + \alpha}{\color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\frac{\beta}{i} \cdot \beta\right)\right)}} \]
    6. Applied egg-rr17.8

      \[\leadsto \color{blue}{\frac{1}{\beta} \cdot \frac{i + \alpha}{\frac{\beta}{i}}} \]
    7. Applied egg-rr17.4

      \[\leadsto \color{blue}{\frac{\frac{i + \alpha}{\beta}}{\frac{\beta}{i}}} \]
  3. Recombined 4 regimes into one program.
  4. Final simplification10.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\beta \leq 1.5 \cdot 10^{+85}:\\ \;\;\;\;\left(0.0625 + 0.0625 \cdot \left(\frac{{\left(\beta + \alpha\right)}^{2} + \beta \cdot \alpha}{i \cdot i} + \frac{\left(\beta + \alpha\right) \cdot 2}{i}\right)\right) - \mathsf{fma}\left(0.125, \frac{\beta + \alpha}{i}, \mathsf{fma}\left(2, \frac{0.0625 \cdot \left(\left(\beta + \alpha\right) \cdot 2\right) + \left(\beta + \alpha\right) \cdot -0.125}{\frac{i \cdot i}{\beta + \alpha}}, 0.00390625 \cdot \frac{\mathsf{fma}\left(4, {\left(\beta + \alpha\right)}^{2} + -1, {\left(\beta + \alpha\right)}^{2} \cdot 20\right)}{i \cdot i}\right)\right)\\ \mathbf{elif}\;\beta \leq 1.2 \cdot 10^{+127}:\\ \;\;\;\;\frac{\frac{i \cdot i}{\frac{{\left(\beta + 2 \cdot i\right)}^{2}}{{\left(\beta + i\right)}^{2}}}}{-1 + \left(\left(\beta + \alpha\right) + 2 \cdot i\right) \cdot \left(\left(\beta + \alpha\right) + 2 \cdot i\right)}\\ \mathbf{elif}\;\beta \leq 1.55 \cdot 10^{+154}:\\ \;\;\;\;\mathsf{fma}\left(\beta \cdot 0.125, \frac{1}{i}, 0.0625\right) + \frac{\beta + \alpha}{i} \cdot -0.125\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]

Alternatives

Alternative 1
Error10.3
Cost15176
\[\begin{array}{l} t_0 := \left(\beta + \alpha\right) + 2 \cdot i\\ \mathbf{if}\;\beta \leq 7 \cdot 10^{+85}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 6.8 \cdot 10^{+127}:\\ \;\;\;\;\frac{\frac{i \cdot i}{\frac{{\left(\beta + 2 \cdot i\right)}^{2}}{{\left(\beta + i\right)}^{2}}}}{-1 + t_0 \cdot t_0}\\ \mathbf{elif}\;\beta \leq 1.65 \cdot 10^{+154}:\\ \;\;\;\;\mathsf{fma}\left(\beta \cdot 0.125, \frac{1}{i}, 0.0625\right) + \frac{\beta + \alpha}{i} \cdot -0.125\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]
Alternative 2
Error10.3
Cost15048
\[\begin{array}{l} \mathbf{if}\;\beta \leq 4.5 \cdot 10^{+85}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 2.55 \cdot 10^{+127}:\\ \;\;\;\;\frac{i \cdot i}{-1 + \left(\beta \cdot \beta + 2 \cdot \left(i \cdot \left(2 \cdot \left(\beta + i\right)\right)\right)\right)} \cdot \frac{{\left(\beta + i\right)}^{2}}{{\left(\beta + 2 \cdot i\right)}^{2}}\\ \mathbf{elif}\;\beta \leq 4.5 \cdot 10^{+153}:\\ \;\;\;\;\mathsf{fma}\left(\beta \cdot 0.125, \frac{1}{i}, 0.0625\right) + \frac{\beta + \alpha}{i} \cdot -0.125\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]
Alternative 3
Error10.9
Cost7756
\[\begin{array}{l} t_0 := \alpha + 2 \cdot i\\ \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 2.05 \cdot 10^{+127}:\\ \;\;\;\;\frac{i \cdot \left(\alpha + i\right)}{-1 + \left(\beta \cdot \beta + t_0 \cdot \left(t_0 + \beta \cdot 2\right)\right)}\\ \mathbf{elif}\;\beta \leq 3.2 \cdot 10^{+154}:\\ \;\;\;\;\mathsf{fma}\left(\beta \cdot 0.125, \frac{1}{i}, 0.0625\right) + \frac{\beta + \alpha}{i} \cdot -0.125\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]
Alternative 4
Error10.9
Cost1992
\[\begin{array}{l} t_0 := \alpha + 2 \cdot i\\ \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 1.45 \cdot 10^{+127}:\\ \;\;\;\;\frac{i \cdot \left(\alpha + i\right)}{-1 + \left(\beta \cdot \beta + t_0 \cdot \left(t_0 + \beta \cdot 2\right)\right)}\\ \mathbf{elif}\;\beta \leq 4 \cdot 10^{+155}:\\ \;\;\;\;\left(0.0625 + 0.125 \cdot \frac{\beta}{i}\right) + \frac{\beta \cdot -0.125}{i}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]
Alternative 5
Error11.0
Cost1736
\[\begin{array}{l} t_0 := \left(\beta + \alpha\right) + 2 \cdot i\\ \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 1.15 \cdot 10^{+127}:\\ \;\;\;\;\frac{i \cdot \left(\alpha + i\right)}{-1 + t_0 \cdot t_0}\\ \mathbf{elif}\;\beta \leq 1.95 \cdot 10^{+154}:\\ \;\;\;\;\left(0.0625 + 0.125 \cdot \frac{\beta}{i}\right) + \frac{\beta \cdot -0.125}{i}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]
Alternative 6
Error11.1
Cost1228
\[\begin{array}{l} \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 3.15 \cdot 10^{+127}:\\ \;\;\;\;\frac{i \cdot \frac{i}{\beta}}{\beta}\\ \mathbf{elif}\;\beta \leq 6.3 \cdot 10^{+153}:\\ \;\;\;\;\left(0.0625 + 0.125 \cdot \frac{\beta}{i}\right) + \frac{\beta \cdot -0.125}{i}\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]
Alternative 7
Error11.1
Cost972
\[\begin{array}{l} \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 4.6 \cdot 10^{+124}:\\ \;\;\;\;\frac{i \cdot \frac{i}{\beta}}{\beta}\\ \mathbf{elif}\;\beta \leq 2.65 \cdot 10^{+154}:\\ \;\;\;\;0.0625\\ \mathbf{else}:\\ \;\;\;\;\frac{\alpha + i}{\beta} \cdot \frac{i}{\beta}\\ \end{array} \]
Alternative 8
Error11.1
Cost972
\[\begin{array}{l} \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 4.6 \cdot 10^{+124}:\\ \;\;\;\;\frac{i \cdot \frac{i}{\beta}}{\beta}\\ \mathbf{elif}\;\beta \leq 1.16 \cdot 10^{+154}:\\ \;\;\;\;0.0625\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{\alpha + i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]
Alternative 9
Error12.6
Cost844
\[\begin{array}{l} t_0 := \frac{i}{\beta} \cdot \frac{i}{\beta}\\ \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 6.5 \cdot 10^{+125}:\\ \;\;\;\;t_0\\ \mathbf{elif}\;\beta \leq 2.02 \cdot 10^{+155}:\\ \;\;\;\;0.0625\\ \mathbf{else}:\\ \;\;\;\;t_0\\ \end{array} \]
Alternative 10
Error12.5
Cost844
\[\begin{array}{l} \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 4.6 \cdot 10^{+124}:\\ \;\;\;\;\frac{i}{\beta \cdot \frac{\beta}{i}}\\ \mathbf{elif}\;\beta \leq 1.7 \cdot 10^{+155}:\\ \;\;\;\;0.0625\\ \mathbf{else}:\\ \;\;\;\;\frac{i}{\beta} \cdot \frac{i}{\beta}\\ \end{array} \]
Alternative 11
Error12.6
Cost844
\[\begin{array}{l} \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 1.2 \cdot 10^{+125}:\\ \;\;\;\;\frac{i \cdot \frac{i}{\beta}}{\beta}\\ \mathbf{elif}\;\beta \leq 7 \cdot 10^{+153}:\\ \;\;\;\;0.0625\\ \mathbf{else}:\\ \;\;\;\;\frac{i}{\beta} \cdot \frac{i}{\beta}\\ \end{array} \]
Alternative 12
Error12.6
Cost844
\[\begin{array}{l} \mathbf{if}\;\beta \leq 1.1 \cdot 10^{+86}:\\ \;\;\;\;0.0625\\ \mathbf{elif}\;\beta \leq 4.6 \cdot 10^{+124}:\\ \;\;\;\;\frac{i \cdot \frac{i}{\beta}}{\beta}\\ \mathbf{elif}\;\beta \leq 2.05 \cdot 10^{+153}:\\ \;\;\;\;0.0625\\ \mathbf{else}:\\ \;\;\;\;\frac{\frac{i}{\beta}}{\frac{\beta}{i}}\\ \end{array} \]
Alternative 13
Error15.8
Cost580
\[\begin{array}{l} \mathbf{if}\;\beta \leq 6.8 \cdot 10^{+239}:\\ \;\;\;\;0.0625\\ \mathbf{else}:\\ \;\;\;\;\frac{i}{\beta} \cdot \frac{\alpha}{\beta}\\ \end{array} \]
Alternative 14
Error16.7
Cost196
\[\begin{array}{l} \mathbf{if}\;\beta \leq 2.65 \cdot 10^{+256}:\\ \;\;\;\;0.0625\\ \mathbf{else}:\\ \;\;\;\;0\\ \end{array} \]
Alternative 15
Error57.8
Cost64
\[0 \]

Error

Reproduce

herbie shell --seed 2022325 
(FPCore (alpha beta i)
  :name "Octave 3.8, jcobi/4"
  :precision binary64
  :pre (and (and (> alpha -1.0) (> beta -1.0)) (> i 1.0))
  (/ (/ (* (* i (+ (+ alpha beta) i)) (+ (* beta alpha) (* i (+ (+ alpha beta) i)))) (* (+ (+ alpha beta) (* 2.0 i)) (+ (+ alpha beta) (* 2.0 i)))) (- (* (+ (+ alpha beta) (* 2.0 i)) (+ (+ alpha beta) (* 2.0 i))) 1.0)))