Average Error: 18.7 → 1.9
Time: 2.3s
Precision: binary64
\[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
↓
\[\frac{1}{\frac{t1 + u}{v} \cdot \left(-1 - \frac{u}{t1}\right)}\]

Error

Bits error versus u

Bits error versus v

Bits error versus t1

Derivation

  1. Initial program 18.7

    \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]

  2. Simplified3.5

    \[\leadsto \color{blue}{\frac{v}{\left(t1 + u\right) \cdot \left(-1 - \frac{u}{t1}\right)}}\]
  3. Using strategy rm

  4. Applied clear-num4.0

    \[\leadsto \color{blue}{\frac{1}{\frac{\left(t1 + u\right) \cdot \left(-1 - \frac{u}{t1}\right)}{v}}}\]

  5. Simplified1.9

    \[\leadsto \frac{1}{\color{blue}{\frac{t1 + u}{v} \cdot \left(-1 - \frac{u}{t1}\right)}}\]

  6. Final simplification1.9

    \[\leadsto \frac{1}{\frac{t1 + u}{v} \cdot \left(-1 - \frac{u}{t1}\right)}\]

Reproduce

herbie shell --seed 2020182 
(FPCore (u v t1)
  :name "Rosa's DopplerBench"
  :precision binary64
  (/ (* (neg t1) v) (* (+ t1 u) (+ t1 u))))