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

  6. Removed slow pow expressions

Original test:


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