Average Error: 37.5 → 0.3

Time: 38.5s

Precision: binary64

Cost: 131009

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

↓

\[\begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.1505143183695406 \cdot 10^{-05}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - {\left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}^{3}} \cdot \left(1 + \left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x} + \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)\right) - \tan x\\ \mathbf{elif}\;\varepsilon \leq 4.7921130663532265 \cdot 10^{-05}:\\ \;\;\;\;\left(\varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}} + 1.3333333333333333 \cdot \left(\frac{{\sin x}^{2}}{{\cos x}^{2}} \cdot {\varepsilon}^{3}\right)\right) + \left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(\frac{{\sin x}^{4}}{{\cos x}^{4}} + 0.3333333333333333\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + {\left(\frac{\sin x}{\cos x}\right)}^{3}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]

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

↓

\begin{array}{l}
\mathbf{if}\;\varepsilon \leq -4.1505143183695406 \cdot 10^{-05}:\\
\;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - {\left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}^{3}} \cdot \left(1 + \left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x} + \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)\right) - \tan x\\

\mathbf{elif}\;\varepsilon \leq 4.7921130663532265 \cdot 10^{-05}:\\
\;\;\;\;\left(\varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}} + 1.3333333333333333 \cdot \left(\frac{{\sin x}^{2}}{{\cos x}^{2}} \cdot {\varepsilon}^{3}\right)\right) + \left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(\frac{{\sin x}^{4}}{{\cos x}^{4}} + 0.3333333333333333\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + {\left(\frac{\sin x}{\cos x}\right)}^{3}\right)\right)\\

\mathbf{else}:\\
\;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\

\end{array}

(FPCore (x eps) :precision binary64 (- (tan (+ x eps)) (tan x)))

↓

(FPCore (x eps)
 :precision binary64
 (if (<= eps -4.1505143183695406e-05)
   (-
    (*
     (/
      (+ (tan x) (tan eps))
      (- 1.0 (pow (/ (* (sin eps) (sin x)) (* (cos eps) (cos x))) 3.0)))
     (+
      1.0
      (+
       (/ (* (sin eps) (sin x)) (* (cos eps) (cos x)))
       (*
        (/ (* (sin eps) (sin x)) (* (cos eps) (cos x)))
        (/ (* (sin eps) (sin x)) (* (cos eps) (cos x)))))))
    (tan x))
   (if (<= eps 4.7921130663532265e-05)
     (+
      (+
       (* eps (/ (pow (sin x) 2.0) (pow (cos x) 2.0)))
       (*
        1.3333333333333333
        (* (/ (pow (sin x) 2.0) (pow (cos x) 2.0)) (pow eps 3.0))))
      (+
       (+
        eps
        (*
         (pow eps 3.0)
         (+ (/ (pow (sin x) 4.0) (pow (cos x) 4.0)) 0.3333333333333333)))
       (* (* eps eps) (+ (/ (sin x) (cos x)) (pow (/ (sin x) (cos x)) 3.0)))))
     (-
      (* (+ (tan x) (tan eps)) (/ 1.0 (- 1.0 (* (tan x) (tan eps)))))
      (tan x)))))

double code(double x, double eps) {
	return tan(x + eps) - tan(x);
}

↓

double code(double x, double eps) {
	double tmp;
	if (eps <= -4.1505143183695406e-05) {
		tmp = (((tan(x) + tan(eps)) / (1.0 - pow(((sin(eps) * sin(x)) / (cos(eps) * cos(x))), 3.0))) * (1.0 + (((sin(eps) * sin(x)) / (cos(eps) * cos(x))) + (((sin(eps) * sin(x)) / (cos(eps) * cos(x))) * ((sin(eps) * sin(x)) / (cos(eps) * cos(x))))))) - tan(x);
	} else if (eps <= 4.7921130663532265e-05) {
		tmp = ((eps * (pow(sin(x), 2.0) / pow(cos(x), 2.0))) + (1.3333333333333333 * ((pow(sin(x), 2.0) / pow(cos(x), 2.0)) * pow(eps, 3.0)))) + ((eps + (pow(eps, 3.0) * ((pow(sin(x), 4.0) / pow(cos(x), 4.0)) + 0.3333333333333333))) + ((eps * eps) * ((sin(x) / cos(x)) + pow((sin(x) / cos(x)), 3.0))));
	} else {
		tmp = ((tan(x) + tan(eps)) * (1.0 / (1.0 - (tan(x) * tan(eps))))) - tan(x);
	}
	return tmp;
}

Error

The X axis uses an exponential scale — Bits error versus `x`

Try it out

In
Out

Enter valid numbers for all inputs

Target

Original	37.5
Target	14.6
Herbie	0.3

\[\frac{\sin \varepsilon}{\cos x \cdot \cos \left(x + \varepsilon\right)}\]

Alternatives

Alternative 1
Error	23.0
Cost	229184

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

Alternative 2
Error	24.8
Cost	215744

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

Alternative 3
Error	23.5
Cost	156608

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

Alternative 4
Error	22.8
Cost	130688

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

Alternative 5
Error	31.1
Cost	124416

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

Alternative 6
Error	23.9
Cost	123584

\[\frac{\sqrt[3]{\tan x + \tan \varepsilon} \cdot \sqrt[3]{\tan x + \tan \varepsilon}}{\sqrt[3]{1 - \tan x \cdot \tan \varepsilon} \cdot \sqrt[3]{1 - \tan x \cdot \tan \varepsilon}} \cdot \frac{\sqrt[3]{\tan x + \tan \varepsilon}}{\sqrt[3]{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]

Alternative 7
Error	31.1
Cost	117952

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

Alternative 8
Error	26.6
Cost	117696

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

Alternative 9
Error	23.5
Cost	117440

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

Alternative 10
Error	24.7
Cost	98240

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

Alternative 11
Error	39.2
Cost	85056

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

Alternative 12
Error	22.8
Cost	78464

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

Alternative 13
Error	31.9
Cost	78400

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

Alternative 14
Error	43.0
Cost	78272

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

Alternative 15
Error	22.9
Cost	78016

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

Alternative 16
Error	23.8
Cost	78016

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

Alternative 17
Error	31.0
Cost	65728

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

Alternative 18
Error	22.9
Cost	64960

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

Alternative 19
Error	31.1
Cost	59008

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

Alternative 20
Error	31.0
Cost	59008

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

Alternative 21
Error	41.3
Cost	58944

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

Alternative 22
Error	22.9
Cost	58944

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

Alternative 23
Error	22.8
Cost	58944

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

Alternative 24
Error	23.0
Cost	58816

\[\frac{\frac{\sin \varepsilon}{\cos \varepsilon} + \frac{\sin x}{\cos x}}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}} - \tan x\]

Alternative 25
Error	26.6
Cost	58816

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

Alternative 26
Error	38.0
Cost	58688

\[\sqrt[3]{\tan \left(\varepsilon + x\right) - \tan x} \cdot \left(\sqrt[3]{\tan \left(\varepsilon + x\right) - \tan x} \cdot \sqrt[3]{\tan \left(\varepsilon + x\right) - \tan x}\right)\]

Alternative 27
Error	26.6
Cost	58688

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

Alternative 28
Error	43.8
Cost	58560

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

Alternative 29
Error	22.9
Cost	51840

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

Alternative 30
Error	22.8
Cost	45760

\[\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}} - \tan x\]

Alternative 31
Error	23.0
Cost	45760

\[\frac{\frac{\sin \varepsilon}{\cos \varepsilon} + \frac{\sin x}{\cos x}}{1 - \tan x \cdot \tan \varepsilon} - \tan x\]

Alternative 32
Error	38.9
Cost	45760

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

Alternative 33
Error	38.2
Cost	45632

\[\sqrt[3]{\tan \left(\varepsilon + x\right)} \cdot \left(\sqrt[3]{\tan \left(\varepsilon + x\right)} \cdot \sqrt[3]{\tan \left(\varepsilon + x\right)}\right) - \tan x\]

Alternative 34
Error	22.8
Cost	45568

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

Alternative 35
Error	26.7
Cost	45568

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

Alternative 36
Error	26.5
Cost	45568

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

Alternative 37
Error	30.5
Cost	45504

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

Alternative 38
Error	30.6
Cost	45504

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

Alternative 39
Error	43.8
Cost	45504

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

Alternative 40
Error	41.8
Cost	45504

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

Alternative 41
Error	43.2
Cost	45504

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

Alternative 42
Error	22.8
Cost	39232

\[\frac{\tan x + \tan \varepsilon}{1 - \frac{\sin \varepsilon \cdot \tan x}{\cos \varepsilon}} - \tan x\]

Alternative 43
Error	22.8
Cost	39232

\[\frac{\tan x + \tan \varepsilon}{1 - \frac{\tan \varepsilon \cdot \sin x}{\cos x}} - \tan x\]

Alternative 44
Error	30.0
Cost	39104

\[\frac{\sin \varepsilon}{\cos \varepsilon} + \frac{x \cdot {\sin \varepsilon}^{2}}{{\cos \varepsilon}^{2}}\]

Alternative 45
Error	22.8
Cost	32832

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

Alternative 46
Error	22.9
Cost	32832

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

Alternative 47
Error	22.8
Cost	32704

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

Alternative 48
Error	51.3
Cost	32576

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

Alternative 49
Error	30.7
Cost	26176

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

Alternative 50
Error	30.7
Cost	26176

\[\varepsilon + \frac{\varepsilon \cdot {\sin x}^{2}}{{\cos x}^{2}}\]

Alternative 51
Error	41.2
Cost	25984

\[\sqrt[3]{{\tan \left(\varepsilon + x\right)}^{3}} - \tan x\]

Alternative 52
Error	51.6
Cost	25920

\[e^{\log \tan \left(\varepsilon + x\right)} - \tan x\]

Alternative 53
Error	45.2
Cost	25920

\[\log \left(e^{\tan \left(\varepsilon + x\right)}\right) - \tan x\]

Alternative 54
Error	37.6
Cost	19776

\[\frac{\sin \left(\varepsilon + x\right)}{\cos \left(\varepsilon + x\right)} - \tan x\]

Alternative 55
Error	38.0
Cost	19520

\[\frac{\sin \varepsilon}{\cos \varepsilon} - \tan x\]

Alternative 56
Error	61.2
Cost	19520

\[\frac{\sin x}{\cos x} - \tan x\]

Alternative 57
Error	37.5
Cost	13120

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

Alternative 58
Error	27.2
Cost	12992

\[\frac{\sin \varepsilon}{\cos \varepsilon}\]

Alternative 59
Error	59.6
Cost	64

\[1\]

Alternative 60
Error	61.3
Cost	64

\[0\]

Alternative 61
Error	59.6
Cost	64

\[-1\]

Derivation

Split input into 3 regimes
if eps < -4.15051431836954061e-5
1. Initial program 29.1
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum_binary64_12050.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied tan-quot_binary64_12290.4
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \color{blue}{\frac{\sin \varepsilon}{\cos \varepsilon}}} - \tan x\]
6. Applied tan-quot_binary64_12290.4
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x}{\cos x}} \cdot \frac{\sin \varepsilon}{\cos \varepsilon}} - \tan x\]
7. Applied frac-times_binary64_10800.4
  \[\leadsto \frac{\tan x + \tan \varepsilon}{1 - \color{blue}{\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}}} - \tan x\]
8. Using strategy rm
9. Applied flip3--_binary64_10740.4
  \[\leadsto \frac{\tan x + \tan \varepsilon}{\color{blue}{\frac{{1}^{3} - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)}^{3}}{1 \cdot 1 + \left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1 \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)}}} - \tan x\]
10. Applied associate-/r/_binary64_10160.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{{1}^{3} - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)}^{3}} \cdot \left(1 \cdot 1 + \left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1 \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)\right)} - \tan x\]
11. Simplified0.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - {\left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)}^{3}}} \cdot \left(1 \cdot 1 + \left(\frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon} + 1 \cdot \frac{\sin x \cdot \sin \varepsilon}{\cos x \cdot \cos \varepsilon}\right)\right) - \tan x\]
12. Simplified0.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - {\left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}^{3}} \cdot \left(1 + \left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x} + \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)\right) - \tan x}\]
if -4.15051431836954061e-5 < eps < 4.79211306635322646e-5
1. Initial program 45.2
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum_binary64_120544.6
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Taylor expanded around 0 0.2
  \[\leadsto \color{blue}{\frac{\sin x \cdot {\varepsilon}^{2}}{\cos x} + \left(1.3333333333333333 \cdot \frac{{\sin x}^{2} \cdot {\varepsilon}^{3}}{{\cos x}^{2}} + \left(\frac{{\sin x}^{2} \cdot \varepsilon}{{\cos x}^{2}} + \left(0.3333333333333333 \cdot {\varepsilon}^{3} + \left(\frac{{\sin x}^{3} \cdot {\varepsilon}^{2}}{{\cos x}^{3}} + \left(\varepsilon + \frac{{\sin x}^{4} \cdot {\varepsilon}^{3}}{{\cos x}^{4}}\right)\right)\right)\right)\right)}\]
5. Simplified0.2
  \[\leadsto \color{blue}{\left(\frac{{\sin x}^{2}}{{\cos x}^{2}} \cdot \varepsilon + 1.3333333333333333 \cdot \left(\frac{{\sin x}^{2}}{{\cos x}^{2}} \cdot {\varepsilon}^{3}\right)\right) + \left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(\frac{{\sin x}^{4}}{{\cos x}^{4}} + 0.3333333333333333\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left({\left(\frac{\sin x}{\cos x}\right)}^{3} + \frac{\sin x}{\cos x}\right)\right)}\]
6. Simplified0.2
  \[\leadsto \color{blue}{\left(\varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}} + 1.3333333333333333 \cdot \left(\frac{{\sin x}^{2}}{{\cos x}^{2}} \cdot {\varepsilon}^{3}\right)\right) + \left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(\frac{{\sin x}^{4}}{{\cos x}^{4}} + 0.3333333333333333\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + {\left(\frac{\sin x}{\cos x}\right)}^{3}\right)\right)}\]
if 4.79211306635322646e-5 < eps
1. Initial program 29.9
  \[\tan \left(x + \varepsilon\right) - \tan x\]
2. Using strategy rm
3. Applied tan-sum_binary64_12050.4
  \[\leadsto \color{blue}{\frac{\tan x + \tan \varepsilon}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
4. Using strategy rm
5. Applied div-inv_binary64_10670.4
  \[\leadsto \color{blue}{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon}} - \tan x\]
6. Simplified0.4
  \[\leadsto \color{blue}{\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x}\]
Recombined 3 regimes into one program.
Final simplification0.3
\[\leadsto \begin{array}{l} \mathbf{if}\;\varepsilon \leq -4.1505143183695406 \cdot 10^{-05}:\\ \;\;\;\;\frac{\tan x + \tan \varepsilon}{1 - {\left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)}^{3}} \cdot \left(1 + \left(\frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x} + \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x} \cdot \frac{\sin \varepsilon \cdot \sin x}{\cos \varepsilon \cdot \cos x}\right)\right) - \tan x\\ \mathbf{elif}\;\varepsilon \leq 4.7921130663532265 \cdot 10^{-05}:\\ \;\;\;\;\left(\varepsilon \cdot \frac{{\sin x}^{2}}{{\cos x}^{2}} + 1.3333333333333333 \cdot \left(\frac{{\sin x}^{2}}{{\cos x}^{2}} \cdot {\varepsilon}^{3}\right)\right) + \left(\left(\varepsilon + {\varepsilon}^{3} \cdot \left(\frac{{\sin x}^{4}}{{\cos x}^{4}} + 0.3333333333333333\right)\right) + \left(\varepsilon \cdot \varepsilon\right) \cdot \left(\frac{\sin x}{\cos x} + {\left(\frac{\sin x}{\cos x}\right)}^{3}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\left(\tan x + \tan \varepsilon\right) \cdot \frac{1}{1 - \tan x \cdot \tan \varepsilon} - \tan x\\ \end{array}\]

Reproduce

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

Error

Try it out

Target

Alternatives

Error

Derivation

`if eps < -4.15051431836954061e-5`

`if -4.15051431836954061e-5 < eps < 4.79211306635322646e-5`

`if 4.79211306635322646e-5 < eps`

Reproduce