Kahan p13 Example 1

Average Error: 0.0 → 0.0

Time: 13.6s

Precision: binary64

Cost: 14272

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}{t + \left(2 + \frac{1}{t}\right)}\\ \frac{\mathsf{fma}\left(t, t_1, 1\right)}{\mathsf{fma}\left(t, t_1, 2\right)} \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 (+ t (+ 2.0 (/ 1.0 t))))))
   (/ (fma t t_1 1.0) (fma t t_1 2.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 / (t + (2.0 + (1.0 / t)));
	return fma(t, t_1, 1.0) / fma(t, t_1, 2.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(t + Float64(2.0 + Float64(1.0 / t))))
	return Float64(fma(t, t_1, 1.0) / fma(t, t_1, 2.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[(t + N[(2.0 + N[(1.0 / t), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, N[(N[(t * t$95$1 + 1.0), $MachinePrecision] / N[(t * t$95$1 + 2.0), $MachinePrecision]), $MachinePrecision]]

Derivation

1. Initial program 0.0

   \[\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)): 1 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)): 58 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, 58 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)): 0 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)): 1 points increase in error, 1 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, 0 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)): 0 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)): 1 points increase in error, 0 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)): 1 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)): 1 points increase in error, 0 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, 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 (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)): 58 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)): 0 points increase in error, 58 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, 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) 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, 1 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))): 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<= *-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)): 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)))) (+.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, 1 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, 1 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. Final simplification 0.0

   \[\leadsto \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)} \]

Alternatives

Alternative 1
Error	0.3
Cost	2248

\[\begin{array}{l} t_1 := \frac{\frac{4 \cdot \left(t \cdot t\right)}{t + 1}}{t + 1}\\ \mathbf{if}\;t \leq -9.074208612972171 \cdot 10^{+154}:\\ \;\;\;\;0.8333333333333334\\ \mathbf{elif}\;t \leq 1310.8664380979144:\\ \;\;\;\;\frac{1 + t_1}{2 + t_1}\\ \mathbf{else}:\\ \;\;\;\;0.8333333333333334\\ \end{array} \]

Alternative 2
Error	0.0
Cost	2240

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

Alternative 3
Error	0.7
Cost	1480

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

Alternative 4
Error	0.7
Cost	1224

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

Alternative 5
Error	0.8
Cost	840

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

Alternative 6
Error	0.9
Cost	584

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

Alternative 7
Error	1.2
Cost	328

\[\begin{array}{l} \mathbf{if}\;t \leq -1.8598140530148706:\\ \;\;\;\;0.8333333333333334\\ \mathbf{elif}\;t \leq 2.2387804098994057 \cdot 10^{-11}:\\ \;\;\;\;0.5\\ \mathbf{else}:\\ \;\;\;\;0.8333333333333334\\ \end{array} \]

Alternative 8
Error	26.0
Cost	64

\[0.5 \]

Reproduce

herbie shell --seed 2022317 
(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))))))