\[\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: 6.2 s
Input Error: 18.1
Output Error: 1.3
Log: ⚲
Profile: 🕒
\(\frac{\frac{-t1}{t1 + u} \cdot v}{t1 + u}\)
  1. Started with
    \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
    18.1
  2. Using strategy rm
    18.1
  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}}\]
    1.3
  4. Using strategy rm
    1.3
  5. Applied associate-*r/ to get
    \[\color{red}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \leadsto \color{blue}{\frac{\frac{-t1}{t1 + u} \cdot v}{t1 + u}}\]
    1.3

Original test:


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