?

Average Error: 37.1 → 0.3
Time: 22.5s
Precision: binary64
Cost: 163208

?

\[\tan \left(x + \varepsilon\right) - \tan x \]
↓
\[\begin{array}{l} t_0 := \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ t_1 := \frac{\sin x}{\cos x}\\ t_2 := 1 - \frac{\tan x}{\frac{1}{\tan \varepsilon}}\\ t_3 := \tan x + \tan \varepsilon\\ t_4 := \frac{{\sin x}^{3}}{{\cos x}^{3}}\\ \mathbf{if}\;\varepsilon \leq -5.8 \cdot 10^{-5}:\\ \;\;\;\;\frac{t_3}{t_2} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 1.1 \cdot 10^{-6}:\\ \;\;\;\;\mathsf{fma}\left(t_1 + t_4, \varepsilon \cdot \varepsilon, \mathsf{fma}\left({\varepsilon}^{3}, t_0 + \left(0.3333333333333333 - \frac{\sin x}{\frac{\cos x}{t_1 \cdot -0.3333333333333333 - t_4}}\right), \varepsilon + \varepsilon \cdot t_0\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t_3, \frac{1}{t_2}, -\tan x\right)\\ \end{array} \]
(FPCore (x eps) :precision binary64 (- (tan (+ x eps)) (tan x)))
↓
(FPCore (x eps)
 :precision binary64
 (let* ((t_0 (/ (pow (sin x) 2.0) (pow (cos x) 2.0)))
        (t_1 (/ (sin x) (cos x)))
        (t_2 (- 1.0 (/ (tan x) (/ 1.0 (tan eps)))))
        (t_3 (+ (tan x) (tan eps)))
        (t_4 (/ (pow (sin x) 3.0) (pow (cos x) 3.0))))
   (if (<= eps -5.8e-5)
     (- (/ t_3 t_2) (tan x))
     (if (<= eps 1.1e-6)
       (fma
        (+ t_1 t_4)
        (* eps eps)
        (fma
         (pow eps 3.0)
         (+
          t_0
          (-
           0.3333333333333333
           (/ (sin x) (/ (cos x) (- (* t_1 -0.3333333333333333) t_4)))))
         (+ eps (* eps t_0))))
       (fma t_3 (/ 1.0 t_2) (- (tan x)))))))
double code(double x, double eps) {
	return tan((x + eps)) - tan(x);
}
↓
double code(double x, double eps) {
	double t_0 = pow(sin(x), 2.0) / pow(cos(x), 2.0);
	double t_1 = sin(x) / cos(x);
	double t_2 = 1.0 - (tan(x) / (1.0 / tan(eps)));
	double t_3 = tan(x) + tan(eps);
	double t_4 = pow(sin(x), 3.0) / pow(cos(x), 3.0);
	double tmp;
	if (eps <= -5.8e-5) {
		tmp = (t_3 / t_2) - tan(x);
	} else if (eps <= 1.1e-6) {
		tmp = fma((t_1 + t_4), (eps * eps), fma(pow(eps, 3.0), (t_0 + (0.3333333333333333 - (sin(x) / (cos(x) / ((t_1 * -0.3333333333333333) - t_4))))), (eps + (eps * t_0))));
	} else {
		tmp = fma(t_3, (1.0 / t_2), -tan(x));
	}
	return tmp;
}

function code(x, eps)
	return Float64(tan(Float64(x + eps)) - tan(x))
end
↓
function code(x, eps)
	t_0 = Float64((sin(x) ^ 2.0) / (cos(x) ^ 2.0))
	t_1 = Float64(sin(x) / cos(x))
	t_2 = Float64(1.0 - Float64(tan(x) / Float64(1.0 / tan(eps))))
	t_3 = Float64(tan(x) + tan(eps))
	t_4 = Float64((sin(x) ^ 3.0) / (cos(x) ^ 3.0))
	tmp = 0.0
	if (eps <= -5.8e-5)
		tmp = Float64(Float64(t_3 / t_2) - tan(x));
	elseif (eps <= 1.1e-6)
		tmp = fma(Float64(t_1 + t_4), Float64(eps * eps), fma((eps ^ 3.0), Float64(t_0 + Float64(0.3333333333333333 - Float64(sin(x) / Float64(cos(x) / Float64(Float64(t_1 * -0.3333333333333333) - t_4))))), Float64(eps + Float64(eps * t_0))));
	else
		tmp = fma(t_3, Float64(1.0 / t_2), Float64(-tan(x)));
	end
	return tmp
end

code[x_, eps_] := N[(N[Tan[N[(x + eps), $MachinePrecision]], $MachinePrecision] - N[Tan[x], $MachinePrecision]), $MachinePrecision]
↓
code[x_, eps_] := Block[{t$95$0 = N[(N[Power[N[Sin[x], $MachinePrecision], 2.0], $MachinePrecision] / N[Power[N[Cos[x], $MachinePrecision], 2.0], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$1 = N[(N[Sin[x], $MachinePrecision] / N[Cos[x], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$2 = N[(1.0 - N[(N[Tan[x], $MachinePrecision] / N[(1.0 / N[Tan[eps], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]}, Block[{t$95$3 = N[(N[Tan[x], $MachinePrecision] + N[Tan[eps], $MachinePrecision]), $MachinePrecision]}, Block[{t$95$4 = N[(N[Power[N[Sin[x], $MachinePrecision], 3.0], $MachinePrecision] / N[Power[N[Cos[x], $MachinePrecision], 3.0], $MachinePrecision]), $MachinePrecision]}, If[LessEqual[eps, -5.8e-5], N[(N[(t$95$3 / t$95$2), $MachinePrecision] - N[Tan[x], $MachinePrecision]), $MachinePrecision], If[LessEqual[eps, 1.1e-6], N[(N[(t$95$1 + t$95$4), $MachinePrecision] * N[(eps * eps), $MachinePrecision] + N[(N[Power[eps, 3.0], $MachinePrecision] * N[(t$95$0 + N[(0.3333333333333333 - N[(N[Sin[x], $MachinePrecision] / N[(N[Cos[x], $MachinePrecision] / N[(N[(t$95$1 * -0.3333333333333333), $MachinePrecision] - t$95$4), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision] + N[(eps + N[(eps * t$95$0), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision], N[(t$95$3 * N[(1.0 / t$95$2), $MachinePrecision] + (-N[Tan[x], $MachinePrecision])), $MachinePrecision]]]]]]]]

\tan \left(x + \varepsilon\right) - \tan x
↓
\begin{array}{l}
t_0 := \frac{{\sin x}^{2}}{{\cos x}^{2}}\\
t_1 := \frac{\sin x}{\cos x}\\
t_2 := 1 - \frac{\tan x}{\frac{1}{\tan \varepsilon}}\\
t_3 := \tan x + \tan \varepsilon\\
t_4 := \frac{{\sin x}^{3}}{{\cos x}^{3}}\\
\mathbf{if}\;\varepsilon \leq -5.8 \cdot 10^{-5}:\\
\;\;\;\;\frac{t_3}{t_2} - \tan x\\

\mathbf{elif}\;\varepsilon \leq 1.1 \cdot 10^{-6}:\\
\;\;\;\;\mathsf{fma}\left(t_1 + t_4, \varepsilon \cdot \varepsilon, \mathsf{fma}\left({\varepsilon}^{3}, t_0 + \left(0.3333333333333333 - \frac{\sin x}{\frac{\cos x}{t_1 \cdot -0.3333333333333333 - t_4}}\right), \varepsilon + \varepsilon \cdot t_0\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\mathsf{fma}\left(t_3, \frac{1}{t_2}, -\tan x\right)\\


\end{array}

Error?

Target

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

Derivation?

  1. Split input into 3 regimes

  2. if eps < -5.8e-5

    1. Initial program 30.0

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

    2. Applied egg-rr0.4

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

    3. Simplified0.4

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]
      Proof

      [Start]0.4

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

      *-commutative [<=]0.4

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

      associate-*l/ [=>]0.4

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

      *-lft-identity [=>]0.4

      \[ \frac{\color{blue}{\tan x + \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x \]

    4. Applied egg-rr0.4

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\tan x}{\frac{1}{\tan \varepsilon}}}} - \tan x \]

    if -5.8e-5 < eps < 1.1000000000000001e-6

    1. Initial program 44.4

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

    2. Applied egg-rr43.9

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

    3. Simplified43.9

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]
      Proof

      [Start]43.9

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

      *-commutative [<=]43.9

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

      associate-*l/ [=>]43.9

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

      *-lft-identity [=>]43.9

      \[ \frac{\color{blue}{\tan x + \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x \]

    4. Applied egg-rr43.9

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\tan x}{\frac{1}{\tan \varepsilon}}}} - \tan x \]

    5. Applied egg-rr43.9

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

    6. Taylor expanded in eps around 0 0.3

      \[\leadsto \color{blue}{\left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right) \cdot {\varepsilon}^{2} + \left(\varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + {\varepsilon}^{3} \cdot \left(0.3333333333333333 + \left(-1 \cdot \frac{\left(-1 \cdot \frac{{\sin x}^{3}}{{\cos x}^{3}} + -0.3333333333333333 \cdot \frac{\sin x}{\cos x}\right) \cdot \sin x}{\cos x} + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\right)\right)} \]

    7. Simplified0.2

      \[\leadsto \color{blue}{\mathsf{fma}\left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}, \varepsilon \cdot \varepsilon, \mathsf{fma}\left({\varepsilon}^{3}, \frac{{\sin x}^{2}}{{\cos x}^{2}} + \left(0.3333333333333333 - \frac{\sin x}{\frac{\cos x}{-0.3333333333333333 \cdot \frac{\sin x}{\cos x} - \frac{{\sin x}^{3}}{{\cos x}^{3}}}}\right), \varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\right)} \]
      Proof

      [Start]0.3

      \[ \left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right) \cdot {\varepsilon}^{2} + \left(\varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + {\varepsilon}^{3} \cdot \left(0.3333333333333333 + \left(-1 \cdot \frac{\left(-1 \cdot \frac{{\sin x}^{3}}{{\cos x}^{3}} + -0.3333333333333333 \cdot \frac{\sin x}{\cos x}\right) \cdot \sin x}{\cos x} + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\right)\right) \]

      fma-def [=>]0.3

      \[ \color{blue}{\mathsf{fma}\left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}, {\varepsilon}^{2}, \varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + {\varepsilon}^{3} \cdot \left(0.3333333333333333 + \left(-1 \cdot \frac{\left(-1 \cdot \frac{{\sin x}^{3}}{{\cos x}^{3}} + -0.3333333333333333 \cdot \frac{\sin x}{\cos x}\right) \cdot \sin x}{\cos x} + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\right)\right)} \]

      unpow2 [=>]0.3

      \[ \mathsf{fma}\left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}, \color{blue}{\varepsilon \cdot \varepsilon}, \varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + {\varepsilon}^{3} \cdot \left(0.3333333333333333 + \left(-1 \cdot \frac{\left(-1 \cdot \frac{{\sin x}^{3}}{{\cos x}^{3}} + -0.3333333333333333 \cdot \frac{\sin x}{\cos x}\right) \cdot \sin x}{\cos x} + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\right)\right) \]

      +-commutative [=>]0.3

      \[ \mathsf{fma}\left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}, \varepsilon \cdot \varepsilon, \color{blue}{{\varepsilon}^{3} \cdot \left(0.3333333333333333 + \left(-1 \cdot \frac{\left(-1 \cdot \frac{{\sin x}^{3}}{{\cos x}^{3}} + -0.3333333333333333 \cdot \frac{\sin x}{\cos x}\right) \cdot \sin x}{\cos x} + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\right) + \varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)}\right) \]

      fma-def [=>]0.3

      \[ \mathsf{fma}\left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}, \varepsilon \cdot \varepsilon, \color{blue}{\mathsf{fma}\left({\varepsilon}^{3}, 0.3333333333333333 + \left(-1 \cdot \frac{\left(-1 \cdot \frac{{\sin x}^{3}}{{\cos x}^{3}} + -0.3333333333333333 \cdot \frac{\sin x}{\cos x}\right) \cdot \sin x}{\cos x} + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right), \varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\right)}\right) \]

    if 1.1000000000000001e-6 < eps

    1. Initial program 30.1

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

    2. Applied egg-rr0.4

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

    3. Simplified0.4

      \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x \]
      Proof

      [Start]0.4

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

      *-commutative [<=]0.4

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

      associate-*l/ [=>]0.4

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

      *-lft-identity [=>]0.4

      \[ \frac{\color{blue}{\tan x + \tan \varepsilon}}{1 - \tan x \cdot \tan \varepsilon} - \tan x \]

    4. Applied egg-rr0.4

      \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\tan x}{\frac{1}{\tan \varepsilon}}}} - \tan x \]

    5. Applied egg-rr0.4

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

    6. Applied egg-rr0.4

      \[\leadsto \mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{1}{1 - \color{blue}{\frac{\tan x}{\frac{1}{\tan \varepsilon}}}}, -\tan x\right) \]
  3. Recombined 3 regimes into one program.

  4. Final simplification0.3

    \[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -5.8 \cdot 10^{-5}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\tan x}{\frac{1}{\tan \varepsilon}}} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 1.1 \cdot 10^{-6}:\\ \;\;\;\;\mathsf{fma}\left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}, \varepsilon \cdot \varepsilon, \mathsf{fma}\left({\varepsilon}^{3}, \frac{{\sin x}^{2}}{{\cos x}^{2}} + \left(0.3333333333333333 - \frac{\sin x}{\frac{\cos x}{\frac{\sin x}{\cos x} \cdot -0.3333333333333333 - \frac{{\sin x}^{3}}{{\cos x}^{3}}}}\right), \varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, \frac{1}{1 - \frac{\tan x}{\frac{1}{\tan \varepsilon}}}, -\tan x\right)\\ \end{array} \]

Alternatives

Alternative 1
Error0.3
Cost72008
\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ t_1 := 1 - \frac{\tan x}{\frac{1}{\tan \varepsilon}}\\ \mathbf{if}\;\varepsilon \leq -2.6 \cdot 10^{-7}:\\ \;\;\;\;\frac{t_0}{t_1} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 2.65 \cdot 10^{-7}:\\ \;\;\;\;\mathsf{fma}\left(\varepsilon, 1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}, \left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right) \cdot \left(\varepsilon \cdot \varepsilon\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t_0, \frac{1}{t_1}, -\tan x\right)\\ \end{array} \]
Alternative 2
Error0.3
Cost65736
\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ t_1 := 1 - \frac{\tan x}{\frac{1}{\tan \varepsilon}}\\ \mathbf{if}\;\varepsilon \leq -2.7 \cdot 10^{-7}:\\ \;\;\;\;\frac{t_0}{t_1} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 2.9 \cdot 10^{-7}:\\ \;\;\;\;\varepsilon \cdot \left(1 + \frac{{\sin x}^{2}}{{\cos x}^{2}}\right) + \left(\frac{\sin x}{\cos x} + \frac{{\sin x}^{3}}{{\cos x}^{3}}\right) \cdot \left(\varepsilon \cdot \varepsilon\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t_0, \frac{1}{t_1}, -\tan x\right)\\ \end{array} \]
Alternative 3
Error0.4
Cost39560
\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ t_1 := 1 - \frac{\tan x}{\frac{1}{\tan \varepsilon}}\\ \mathbf{if}\;\varepsilon \leq -3.1 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{t_1} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 5.2 \cdot 10^{-9}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(t_0, \frac{1}{t_1}, -\tan x\right)\\ \end{array} \]
Alternative 4
Error0.4
Cost39496
\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -5.5 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{1 - \frac{\tan x}{\frac{1}{\tan \varepsilon}}} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 5.2 \cdot 10^{-9}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;\frac{t_0}{1 - \frac{\sin \varepsilon}{\frac{\cos \varepsilon}{\tan x}}} - \tan x\\ \end{array} \]
Alternative 5
Error0.4
Cost33097
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -2.9 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 7.3 \cdot 10^{-9}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \frac{\tan x}{\frac{1}{\tan \varepsilon}}} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \end{array} \]
Alternative 6
Error0.4
Cost33096
\[\begin{array}{l} t_0 := \tan x + \tan \varepsilon\\ t_1 := 1 - \tan x \cdot \tan \varepsilon\\ \mathbf{if}\;\varepsilon \leq -2.8 \cdot 10^{-9}:\\ \;\;\;\;\frac{t_0}{t_1} - \tan x\\ \mathbf{elif}\;\varepsilon \leq 5.2 \cdot 10^{-9}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \mathbf{else}:\\ \;\;\;\;t_0 \cdot \frac{1}{t_1} - \tan x\\ \end{array} \]
Alternative 7
Error0.4
Cost32969
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -3.7 \cdot 10^{-9} \lor \neg \left(\varepsilon \leq 2.6 \cdot 10^{-9}\right):\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \end{array} \]
Alternative 8
Error14.6
Cost26441
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -2 \cdot 10^{-5} \lor \neg \left(\varepsilon \leq 1.1 \cdot 10^{-6}\right):\\ \;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, 1, -\tan x\right)\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}}\\ \end{array} \]
Alternative 9
Error14.6
Cost26249
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -2.4 \cdot 10^{-6} \lor \neg \left(\varepsilon \leq 8.4 \cdot 10^{-7}\right):\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon}\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\varepsilon, {\left(\frac{\sin x}{\cos x}\right)}^{2}, \varepsilon\right)\\ \end{array} \]
Alternative 10
Error14.6
Cost26249
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -2.8 \cdot 10^{-6} \lor \neg \left(\varepsilon \leq 1.05 \cdot 10^{-6}\right):\\ \;\;\;\;\mathsf{fma}\left(\tan x + \tan \varepsilon, 1, -\tan x\right)\\ \mathbf{else}:\\ \;\;\;\;\mathsf{fma}\left(\varepsilon, {\left(\frac{\sin x}{\cos x}\right)}^{2}, \varepsilon\right)\\ \end{array} \]
Alternative 11
Error14.7
Cost19977
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -1.02 \cdot 10^{-6} \lor \neg \left(\varepsilon \leq 7.4 \cdot 10^{-7}\right):\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon}\\ \mathbf{else}:\\ \;\;\;\;\varepsilon \cdot \left(1 + {\left(\frac{\sin x}{\cos x}\right)}^{2}\right)\\ \end{array} \]
Alternative 12
Error14.7
Cost19977
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -7.2 \cdot 10^{-6} \lor \neg \left(\varepsilon \leq 1.06 \cdot 10^{-6}\right):\\ \;\;\;\;\frac{\sin \varepsilon}{\cos \varepsilon}\\ \mathbf{else}:\\ \;\;\;\;\varepsilon + \varepsilon \cdot {\left(\frac{\sin x}{\cos x}\right)}^{2}\\ \end{array} \]
Alternative 13
Error27.4
Cost13257
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -3850 \lor \neg \left(\varepsilon \leq 1.08 \cdot 10^{-7}\right):\\ \;\;\;\;\tan \varepsilon - \tan x\\ \mathbf{else}:\\ \;\;\;\;\varepsilon\\ \end{array} \]
Alternative 14
Error27.2
Cost12992
\[\frac{\sin \varepsilon}{\cos \varepsilon} \]
Alternative 15
Error29.2
Cost7240
\[\begin{array}{l} t_0 := \tan \left(\varepsilon + x\right) - x\\ \mathbf{if}\;\varepsilon \leq -3850:\\ \;\;\;\;t_0\\ \mathbf{elif}\;\varepsilon \leq 3.1 \cdot 10^{-7}:\\ \;\;\;\;\varepsilon\\ \mathbf{else}:\\ \;\;\;\;x + \left(t_0 - x\right)\\ \end{array} \]
Alternative 16
Error29.2
Cost6985
\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -3850 \lor \neg \left(\varepsilon \leq 2.1 \cdot 10^{-7}\right):\\ \;\;\;\;\tan \left(\varepsilon + x\right) - x\\ \mathbf{else}:\\ \;\;\;\;\varepsilon\\ \end{array} \]
Alternative 17
Error44.2
Cost64
\[\varepsilon \]

Error

Reproduce?

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