\[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
Test:
Rosa's DopplerBench
Bits:
128 bits
Bits error versus u
Bits error versus v
Bits error versus t1
Time: 8.8 s
Input Error: 8.9
Output Error: 0.6
Log: ⚲
Profile: 🕒
\(\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}\)
  1. Started with
    \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
    8.9
  2. Using strategy rm
    8.9
  3. Applied times-frac to get
    \[\color{red}{\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}} \leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}}\]
    0.6
  4. Removed slow pow expressions

Original test:


(lambda ((u default) (v default) (t1 default))
  #:name "Rosa's DopplerBench"
  (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))