Kahan p13 Example 1

Average Error: 0.1 → 0.0

Time: 14.0s

Precision: binary64

Cost: 20736

Math

\[\frac{1 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}}{2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}} \]

↓

\[\begin{array}{l} t_1 := \frac{4}{\frac{1}{t} + \left(t + 2\right)}\\ {\left(\frac{\mathsf{fma}\left(t, t_1, 2\right)}{\mathsf{fma}\left(t, t_1, 1\right)}\right)}^{-1} \end{array} \]

FPCore

(FPCore (t)
 :precision binary64
 (/
  (+ 1.0 (* (/ (* 2.0 t) (+ 1.0 t)) (/ (* 2.0 t) (+ 1.0 t))))
  (+ 2.0 (* (/ (* 2.0 t) (+ 1.0 t)) (/ (* 2.0 t) (+ 1.0 t))))))

↓

(FPCore (t)
 :precision binary64
 (let* ((t_1 (/ 4.0 (+ (/ 1.0 t) (+ t 2.0)))))
   (pow (/ (fma t t_1 2.0) (fma t t_1 1.0)) -1.0)))

C

double code(double t) {
	return (1.0 + (((2.0 * t) / (1.0 + t)) * ((2.0 * t) / (1.0 + t)))) / (2.0 + (((2.0 * t) / (1.0 + t)) * ((2.0 * t) / (1.0 + t))));
}

↓

double code(double t) {
	double t_1 = 4.0 / ((1.0 / t) + (t + 2.0));
	return pow((fma(t, t_1, 2.0) / fma(t, t_1, 1.0)), -1.0);
}

Julia

function code(t)
	return Float64(Float64(1.0 + Float64(Float64(Float64(2.0 * t) / Float64(1.0 + t)) * Float64(Float64(2.0 * t) / Float64(1.0 + t)))) / Float64(2.0 + Float64(Float64(Float64(2.0 * t) / Float64(1.0 + t)) * Float64(Float64(2.0 * t) / Float64(1.0 + t)))))
end

↓

function code(t)
	t_1 = Float64(4.0 / Float64(Float64(1.0 / t) + Float64(t + 2.0)))
	return Float64(fma(t, t_1, 2.0) / fma(t, t_1, 1.0)) ^ -1.0
end

Wolfram

code[t_] := N[(N[(1.0 + N[(N[(N[(2.0 * t), $MachinePrecision] / N[(1.0 + t), $MachinePrecision]), $MachinePrecision] * N[(N[(2.0 * t), $MachinePrecision] / N[(1.0 + t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(2.0 + N[(N[(N[(2.0 * t), $MachinePrecision] / N[(1.0 + t), $MachinePrecision]), $MachinePrecision] * N[(N[(2.0 * t), $MachinePrecision] / N[(1.0 + t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

↓

code[t_] := Block[{t$95$1 = N[(4.0 / N[(N[(1.0 / t), $MachinePrecision] + N[(t + 2.0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[Power[N[(N[(t * t$95$1 + 2.0), $MachinePrecision] / N[(t * t$95$1 + 1.0), $MachinePrecision]), $MachinePrecision], -1.0], $MachinePrecision]]

Derivation

1. Initial program 0.1

   \[\frac{1 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}}{2 + \frac{2 \cdot t}{1 + t} \cdot \frac{2 \cdot t}{1 + t}} \]

2. Simplified 0.0

   \[\leadsto \color{blue}{\frac{\mathsf{fma}\left(t, \frac{4}{t + \left(2 + \frac{1}{t}\right)}, 1\right)}{\mathsf{fma}\left(t, \frac{4}{t + \left(2 + \frac{1}{t}\right)}, 2\right)}} \]
   Proof
   (/.f64 (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (Rewrite<= metadata-eval (*.f64 2 2)) (+.f64 t (+.f64 2 (/.f64 1 t)))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 (Rewrite<= metadata-eval (+.f64 1 1)) (/.f64 1 t)))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (Rewrite<= associate-+r+_binary64 (+.f64 1 (+.f64 1 (/.f64 1 t)))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (Rewrite<= *-inverses_binary64 (/.f64 t t)) (/.f64 1 t))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 t 1)) t) (/.f64 1 t))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (/.f64 (*.f64 t 1) (Rewrite<= *-lft-identity_binary64 (*.f64 1 t))) (/.f64 1 t))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 t 1) (/.f64 1 t))) (/.f64 1 t))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (*.f64 (Rewrite=> /-rgt-identity_binary64 t) (/.f64 1 t)) (/.f64 1 t))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (*.f64 t (/.f64 1 t)) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 1 t))))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (Rewrite<= distribute-rgt-in_binary64 (*.f64 (/.f64 1 t) (+.f64 t 1)))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (*.f64 (/.f64 1 t) (Rewrite<= +-commutative_binary64 (+.f64 1 t)))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 t (+.f64 1 t))))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 1 (+.f64 1 t)) t))))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (/.f64 (Rewrite=> *-lft-identity_binary64 (+.f64 1 t)) t)))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 t 1) (/.f64 (+.f64 1 t) t)))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 t)) (/.f64 (+.f64 1 t) t))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (+.f64 1 t) 1)) (/.f64 (+.f64 1 t) t))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (/.f64 (+.f64 1 t) (Rewrite<= *-inverses_binary64 (/.f64 t t))) (/.f64 (+.f64 1 t) t))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 1 t) t) t)) (/.f64 (+.f64 1 t) t))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 70 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (+.f64 1 t) t) t)) (/.f64 (+.f64 1 t) t))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 70 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (*.f64 (/.f64 (+.f64 1 t) t) t) (Rewrite<= *-rgt-identity_binary64 (*.f64 (/.f64 (+.f64 1 t) t) 1)))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (Rewrite=> distribute-lft-out_binary64 (*.f64 (/.f64 (+.f64 1 t) t) (+.f64 t 1)))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 1 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 2) (*.f64 (/.f64 (+.f64 1 t) t) (Rewrite<= +-commutative_binary64 (+.f64 1 t)))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (*.f64 2 2) (/.f64 (+.f64 1 t) t)) (+.f64 1 t))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 2 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 2 (/.f64 (+.f64 1 t) t)))) (+.f64 1 t)) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (fma.f64 t (/.f64 (*.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 2 t) (+.f64 1 t)))) (+.f64 1 t)) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 1 points increase in error, 1 points decrease in error
   (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 t (/.f64 (*.f64 2 (/.f64 (*.f64 2 t) (+.f64 1 t))) (+.f64 1 t))) 1)) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 1 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (*.f64 2 (/.f64 (*.f64 2 t) (+.f64 1 t))) (+.f64 1 t)) t)) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 2 (/.f64 (*.f64 2 t) (+.f64 1 t))) (/.f64 (+.f64 1 t) t))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 2 points decrease in error
   (/.f64 (+.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 2 (/.f64 (+.f64 1 t) t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 2 t) (+.f64 1 t))) (/.f64 (*.f64 2 t) (+.f64 1 t))) 1) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 2 points increase in error, 1 points decrease in error
   (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t))))) (fma.f64 t (/.f64 4 (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (Rewrite<= metadata-eval (*.f64 2 2)) (+.f64 t (+.f64 2 (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 (Rewrite<= metadata-eval (+.f64 1 1)) (/.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (Rewrite<= associate-+r+_binary64 (+.f64 1 (+.f64 1 (/.f64 1 t)))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (Rewrite<= *-inverses_binary64 (/.f64 t t)) (/.f64 1 t))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 t 1)) t) (/.f64 1 t))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (/.f64 (*.f64 t 1) (Rewrite<= *-lft-identity_binary64 (*.f64 1 t))) (/.f64 1 t))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 t 1) (/.f64 1 t))) (/.f64 1 t))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (*.f64 (Rewrite=> /-rgt-identity_binary64 t) (/.f64 1 t)) (/.f64 1 t))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (+.f64 (*.f64 t (/.f64 1 t)) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 1 t))))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (Rewrite<= distribute-rgt-in_binary64 (*.f64 (/.f64 1 t) (+.f64 t 1)))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (*.f64 (/.f64 1 t) (Rewrite<= +-commutative_binary64 (+.f64 1 t)))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 t (+.f64 1 t))))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 1 (+.f64 1 t)) t))))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 t (+.f64 1 (/.f64 (Rewrite=> *-lft-identity_binary64 (+.f64 1 t)) t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 t 1) (/.f64 (+.f64 1 t) t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 t)) (/.f64 (+.f64 1 t) t))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (+.f64 1 t) 1)) (/.f64 (+.f64 1 t) t))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (/.f64 (+.f64 1 t) (Rewrite<= *-inverses_binary64 (/.f64 t t))) (/.f64 (+.f64 1 t) t))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 1 t) t) t)) (/.f64 (+.f64 1 t) t))) 2)): 69 points increase in error, 2 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (+.f64 1 t) t) t)) (/.f64 (+.f64 1 t) t))) 2)): 2 points increase in error, 69 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (+.f64 (*.f64 (/.f64 (+.f64 1 t) t) t) (Rewrite<= *-rgt-identity_binary64 (*.f64 (/.f64 (+.f64 1 t) t) 1)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (Rewrite=> distribute-lft-out_binary64 (*.f64 (/.f64 (+.f64 1 t) t) (+.f64 t 1)))) 2)): 0 points increase in error, 1 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 2) (*.f64 (/.f64 (+.f64 1 t) t) (Rewrite<= +-commutative_binary64 (+.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (*.f64 2 2) (/.f64 (+.f64 1 t) t)) (+.f64 1 t))) 2)): 1 points increase in error, 1 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (Rewrite<= associate-*r/_binary64 (*.f64 2 (/.f64 2 (/.f64 (+.f64 1 t) t)))) (+.f64 1 t)) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (fma.f64 t (/.f64 (*.f64 2 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 2 t) (+.f64 1 t)))) (+.f64 1 t)) 2)): 0 points increase in error, 2 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 t (/.f64 (*.f64 2 (/.f64 (*.f64 2 t) (+.f64 1 t))) (+.f64 1 t))) 2))): 1 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (*.f64 2 (/.f64 (*.f64 2 t) (+.f64 1 t))) (+.f64 1 t)) t)) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (+.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (*.f64 2 (/.f64 (*.f64 2 t) (+.f64 1 t))) (/.f64 (+.f64 1 t) t))) 2)): 2 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (+.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 2 (/.f64 (+.f64 1 t) t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) 2)): 0 points increase in error, 0 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (+.f64 (*.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 2 t) (+.f64 1 t))) (/.f64 (*.f64 2 t) (+.f64 1 t))) 2)): 0 points increase in error, 3 points decrease in error
   (/.f64 (+.f64 1 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))) (Rewrite<= +-commutative_binary64 (+.f64 2 (*.f64 (/.f64 (*.f64 2 t) (+.f64 1 t)) (/.f64 (*.f64 2 t) (+.f64 1 t)))))): 0 points increase in error, 0 points decrease in error

3. Applied egg-rr 0.0

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

4. Final simplification 0.0

   \[\leadsto {\left(\frac{\mathsf{fma}\left(t, \frac{4}{\frac{1}{t} + \left(t + 2\right)}, 2\right)}{\mathsf{fma}\left(t, \frac{4}{\frac{1}{t} + \left(t + 2\right)}, 1\right)}\right)}^{-1} \]

Alternatives

Alternative 1
Error	0.0
Cost	14272

\[\begin{array}{l} t_1 := \frac{4}{t + \left(\frac{1}{t} + 2\right)}\\ \frac{\mathsf{fma}\left(t, t_1, 1\right)}{\mathsf{fma}\left(t, t_1, 2\right)} \end{array} \]

Alternative 2
Error	0.2
Cost	2248

\[\begin{array}{l} t_1 := \frac{t \cdot 2}{t + 1}\\ t_2 := \frac{\frac{4 \cdot \left(t \cdot t\right)}{t + 1}}{t + 1}\\ \mathbf{if}\;t \leq -6.257038870668207 \cdot 10^{+157}:\\ \;\;\;\;0.8333333333333334\\ \mathbf{elif}\;t \leq 50553502.742709085:\\ \;\;\;\;\frac{1 + t_2}{2 + t_2}\\ \mathbf{else}:\\ \;\;\;\;\frac{5 + \frac{-8}{t}}{2 + t_1 \cdot t_1}\\ \end{array} \]

Alternative 3
Error	0.1
Cost	2240

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

Alternative 4
Error	0.8
Cost	1864

\[\begin{array}{l} t_1 := 0.8333333333333334 + \frac{-0.2222222222222222}{t}\\ \mathbf{if}\;t \leq -1043110319886.8457:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 0.3917278794254961:\\ \;\;\;\;\frac{1 + \left(t \cdot 2\right) \cdot \left(t \cdot \left(2 + t \cdot \left(t \cdot 2 + -2\right)\right)\right)}{2 + 4 \cdot \left(t \cdot t\right)}\\ \mathbf{else}:\\ \;\;\;\;t_1 + \frac{\frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\ \end{array} \]

Alternative 5
Error	0.8
Cost	1480

\[\begin{array}{l} t_1 := 4 \cdot \left(t \cdot t\right)\\ t_2 := 0.8333333333333334 + \frac{-0.2222222222222222}{t}\\ \mathbf{if}\;t \leq -1043110319886.8457:\\ \;\;\;\;t_2\\ \mathbf{elif}\;t \leq 0.3917278794254961:\\ \;\;\;\;\frac{1 + \frac{t_1}{t + 1}}{2 + t_1}\\ \mathbf{else}:\\ \;\;\;\;t_2 + \frac{\frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\ \end{array} \]

Alternative 6
Error	0.8
Cost	1224

\[\begin{array}{l} t_1 := 0.8333333333333334 + \frac{-0.2222222222222222}{t}\\ \mathbf{if}\;t \leq -1043110319886.8457:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 0.3917278794254961:\\ \;\;\;\;\frac{1 + t \cdot \left(t \cdot 4\right)}{2 + 4 \cdot \left(t \cdot t\right)}\\ \mathbf{else}:\\ \;\;\;\;t_1 - \frac{-0.037037037037037035}{t \cdot t}\\ \end{array} \]

Alternative 7
Error	0.8
Cost	1224

\[\begin{array}{l} t_1 := 0.8333333333333334 + \frac{-0.2222222222222222}{t}\\ \mathbf{if}\;t \leq -1043110319886.8457:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 0.3917278794254961:\\ \;\;\;\;\frac{1 + t \cdot \left(t \cdot 4\right)}{2 + 4 \cdot \left(t \cdot t\right)}\\ \mathbf{else}:\\ \;\;\;\;t_1 + \frac{\frac{\frac{0.04938271604938271}{t} + 0.037037037037037035}{t}}{t}\\ \end{array} \]

Alternative 8
Error	1.4
Cost	968

\[\begin{array}{l} t_1 := 0.8333333333333334 + \frac{-0.2222222222222222}{t}\\ \mathbf{if}\;t \leq -1043110319886.8457:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 2.5988283996482075 \cdot 10^{-12}:\\ \;\;\;\;0.5\\ \mathbf{else}:\\ \;\;\;\;t_1 - \frac{-0.037037037037037035}{t \cdot t}\\ \end{array} \]

Alternative 9
Error	1.0
Cost	584

\[\begin{array}{l} t_1 := 0.8333333333333334 + \frac{-0.2222222222222222}{t}\\ \mathbf{if}\;t \leq -1043110319886.8457:\\ \;\;\;\;t_1\\ \mathbf{elif}\;t \leq 0.3917278794254961:\\ \;\;\;\;0.5\\ \mathbf{else}:\\ \;\;\;\;t_1\\ \end{array} \]

Alternative 10
Error	1.2
Cost	328

\[\begin{array}{l} \mathbf{if}\;t \leq -1043110319886.8457:\\ \;\;\;\;0.8333333333333334\\ \mathbf{elif}\;t \leq 0.3917278794254961:\\ \;\;\;\;0.5\\ \mathbf{else}:\\ \;\;\;\;0.8333333333333334\\ \end{array} \]

Alternative 11
Error	25.9
Cost	64

\[0.5 \]

Reproduce

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