\[\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.2 s
Input Error: 18.3
Output Error: 1.4
Log: ⚲
Profile: 🕒
\(\left(\frac{-t1}{t1 + u} \cdot v\right) \cdot \frac{1}{t1 + u}\)
  1. Started with
    \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
    18.3
  2. Using strategy rm
    18.3
  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 div-inv to get
    \[\frac{-t1}{t1 + u} \cdot \color{red}{\frac{v}{t1 + u}} \leadsto \frac{-t1}{t1 + u} \cdot \color{blue}{\left(v \cdot \frac{1}{t1 + u}\right)}\]
    1.4
  6. Applied associate-*r* to get
    \[\color{red}{\frac{-t1}{t1 + u} \cdot \left(v \cdot \frac{1}{t1 + u}\right)} \leadsto \color{blue}{\left(\frac{-t1}{t1 + u} \cdot v\right) \cdot \frac{1}{t1 + u}}\]
    1.4
  7. Removed slow pow expressions

Original test:


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