Average Error: 0.3 → 1.1
Time: 19.8s
Precision: 64
Internal Precision: 128
\[\frac{1 - \tan x \cdot \tan x}{1 + \tan x \cdot \tan x}\]
↓
\[\frac{\log \left(e^{-\tan x \cdot \tan x} \cdot e\right)}{\tan x \cdot \tan x + 1}\]

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 add-log-exp1.1

    \[\leadsto \frac{\color{blue}{\log \left(e^{1 - \tan x \cdot \tan x}\right)}}{1 + \tan x \cdot \tan x}\]
  4. Using strategy rm

  5. Applied sub-neg1.1

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

  6. Applied exp-sum1.1

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

  7. Simplified1.1

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

  8. Final simplification1.1

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

Reproduce

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