Average Error: 0.3 → 0.4
Time: 13.2s
Precision: 64
\[\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]
↓
\[\left(\sqrt{1} + \tan x\right) \cdot \left(\frac{\sqrt{1}}{\mathsf{fma}\left(\tan x, \tan x, 1\right)} - \tan x \cdot \frac{1}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}\right)\]
\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}
↓
\left(\sqrt{1} + \tan x\right) \cdot \left(\frac{\sqrt{1}}{\mathsf{fma}\left(\tan x, \tan x, 1\right)} - \tan x \cdot \frac{1}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}\right)
double f(double x) {
        double r20710 = 1.0;
        double r20711 = x;
        double r20712 = tan(r20711);
        double r20713 = r20712 * r20712;
        double r20714 = r20710 - r20713;
        double r20715 = r20710 + r20713;
        double r20716 = r20714 / r20715;
        return r20716;
}
↓
double f(double x) {
        double r20717 = 1.0;
        double r20718 = sqrt(r20717);
        double r20719 = x;
        double r20720 = tan(r20719);
        double r20721 = r20718 + r20720;
        double r20722 = fma(r20720, r20720, r20717);
        double r20723 = r20718 / r20722;
        double r20724 = 1.0;
        double r20725 = r20724 / r20722;
        double r20726 = r20720 * r20725;
        double r20727 = r20723 - r20726;
        double r20728 = r20721 * r20727;
        return r20728;
}

Error

Bits error versus x

Derivation

  1. Initial program 0.3

    \[\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]
  2. Using strategy rm

  3. Applied *-un-lft-identity0.3

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

  4. Applied add-sqr-sqrt0.3

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

  5. Applied difference-of-squares0.3

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

  6. Applied times-frac0.4

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

  7. Simplified0.4

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

  8. Simplified0.4

    \[\leadsto \left(\sqrt{1} + \tan x\right) \cdot \color{blue}{\frac{\sqrt{1} - \tan x}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}}\]
  9. Using strategy rm

  10. Applied div-sub0.4

    \[\leadsto \left(\sqrt{1} + \tan x\right) \cdot \color{blue}{\left(\frac{\sqrt{1}}{\mathsf{fma}\left(\tan x, \tan x, 1\right)} - \frac{\tan x}{\mathsf{fma}\left(\tan x, \tan x, 1\right)}\right)}\]
  11. Using strategy rm

  12. Applied div-inv0.4

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

  13. Final simplification0.4

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

Reproduce

herbie shell --seed 2020047 +o rules:numerics
(FPCore (x)
  :name "Trigonometry B"
  :precision binary64
  (/ (- 1 (* (tan x) (tan x))) (+ 1 (* (tan x) (tan x)))))