Average Error: 37.4 → 0.3
Time: 15.3s
Precision: binary64
Cost: 52032
\[\tan \left(x + \varepsilon\right) - \tan x \]
↓
\[\tan x \cdot \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, \frac{\tan \varepsilon}{\tan x}\right)}{1 - \tan x \cdot \tan \varepsilon} \]
(FPCore (x eps) :precision binary64 (- (tan (+ x eps)) (tan x)))
↓
(FPCore (x eps)
 :precision binary64
 (*
  (tan x)
  (/
   (fma (tan x) (tan eps) (/ (tan eps) (tan x)))
   (- 1.0 (* (tan x) (tan eps))))))
double code(double x, double eps) {
	return tan((x + eps)) - tan(x);
}
↓
double code(double x, double eps) {
	return tan(x) * (fma(tan(x), tan(eps), (tan(eps) / tan(x))) / (1.0 - (tan(x) * tan(eps))));
}

function code(x, eps)
	return Float64(tan(Float64(x + eps)) - tan(x))
end
↓
function code(x, eps)
	return Float64(tan(x) * Float64(fma(tan(x), tan(eps), Float64(tan(eps) / tan(x))) / Float64(1.0 - Float64(tan(x) * tan(eps)))))
end

code[x_, eps_] := N[(N[Tan[N[(x + eps), $MachinePrecision]], $MachinePrecision] - N[Tan[x], $MachinePrecision]), $MachinePrecision]
↓
code[x_, eps_] := N[(N[Tan[x], $MachinePrecision] * N[(N[(N[Tan[x], $MachinePrecision] * N[Tan[eps], $MachinePrecision] + N[(N[Tan[eps], $MachinePrecision] / N[Tan[x], $MachinePrecision]), $MachinePrecision]), $MachinePrecision] / N[(1.0 - N[(N[Tan[x], $MachinePrecision] * N[Tan[eps], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]

\tan \left(x + \varepsilon\right) - \tan x
↓
\tan x \cdot \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, \frac{\tan \varepsilon}{\tan x}\right)}{1 - \tan x \cdot \tan \varepsilon}

Error

Target

Original37.4
Target15.6
Herbie0.3
\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)} \]

Derivation

  1. Initial program 37.4

    \[\tan \left(x + \varepsilon\right) - \tan x \]

  2. Applied egg-rr37.4

    \[\leadsto \color{blue}{\mathsf{fma}\left(\tan \left(x + \varepsilon\right), 1, -\frac{1}{\cos x} \cdot \sin x\right) + \mathsf{fma}\left(-\frac{1}{\cos x}, \sin x, \frac{1}{\cos x} \cdot \sin x\right)} \]

  3. Simplified37.4

    \[\leadsto \color{blue}{\tan \left(x + \varepsilon\right) - \frac{\sin x}{\cos x}} \]
    Proof
    (-.f64 (tan.f64 (+.f64 x eps)) (/.f64 (sin.f64 x) (cos.f64 x))): 0 points increase in error, 0 points decrease in error
    (-.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (tan.f64 (+.f64 x eps)))) (/.f64 (sin.f64 x) (cos.f64 x))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 1 (tan.f64 (+.f64 x eps))) (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (sin.f64 x))) (cos.f64 x))): 0 points increase in error, 0 points decrease in error
    (-.f64 (*.f64 1 (tan.f64 (+.f64 x eps))) (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))): 25 points increase in error, 16 points decrease in error
    (Rewrite=> fma-neg_binary64 (fma.f64 1 (tan.f64 (+.f64 x eps)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))): 0 points increase in error, 0 points decrease in error
    (Rewrite<= +-lft-identity_binary64 (+.f64 0 (fma.f64 1 (tan.f64 (+.f64 x eps)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite<= +-inverses_binary64 (-.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)) (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))) (fma.f64 1 (tan.f64 (+.f64 x eps)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))) (fma.f64 1 (tan.f64 (+.f64 x eps)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))) (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))) (fma.f64 1 (tan.f64 (+.f64 x eps)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (Rewrite=> distribute-lft-neg-in_binary64 (*.f64 (neg.f64 (/.f64 1 (cos.f64 x))) (sin.f64 x))) (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))) (fma.f64 1 (tan.f64 (+.f64 x eps)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite<= fma-udef_binary64 (fma.f64 (neg.f64 (/.f64 1 (cos.f64 x))) (sin.f64 x) (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))) (fma.f64 1 (tan.f64 (+.f64 x eps)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))): 44 points increase in error, 46 points decrease in error
    (Rewrite<= +-commutative_binary64 (+.f64 (fma.f64 1 (tan.f64 (+.f64 x eps)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))) (fma.f64 (neg.f64 (/.f64 1 (cos.f64 x))) (sin.f64 x) (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite=> fma-udef_binary64 (+.f64 (*.f64 1 (tan.f64 (+.f64 x eps))) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))) (fma.f64 (neg.f64 (/.f64 1 (cos.f64 x))) (sin.f64 x) (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (tan.f64 (+.f64 x eps)) 1)) (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))) (fma.f64 (neg.f64 (/.f64 1 (cos.f64 x))) (sin.f64 x) (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))): 0 points increase in error, 0 points decrease in error
    (+.f64 (Rewrite<= fma-udef_binary64 (fma.f64 (tan.f64 (+.f64 x eps)) 1 (neg.f64 (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x))))) (fma.f64 (neg.f64 (/.f64 1 (cos.f64 x))) (sin.f64 x) (*.f64 (/.f64 1 (cos.f64 x)) (sin.f64 x)))): 0 points increase in error, 0 points decrease in error

  4. Applied egg-rr21.9

    \[\leadsto \color{blue}{\frac{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{\tan x} - \left(1 - \tan x \cdot \tan \varepsilon\right) \cdot 1}{\left(1 - \tan x \cdot \tan \varepsilon\right) \cdot \frac{1}{\tan x}}} \]

  5. Simplified19.6

    \[\leadsto \color{blue}{\frac{\left(\frac{\tan x + \tan \varepsilon}{\tan x} - 1\right) + \tan x \cdot \tan \varepsilon}{\frac{1 - \tan x \cdot \tan \varepsilon}{\tan x}}} \]
    Proof
    (/.f64 (+.f64 (-.f64 (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)) 1) (*.f64 (tan.f64 x) (tan.f64 eps))) (/.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))): 0 points increase in error, 0 points decrease in error
    (/.f64 (+.f64 (-.f64 (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) 1)) (tan.f64 x)) 1) (*.f64 (tan.f64 x) (tan.f64 eps))) (/.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))): 0 points increase in error, 0 points decrease in error
    (/.f64 (+.f64 (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (/.f64 1 (tan.f64 x)))) 1) (*.f64 (tan.f64 x) (tan.f64 eps))) (/.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))): 24 points increase in error, 26 points decrease in error
    (/.f64 (Rewrite<= associate--r-_binary64 (-.f64 (*.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (/.f64 1 (tan.f64 x))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))) (/.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))): 67 points increase in error, 6 points decrease in error
    (/.f64 (-.f64 (*.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (/.f64 1 (tan.f64 x))) (Rewrite<= *-rgt-identity_binary64 (*.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) 1))) (/.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))): 0 points increase in error, 0 points decrease in error
    (/.f64 (-.f64 (*.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (/.f64 1 (tan.f64 x))) (*.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) 1)) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) 1)) (tan.f64 x))): 0 points increase in error, 0 points decrease in error
    (/.f64 (-.f64 (*.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (/.f64 1 (tan.f64 x))) (*.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) 1)) (Rewrite<= associate-*r/_binary64 (*.f64 (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))) (/.f64 1 (tan.f64 x))))): 9 points increase in error, 8 points decrease in error

  6. Applied egg-rr39.5

    \[\leadsto \color{blue}{e^{\mathsf{log1p}\left(\tan x \cdot \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, \frac{\tan x + \tan \varepsilon}{\tan x} + -1\right)}{1 - \tan x \cdot \tan \varepsilon}\right)} - 1} \]

  7. Simplified19.6

    \[\leadsto \color{blue}{\mathsf{fma}\left(\tan x, \tan \varepsilon, \frac{\tan x + \tan \varepsilon}{\tan x} + -1\right) \cdot \frac{\tan x}{1 - \tan x \cdot \tan \varepsilon}} \]
    Proof
    (*.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)) -1)) (/.f64 (tan.f64 x) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 0 points increase in error, 0 points decrease in error
    (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (tan.f64 x) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps)))) (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)) -1)))): 0 points increase in error, 0 points decrease in error
    (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (tan.f64 x) (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)) -1))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 8 points increase in error, 14 points decrease in error
    (Rewrite<= associate-*r/_binary64 (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)) -1)) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps)))))): 12 points increase in error, 7 points decrease in error
    (Rewrite<= expm1-log1p_binary64 (expm1.f64 (log1p.f64 (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)) -1)) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps)))))))): 59 points increase in error, 3 points decrease in error
    (Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (log1p.f64 (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)) -1)) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))))) 1)): 141 points increase in error, 10 points decrease in error

  8. Applied egg-rr21.8

    \[\leadsto \color{blue}{0 + \left(\mathsf{fma}\left(\tan x, \tan \varepsilon, \frac{\tan x + \tan \varepsilon}{\tan x}\right) + -1\right) \cdot \frac{\tan x}{\mathsf{fma}\left(\tan \varepsilon, -\tan x, 1\right)}} \]

  9. Simplified0.3

    \[\leadsto \color{blue}{\tan x \cdot \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, \frac{\tan \varepsilon}{\tan x}\right)}{1 - \tan x \cdot \tan \varepsilon}} \]
    Proof
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (tan.f64 eps) (tan.f64 x))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (tan.f64 eps) 1)) (tan.f64 x))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (Rewrite<= associate-*r/_binary64 (*.f64 (tan.f64 eps) (/.f64 1 (tan.f64 x))))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 43 points increase in error, 8 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (Rewrite<= +-lft-identity_binary64 (+.f64 0 (*.f64 (tan.f64 eps) (/.f64 1 (tan.f64 x)))))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) (*.f64 (tan.f64 eps) (/.f64 1 (tan.f64 x))))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (Rewrite<= associate-+r+_binary64 (+.f64 -1 (+.f64 1 (*.f64 (tan.f64 eps) (/.f64 1 (tan.f64 x))))))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 98 points increase in error, 4 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 -1 (+.f64 (Rewrite<= rgt-mult-inverse_binary64 (*.f64 (tan.f64 x) (/.f64 1 (tan.f64 x)))) (*.f64 (tan.f64 eps) (/.f64 1 (tan.f64 x)))))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 11 points increase in error, 1 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 -1 (Rewrite<= distribute-rgt-in_binary64 (*.f64 (/.f64 1 (tan.f64 x)) (+.f64 (tan.f64 x) (tan.f64 eps)))))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 12 points increase in error, 6 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 -1 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 (+.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x))))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 4 points increase in error, 49 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (+.f64 -1 (/.f64 (Rewrite=> *-lft-identity_binary64 (+.f64 (tan.f64 x) (tan.f64 eps))) (tan.f64 x)))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)) -1))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (tan.f64 x) (tan.f64 eps)) (+.f64 (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)) -1))) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 2 points increase in error, 3 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 (tan.f64 x) (tan.f64 eps)) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1)) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 75 points increase in error, 6 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (+.f64 (Rewrite<= fma-udef_binary64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x)))) -1) (-.f64 1 (*.f64 (tan.f64 x) (tan.f64 eps))))): 5 points increase in error, 1 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (+.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1) (Rewrite<= unsub-neg_binary64 (+.f64 1 (neg.f64 (*.f64 (tan.f64 x) (tan.f64 eps))))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (+.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1) (+.f64 1 (neg.f64 (Rewrite=> *-commutative_binary64 (*.f64 (tan.f64 eps) (tan.f64 x))))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (+.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1) (+.f64 1 (Rewrite<= distribute-rgt-neg-out_binary64 (*.f64 (tan.f64 eps) (neg.f64 (tan.f64 x))))))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (+.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (tan.f64 eps) (neg.f64 (tan.f64 x))) 1)))): 0 points increase in error, 0 points decrease in error
    (*.f64 (tan.f64 x) (/.f64 (+.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1) (Rewrite<= fma-udef_binary64 (fma.f64 (tan.f64 eps) (neg.f64 (tan.f64 x)) 1)))): 5 points increase in error, 1 points decrease in error
    (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (+.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1) (fma.f64 (tan.f64 eps) (neg.f64 (tan.f64 x)) 1)) (tan.f64 x))): 0 points increase in error, 0 points decrease in error
    (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (+.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1) (tan.f64 x)) (fma.f64 (tan.f64 eps) (neg.f64 (tan.f64 x)) 1))): 6 points increase in error, 8 points decrease in error
    (Rewrite<= associate-*r/_binary64 (*.f64 (+.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1) (/.f64 (tan.f64 x) (fma.f64 (tan.f64 eps) (neg.f64 (tan.f64 x)) 1)))): 10 points increase in error, 9 points decrease in error
    (Rewrite<= +-lft-identity_binary64 (+.f64 0 (*.f64 (+.f64 (fma.f64 (tan.f64 x) (tan.f64 eps) (/.f64 (+.f64 (tan.f64 x) (tan.f64 eps)) (tan.f64 x))) -1) (/.f64 (tan.f64 x) (fma.f64 (tan.f64 eps) (neg.f64 (tan.f64 x)) 1))))): 0 points increase in error, 0 points decrease in error

  10. Final simplification0.3

    \[\leadsto \tan x \cdot \frac{\mathsf{fma}\left(\tan x, \tan \varepsilon, \frac{\tan \varepsilon}{\tan x}\right)}{1 - \tan x \cdot \tan \varepsilon} \]

Alternatives

Alternative 1
Error19.6
Cost46016
\[\begin{array}{l} t_0 := \tan x \cdot \tan \varepsilon\\ \frac{t_0 + \left(-1 + \left(\frac{\tan \varepsilon}{\tan x} + 1\right)\right)}{\frac{1 - t_0}{\tan x}} \end{array} \]
Alternative 2
Error19.6
Cost45888
\[\frac{\tan x \cdot \tan \varepsilon + \left(-1 + \frac{\tan x + \tan \varepsilon}{\tan x}\right)}{\frac{1}{\tan x} - \tan \varepsilon} \]
Alternative 3
Error21.7
Cost32704
\[\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x \]
Alternative 4
Error37.4
Cost19712
\[\tan \left(x + \varepsilon\right) - {\left(\frac{1}{\tan x}\right)}^{-1} \]
Alternative 5
Error37.4
Cost13120
\[\tan \left(x + \varepsilon\right) - \tan x \]

Error

Reproduce

herbie shell --seed 2022334 
(FPCore (x eps)
  :name "2tan (problem 3.3.2)"
  :precision binary64

  :herbie-target
  (/ (sin eps) (* (cos x) (cos (+ x eps))))

  (- (tan (+ x eps)) (tan x)))