Rosa's DopplerBench

1. Initial program 73.2%

   \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
2. Step-by-step derivation

   1. times-frac97.5%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

3. Simplified97.5%

   \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

4. Final simplification97.5%

   \[\leadsto \frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u} \]

1. Split input into 3 regimes

2. if t1 < -3.19999999999999991e60 or -9.0000000000000002e-25 < t1 < -7.0000000000000003e-146

   1. Initial program 65.7%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. *-commutative65.7%

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

      2. times-frac99.9%

         \[\leadsto \color{blue}{\frac{v}{t1 + u} \cdot \frac{-t1}{t1 + u}} \]

      3. neg-mul-199.9%

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

      4. associate-/l*99.9%

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

      5. associate-*r/99.8%

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

      6. associate-/l*99.8%

         \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{\frac{t1 + u}{t1}}{-1}}} \]

      7. associate-/l/99.8%

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

      8. neg-mul-199.8%

         \[\leadsto \frac{\frac{v}{t1 + u}}{\frac{t1 + u}{\color{blue}{-t1}}} \]

      9. *-lft-identity99.8%

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

      10. metadata-eval99.8%

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

      11. times-frac99.8%

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

      12. neg-mul-199.8%

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

      13. remove-double-neg99.8%

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

      14. neg-mul-199.8%

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

      15. sub0-neg99.8%

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

      16. associate--r+99.8%

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

      17. neg-sub099.8%

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

      18. div-sub99.9%

          \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{-t1}{t1} - \frac{u}{t1}}} \]

      19. distribute-frac-neg99.9%

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

      20. *-inverses99.9%

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

      21. metadata-eval99.9%

          \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{-1} - \frac{u}{t1}} \]

   3. Simplified99.9%

      \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{-1 - \frac{u}{t1}}} \]

   4. Taylor expanded in t1 around inf 77.7%

      \[\leadsto \frac{\color{blue}{\frac{v}{t1}}}{-1 - \frac{u}{t1}} \]

   if -3.19999999999999991e60 < t1 < -9.0000000000000002e-25 or -7.0000000000000003e-146 < t1 < 5.49999999999999977e-133

   1. Initial program 83.8%

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

   2. Taylor expanded in t1 around 0 82.5%

      \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
   3. Step-by-step derivation

      1. mul-1-neg82.5%

         \[\leadsto \color{blue}{-\frac{t1 \cdot v}{{u}^{2}}} \]

      2. unpow282.5%

         \[\leadsto -\frac{t1 \cdot v}{\color{blue}{u \cdot u}} \]

      3. times-frac90.1%

         \[\leadsto -\color{blue}{\frac{t1}{u} \cdot \frac{v}{u}} \]

      4. *-commutative90.1%

         \[\leadsto -\color{blue}{\frac{v}{u} \cdot \frac{t1}{u}} \]

      5. distribute-rgt-neg-in90.1%

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

   4. Simplified90.1%

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

   if 5.49999999999999977e-133 < t1

   1. Initial program 68.2%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. associate-/l*77.2%

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

      2. associate-/l*85.4%

         \[\leadsto \frac{-t1}{\color{blue}{\frac{t1 + u}{\frac{v}{t1 + u}}}} \]

   3. Simplified85.4%

      \[\leadsto \color{blue}{\frac{-t1}{\frac{t1 + u}{\frac{v}{t1 + u}}}} \]

   4. Taylor expanded in t1 around inf 69.7%

      \[\leadsto \frac{-t1}{\frac{t1 + u}{\color{blue}{\frac{v}{t1}}}} \]

   5. Taylor expanded in v around 0 77.0%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1 + u}} \]
   6. Step-by-step derivation

      1. neg-mul-177.0%

         \[\leadsto \color{blue}{-\frac{v}{t1 + u}} \]

      2. distribute-neg-frac77.0%

         \[\leadsto \color{blue}{\frac{-v}{t1 + u}} \]

   7. Simplified77.0%

      \[\leadsto \color{blue}{\frac{-v}{t1 + u}} \]
3. Recombined 3 regimes into one program.

4. Final simplification82.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;t1 \leq -3.2 \cdot 10^{+60}:\\ \;\;\;\;\frac{\frac{v}{t1}}{-1 - \frac{u}{t1}}\\ \mathbf{elif}\;t1 \leq -9 \cdot 10^{-25}:\\ \;\;\;\;\frac{t1}{u} \cdot \frac{-v}{u}\\ \mathbf{elif}\;t1 \leq -7 \cdot 10^{-146}:\\ \;\;\;\;\frac{\frac{v}{t1}}{-1 - \frac{u}{t1}}\\ \mathbf{elif}\;t1 \leq 5.5 \cdot 10^{-133}:\\ \;\;\;\;\frac{t1}{u} \cdot \frac{-v}{u}\\ \mathbf{else}:\\ \;\;\;\;\frac{-v}{t1 + u}\\ \end{array} \]

1. Split input into 2 regimes

2. if u < -1.3e-95 or 6.79999999999999946e-55 < u

   1. Initial program 80.8%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.8%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.8%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around 0 78.8%

      \[\leadsto \color{blue}{\left(-1 \cdot \frac{t1}{u}\right)} \cdot \frac{v}{t1 + u} \]
   5. Step-by-step derivation

      1. mul-1-neg78.8%

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

   6. Simplified78.8%

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

   if -1.3e-95 < u < 6.79999999999999946e-55

   1. Initial program 61.6%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.1%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.1%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around inf 82.1%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
   5. Step-by-step derivation

      1. associate-*r/82.1%

         \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]

      2. neg-mul-182.1%

         \[\leadsto \frac{\color{blue}{-v}}{t1} \]

   6. Simplified82.1%

      \[\leadsto \color{blue}{\frac{-v}{t1}} \]
3. Recombined 2 regimes into one program.

4. Final simplification80.1%

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -1.3 \cdot 10^{-95} \lor \neg \left(u \leq 6.8 \cdot 10^{-55}\right):\\ \;\;\;\;\frac{v}{t1 + u} \cdot \frac{-t1}{u}\\ \mathbf{else}:\\ \;\;\;\;\frac{-v}{t1}\\ \end{array} \]

1. Split input into 3 regimes

2. if u < -2.7000000000000001e-94

   1. Initial program 83.3%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac98.6%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified98.6%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around 0 78.9%

      \[\leadsto \color{blue}{\left(-1 \cdot \frac{t1}{u}\right)} \cdot \frac{v}{t1 + u} \]
   5. Step-by-step derivation

      1. mul-1-neg78.9%

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

   6. Simplified78.9%

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

   if -2.7000000000000001e-94 < u < 1.9000000000000001e-54

   1. Initial program 61.6%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.1%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.1%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around inf 82.1%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
   5. Step-by-step derivation

      1. associate-*r/82.1%

         \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]

      2. neg-mul-182.1%

         \[\leadsto \frac{\color{blue}{-v}}{t1} \]

   6. Simplified82.1%

      \[\leadsto \color{blue}{\frac{-v}{t1}} \]

   if 1.9000000000000001e-54 < u

   1. Initial program 77.4%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac96.6%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified96.6%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around 0 78.6%

      \[\leadsto \color{blue}{\left(-1 \cdot \frac{t1}{u}\right)} \cdot \frac{v}{t1 + u} \]
   5. Step-by-step derivation

      1. mul-1-neg78.6%

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

   6. Simplified78.6%

      \[\leadsto \color{blue}{\left(-\frac{t1}{u}\right)} \cdot \frac{v}{t1 + u} \]
   7. Step-by-step derivation

      1. add-sqr-sqrt51.9%

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

      2. sqrt-unprod61.6%

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

      3. sqr-neg61.6%

         \[\leadsto \sqrt{\color{blue}{\frac{t1}{u} \cdot \frac{t1}{u}}} \cdot \frac{v}{t1 + u} \]

      4. sqrt-unprod35.7%

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

      5. add-sqr-sqrt49.3%

         \[\leadsto \color{blue}{\frac{t1}{u}} \cdot \frac{v}{t1 + u} \]

      6. frac-2neg49.3%

         \[\leadsto \color{blue}{\frac{-t1}{-u}} \cdot \frac{v}{t1 + u} \]

      7. associate-*l/49.2%

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

      8. add-sqr-sqrt21.2%

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

      9. sqrt-unprod51.0%

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

      10. sqr-neg51.0%

          \[\leadsto \frac{\sqrt{\color{blue}{t1 \cdot t1}} \cdot \frac{v}{t1 + u}}{-u} \]

      11. sqrt-prod37.0%

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

      12. add-sqr-sqrt80.3%

          \[\leadsto \frac{\color{blue}{t1} \cdot \frac{v}{t1 + u}}{-u} \]

   8. Applied egg-rr80.3%

      \[\leadsto \color{blue}{\frac{t1 \cdot \frac{v}{t1 + u}}{-u}} \]
3. Recombined 3 regimes into one program.

4. Final simplification80.5%

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -2.7 \cdot 10^{-94}:\\ \;\;\;\;\frac{v}{t1 + u} \cdot \frac{-t1}{u}\\ \mathbf{elif}\;u \leq 1.9 \cdot 10^{-54}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{t1 \cdot \frac{v}{t1 + u}}{-u}\\ \end{array} \]

1. Split input into 3 regimes

2. if u < -1.55e-114

   1. Initial program 83.3%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.7%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.7%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]
   4. Step-by-step derivation

      1. associate-*r/99.3%

         \[\leadsto \color{blue}{\frac{\frac{-t1}{t1 + u} \cdot v}{t1 + u}} \]

      2. frac-2neg99.3%

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

      3. add-sqr-sqrt45.5%

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

      4. sqrt-unprod54.8%

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

      5. sqr-neg54.8%

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

      6. sqrt-unprod28.9%

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

      7. add-sqr-sqrt54.5%

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

      8. distribute-lft-neg-out54.5%

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

      9. distribute-frac-neg54.5%

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

      10. add-sqr-sqrt25.6%

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

      11. sqrt-unprod59.1%

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

      12. sqr-neg59.1%

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

      13. sqrt-unprod53.7%

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

      14. add-sqr-sqrt99.3%

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

      15. distribute-neg-in99.3%

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

      16. add-sqr-sqrt45.5%

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

      17. sqrt-unprod81.9%

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

      18. sqr-neg81.9%

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

      19. sqrt-unprod38.5%

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

      20. add-sqr-sqrt78.5%

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

      21. sub-neg78.5%

          \[\leadsto \frac{\frac{t1}{t1 + u} \cdot v}{\color{blue}{t1 - u}} \]

   5. Applied egg-rr78.5%

      \[\leadsto \color{blue}{\frac{\frac{t1}{t1 + u} \cdot v}{t1 - u}} \]

   if -1.55e-114 < u < 8.19999999999999977e-52

   1. Initial program 60.2%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.9%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.9%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around inf 83.7%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
   5. Step-by-step derivation

      1. associate-*r/83.7%

         \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]

      2. neg-mul-183.7%

         \[\leadsto \frac{\color{blue}{-v}}{t1} \]

   6. Simplified83.7%

      \[\leadsto \color{blue}{\frac{-v}{t1}} \]

   if 8.19999999999999977e-52 < u

   1. Initial program 77.4%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac96.6%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified96.6%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around 0 78.6%

      \[\leadsto \color{blue}{\left(-1 \cdot \frac{t1}{u}\right)} \cdot \frac{v}{t1 + u} \]
   5. Step-by-step derivation

      1. mul-1-neg78.6%

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

   6. Simplified78.6%

      \[\leadsto \color{blue}{\left(-\frac{t1}{u}\right)} \cdot \frac{v}{t1 + u} \]
   7. Step-by-step derivation

      1. add-sqr-sqrt51.9%

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

      2. sqrt-unprod61.6%

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

      3. sqr-neg61.6%

         \[\leadsto \sqrt{\color{blue}{\frac{t1}{u} \cdot \frac{t1}{u}}} \cdot \frac{v}{t1 + u} \]

      4. sqrt-unprod35.7%

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

      5. add-sqr-sqrt49.3%

         \[\leadsto \color{blue}{\frac{t1}{u}} \cdot \frac{v}{t1 + u} \]

      6. frac-2neg49.3%

         \[\leadsto \color{blue}{\frac{-t1}{-u}} \cdot \frac{v}{t1 + u} \]

      7. associate-*l/49.2%

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

      8. add-sqr-sqrt21.2%

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

      9. sqrt-unprod51.0%

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

      10. sqr-neg51.0%

          \[\leadsto \frac{\sqrt{\color{blue}{t1 \cdot t1}} \cdot \frac{v}{t1 + u}}{-u} \]

      11. sqrt-prod37.0%

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

      12. add-sqr-sqrt80.3%

          \[\leadsto \frac{\color{blue}{t1} \cdot \frac{v}{t1 + u}}{-u} \]

   8. Applied egg-rr80.3%

      \[\leadsto \color{blue}{\frac{t1 \cdot \frac{v}{t1 + u}}{-u}} \]
3. Recombined 3 regimes into one program.

4. Final simplification80.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -1.55 \cdot 10^{-114}:\\ \;\;\;\;\frac{v \cdot \frac{t1}{t1 + u}}{t1 - u}\\ \mathbf{elif}\;u \leq 8.2 \cdot 10^{-52}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{t1 \cdot \frac{v}{t1 + u}}{-u}\\ \end{array} \]

1. Split input into 2 regimes

2. if u < -8.50000000000000044e-60 or 6.1999999999999998e-52 < u

   1. Initial program 80.1%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.7%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.7%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around 0 67.3%

      \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
   5. Step-by-step derivation

      1. associate-*r/67.3%

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

      2. neg-mul-167.3%

         \[\leadsto \frac{\color{blue}{-t1 \cdot v}}{{u}^{2}} \]

      3. distribute-rgt-neg-out67.3%

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

      4. unpow267.3%

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

   6. Simplified67.3%

      \[\leadsto \color{blue}{\frac{t1 \cdot \left(-v\right)}{u \cdot u}} \]
   7. Step-by-step derivation

      1. frac-2neg67.3%

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

      2. distribute-frac-neg67.3%

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

      3. add-sqr-sqrt39.2%

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

      4. sqrt-unprod55.3%

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

      5. sqr-neg55.3%

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

      6. sqrt-unprod20.8%

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

      7. add-sqr-sqrt47.7%

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

      8. distribute-rgt-neg-in47.7%

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

      9. frac-2neg47.7%

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

      10. times-frac48.6%

          \[\leadsto -\color{blue}{\frac{t1}{u} \cdot \frac{-v}{u}} \]

      11. associate-*l/48.5%

          \[\leadsto -\color{blue}{\frac{t1 \cdot \frac{-v}{u}}{u}} \]

      12. add-sqr-sqrt20.8%

          \[\leadsto -\frac{t1 \cdot \frac{\color{blue}{\sqrt{-v} \cdot \sqrt{-v}}}{u}}{u} \]

      13. sqrt-unprod58.1%

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

      14. sqr-neg58.1%

          \[\leadsto -\frac{t1 \cdot \frac{\sqrt{\color{blue}{v \cdot v}}}{u}}{u} \]

      15. sqrt-unprod44.7%

          \[\leadsto -\frac{t1 \cdot \frac{\color{blue}{\sqrt{v} \cdot \sqrt{v}}}{u}}{u} \]

      16. add-sqr-sqrt75.7%

          \[\leadsto -\frac{t1 \cdot \frac{\color{blue}{v}}{u}}{u} \]

   8. Applied egg-rr75.7%

      \[\leadsto \color{blue}{-\frac{t1 \cdot \frac{v}{u}}{u}} \]

   if -8.50000000000000044e-60 < u < 6.1999999999999998e-52

   1. Initial program 63.4%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.2%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.2%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around inf 80.9%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
   5. Step-by-step derivation

      1. associate-*r/80.9%

         \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]

      2. neg-mul-180.9%

         \[\leadsto \frac{\color{blue}{-v}}{t1} \]

   6. Simplified80.9%

      \[\leadsto \color{blue}{\frac{-v}{t1}} \]
3. Recombined 2 regimes into one program.

4. Final simplification77.9%

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -8.5 \cdot 10^{-60} \lor \neg \left(u \leq 6.2 \cdot 10^{-52}\right):\\ \;\;\;\;\frac{t1 \cdot \frac{-v}{u}}{u}\\ \mathbf{else}:\\ \;\;\;\;\frac{-v}{t1}\\ \end{array} \]

1. Split input into 3 regimes

2. if u < -1.2e-61

   1. Initial program 82.3%

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

   2. Taylor expanded in t1 around 0 68.0%

      \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
   3. Step-by-step derivation

      1. mul-1-neg68.0%

         \[\leadsto \color{blue}{-\frac{t1 \cdot v}{{u}^{2}}} \]

      2. unpow268.0%

         \[\leadsto -\frac{t1 \cdot v}{\color{blue}{u \cdot u}} \]

      3. times-frac74.6%

         \[\leadsto -\color{blue}{\frac{t1}{u} \cdot \frac{v}{u}} \]

      4. *-commutative74.6%

         \[\leadsto -\color{blue}{\frac{v}{u} \cdot \frac{t1}{u}} \]

      5. distribute-rgt-neg-in74.6%

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

   4. Simplified74.6%

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

   if -1.2e-61 < u < 1.16e-54

   1. Initial program 63.4%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.2%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.2%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around inf 80.9%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
   5. Step-by-step derivation

      1. associate-*r/80.9%

         \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]

      2. neg-mul-180.9%

         \[\leadsto \frac{\color{blue}{-v}}{t1} \]

   6. Simplified80.9%

      \[\leadsto \color{blue}{\frac{-v}{t1}} \]

   if 1.16e-54 < u

   1. Initial program 77.4%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac96.6%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified96.6%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around 0 66.4%

      \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
   5. Step-by-step derivation

      1. associate-*r/66.4%

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

      2. neg-mul-166.4%

         \[\leadsto \frac{\color{blue}{-t1 \cdot v}}{{u}^{2}} \]

      3. distribute-rgt-neg-out66.4%

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

      4. unpow266.4%

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

   6. Simplified66.4%

      \[\leadsto \color{blue}{\frac{t1 \cdot \left(-v\right)}{u \cdot u}} \]
   7. Step-by-step derivation

      1. frac-2neg66.4%

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

      2. distribute-frac-neg66.4%

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

      3. add-sqr-sqrt34.3%

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

      4. sqrt-unprod51.8%

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

      5. sqr-neg51.8%

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

      6. sqrt-unprod21.4%

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

      7. add-sqr-sqrt44.5%

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

      8. distribute-rgt-neg-in44.5%

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

      9. frac-2neg44.5%

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

      10. times-frac45.9%

          \[\leadsto -\color{blue}{\frac{t1}{u} \cdot \frac{-v}{u}} \]

      11. associate-*l/45.8%

          \[\leadsto -\color{blue}{\frac{t1 \cdot \frac{-v}{u}}{u}} \]

      12. add-sqr-sqrt21.4%

          \[\leadsto -\frac{t1 \cdot \frac{\color{blue}{\sqrt{-v} \cdot \sqrt{-v}}}{u}}{u} \]

      13. sqrt-unprod56.8%

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

      14. sqr-neg56.8%

          \[\leadsto -\frac{t1 \cdot \frac{\sqrt{\color{blue}{v \cdot v}}}{u}}{u} \]

      15. sqrt-unprod41.9%

          \[\leadsto -\frac{t1 \cdot \frac{\color{blue}{\sqrt{v} \cdot \sqrt{v}}}{u}}{u} \]

      16. add-sqr-sqrt77.5%

          \[\leadsto -\frac{t1 \cdot \frac{\color{blue}{v}}{u}}{u} \]

   8. Applied egg-rr77.5%

      \[\leadsto \color{blue}{-\frac{t1 \cdot \frac{v}{u}}{u}} \]
3. Recombined 3 regimes into one program.

4. Final simplification78.0%

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -1.2 \cdot 10^{-61}:\\ \;\;\;\;\frac{t1}{u} \cdot \frac{-v}{u}\\ \mathbf{elif}\;u \leq 1.16 \cdot 10^{-54}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{t1 \cdot \frac{-v}{u}}{u}\\ \end{array} \]

1. Split input into 3 regimes

2. if u < -5.6000000000000001e-58

   1. Initial program 82.3%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac98.5%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified98.5%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around 0 68.0%

      \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
   5. Step-by-step derivation

      1. associate-*r/68.0%

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

      2. neg-mul-168.0%

         \[\leadsto \frac{\color{blue}{-t1 \cdot v}}{{u}^{2}} \]

      3. distribute-rgt-neg-out68.0%

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

      4. unpow268.0%

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

   6. Simplified68.0%

      \[\leadsto \color{blue}{\frac{t1 \cdot \left(-v\right)}{u \cdot u}} \]
   7. Step-by-step derivation

      1. associate-/l*69.9%

         \[\leadsto \color{blue}{\frac{t1}{\frac{u \cdot u}{-v}}} \]

      2. associate-/r/66.1%

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

      3. add-sqr-sqrt24.8%

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

      4. sqrt-unprod55.3%

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

      5. sqr-neg55.3%

         \[\leadsto \frac{t1}{u \cdot u} \cdot \sqrt{\color{blue}{v \cdot v}} \]

      6. sqrt-unprod30.2%

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

      7. add-sqr-sqrt50.6%

         \[\leadsto \frac{t1}{u \cdot u} \cdot \color{blue}{v} \]

   8. Applied egg-rr50.6%

      \[\leadsto \color{blue}{\frac{t1}{u \cdot u} \cdot v} \]
   9. Step-by-step derivation

      1. associate-*l/50.2%

         \[\leadsto \color{blue}{\frac{t1 \cdot v}{u \cdot u}} \]

      2. *-commutative50.2%

         \[\leadsto \frac{\color{blue}{v \cdot t1}}{u \cdot u} \]

      3. frac-times50.7%

         \[\leadsto \color{blue}{\frac{v}{u} \cdot \frac{t1}{u}} \]

      4. clear-num50.7%

         \[\leadsto \color{blue}{\frac{1}{\frac{u}{v}}} \cdot \frac{t1}{u} \]

      5. frac-2neg50.7%

         \[\leadsto \frac{1}{\frac{u}{v}} \cdot \color{blue}{\frac{-t1}{-u}} \]

      6. frac-times51.9%

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

      7. *-un-lft-identity51.9%

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

      8. add-sqr-sqrt51.9%

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

      9. sqrt-unprod52.1%

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

      10. sqr-neg52.1%

          \[\leadsto \frac{-t1}{\frac{u}{v} \cdot \sqrt{\color{blue}{u \cdot u}}} \]

      11. sqrt-prod0.0%

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

      12. add-sqr-sqrt75.1%

          \[\leadsto \frac{-t1}{\frac{u}{v} \cdot \color{blue}{u}} \]

   10. Applied egg-rr75.1%

       \[\leadsto \color{blue}{\frac{-t1}{\frac{u}{v} \cdot u}} \]

   if -5.6000000000000001e-58 < u < 8.9999999999999997e-54

   1. Initial program 63.4%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.2%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.2%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around inf 80.9%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
   5. Step-by-step derivation

      1. associate-*r/80.9%

         \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]

      2. neg-mul-180.9%

         \[\leadsto \frac{\color{blue}{-v}}{t1} \]

   6. Simplified80.9%

      \[\leadsto \color{blue}{\frac{-v}{t1}} \]

   if 8.9999999999999997e-54 < u

   1. Initial program 77.4%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac96.6%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified96.6%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around 0 66.4%

      \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
   5. Step-by-step derivation

      1. associate-*r/66.4%

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

      2. neg-mul-166.4%

         \[\leadsto \frac{\color{blue}{-t1 \cdot v}}{{u}^{2}} \]

      3. distribute-rgt-neg-out66.4%

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

      4. unpow266.4%

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

   6. Simplified66.4%

      \[\leadsto \color{blue}{\frac{t1 \cdot \left(-v\right)}{u \cdot u}} \]
   7. Step-by-step derivation

      1. frac-2neg66.4%

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

      2. distribute-frac-neg66.4%

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

      3. add-sqr-sqrt34.3%

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

      4. sqrt-unprod51.8%

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

      5. sqr-neg51.8%

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

      6. sqrt-unprod21.4%

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

      7. add-sqr-sqrt44.5%

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

      8. distribute-rgt-neg-in44.5%

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

      9. frac-2neg44.5%

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

      10. times-frac45.9%

          \[\leadsto -\color{blue}{\frac{t1}{u} \cdot \frac{-v}{u}} \]

      11. associate-*l/45.8%

          \[\leadsto -\color{blue}{\frac{t1 \cdot \frac{-v}{u}}{u}} \]

      12. add-sqr-sqrt21.4%

          \[\leadsto -\frac{t1 \cdot \frac{\color{blue}{\sqrt{-v} \cdot \sqrt{-v}}}{u}}{u} \]

      13. sqrt-unprod56.8%

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

      14. sqr-neg56.8%

          \[\leadsto -\frac{t1 \cdot \frac{\sqrt{\color{blue}{v \cdot v}}}{u}}{u} \]

      15. sqrt-unprod41.9%

          \[\leadsto -\frac{t1 \cdot \frac{\color{blue}{\sqrt{v} \cdot \sqrt{v}}}{u}}{u} \]

      16. add-sqr-sqrt77.5%

          \[\leadsto -\frac{t1 \cdot \frac{\color{blue}{v}}{u}}{u} \]

   8. Applied egg-rr77.5%

      \[\leadsto \color{blue}{-\frac{t1 \cdot \frac{v}{u}}{u}} \]
3. Recombined 3 regimes into one program.

4. Final simplification78.2%

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -5.6 \cdot 10^{-58}:\\ \;\;\;\;\frac{-t1}{u \cdot \frac{u}{v}}\\ \mathbf{elif}\;u \leq 9 \cdot 10^{-54}:\\ \;\;\;\;\frac{-v}{t1}\\ \mathbf{else}:\\ \;\;\;\;\frac{t1 \cdot \frac{-v}{u}}{u}\\ \end{array} \]

1. Split input into 2 regimes

2. if u < -3.8000000000000003e113 or 3.7999999999999999e46 < u

   1. Initial program 76.3%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac98.5%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified98.5%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around 0 74.2%

      \[\leadsto \color{blue}{-1 \cdot \frac{t1 \cdot v}{{u}^{2}}} \]
   5. Step-by-step derivation

      1. associate-*r/74.2%

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

      2. neg-mul-174.2%

         \[\leadsto \frac{\color{blue}{-t1 \cdot v}}{{u}^{2}} \]

      3. distribute-rgt-neg-out74.2%

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

      4. unpow274.2%

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

   6. Simplified74.2%

      \[\leadsto \color{blue}{\frac{t1 \cdot \left(-v\right)}{u \cdot u}} \]
   7. Step-by-step derivation

      1. associate-/l*75.7%

         \[\leadsto \color{blue}{\frac{t1}{\frac{u \cdot u}{-v}}} \]

      2. associate-/r/72.2%

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

      3. add-sqr-sqrt32.0%

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

      4. sqrt-unprod66.2%

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

      5. sqr-neg66.2%

         \[\leadsto \frac{t1}{u \cdot u} \cdot \sqrt{\color{blue}{v \cdot v}} \]

      6. sqrt-unprod39.1%

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

      7. add-sqr-sqrt69.9%

         \[\leadsto \frac{t1}{u \cdot u} \cdot \color{blue}{v} \]

   8. Applied egg-rr69.9%

      \[\leadsto \color{blue}{\frac{t1}{u \cdot u} \cdot v} \]

   if -3.8000000000000003e113 < u < 3.7999999999999999e46

   1. Initial program 71.6%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.0%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.0%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around inf 66.0%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
   5. Step-by-step derivation

      1. associate-*r/66.0%

         \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]

      2. neg-mul-166.0%

         \[\leadsto \frac{\color{blue}{-v}}{t1} \]

   6. Simplified66.0%

      \[\leadsto \color{blue}{\frac{-v}{t1}} \]
3. Recombined 2 regimes into one program.

4. Final simplification67.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -3.8 \cdot 10^{+113} \lor \neg \left(u \leq 3.8 \cdot 10^{+46}\right):\\ \;\;\;\;v \cdot \frac{t1}{u \cdot u}\\ \mathbf{else}:\\ \;\;\;\;\frac{-v}{t1}\\ \end{array} \]

1. Initial program 73.2%

   \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
2. Step-by-step derivation

   1. *-commutative73.2%

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

   2. times-frac97.5%

      \[\leadsto \color{blue}{\frac{v}{t1 + u} \cdot \frac{-t1}{t1 + u}} \]

   3. neg-mul-197.5%

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

   4. associate-/l*96.8%

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

   5. associate-*r/96.8%

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

   6. associate-/l*96.8%

      \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{\frac{t1 + u}{t1}}{-1}}} \]

   7. associate-/l/96.8%

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

   8. neg-mul-196.8%

      \[\leadsto \frac{\frac{v}{t1 + u}}{\frac{t1 + u}{\color{blue}{-t1}}} \]

   9. *-lft-identity96.8%

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

   10. metadata-eval96.8%

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

   11. times-frac96.8%

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

   12. neg-mul-196.8%

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

   13. remove-double-neg96.8%

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

   14. neg-mul-196.8%

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

   15. sub0-neg96.8%

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

   16. associate--r+96.8%

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

   17. neg-sub096.8%

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

   18. div-sub96.8%

       \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{-t1}{t1} - \frac{u}{t1}}} \]

   19. distribute-frac-neg96.8%

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

   20. *-inverses96.8%

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

   21. metadata-eval96.8%

       \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{-1} - \frac{u}{t1}} \]

3. Simplified96.8%

   \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{-1 - \frac{u}{t1}}} \]

4. Final simplification96.8%

   \[\leadsto \frac{\frac{v}{t1 + u}}{-1 - \frac{u}{t1}} \]

1. Split input into 2 regimes

2. if u < -5.1999999999999998e113 or 3.00000000000000026e154 < u

   1. Initial program 74.7%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. *-commutative74.7%

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

      2. times-frac98.2%

         \[\leadsto \color{blue}{\frac{v}{t1 + u} \cdot \frac{-t1}{t1 + u}} \]

      3. neg-mul-198.2%

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

      4. associate-/l*98.2%

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

      5. associate-*r/98.2%

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

      6. associate-/l*98.2%

         \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{\frac{\frac{t1 + u}{t1}}{-1}}} \]

      7. associate-/l/98.2%

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

      8. neg-mul-198.2%

         \[\leadsto \frac{\frac{v}{t1 + u}}{\frac{t1 + u}{\color{blue}{-t1}}} \]

      9. *-lft-identity98.2%

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

      10. metadata-eval98.2%

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

      11. times-frac98.2%

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

      12. neg-mul-198.2%

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

      13. remove-double-neg98.2%

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

      14. neg-mul-198.2%

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

      15. sub0-neg98.2%

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

      16. associate--r+98.2%

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

      17. neg-sub098.2%

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

      18. div-sub98.2%

          \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{\frac{-t1}{t1} - \frac{u}{t1}}} \]

      19. distribute-frac-neg98.2%

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

      20. *-inverses98.2%

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

      21. metadata-eval98.2%

          \[\leadsto \frac{\frac{v}{t1 + u}}{\color{blue}{-1} - \frac{u}{t1}} \]

   3. Simplified98.2%

      \[\leadsto \color{blue}{\frac{\frac{v}{t1 + u}}{-1 - \frac{u}{t1}}} \]

   4. Taylor expanded in t1 around inf 52.9%

      \[\leadsto \frac{\color{blue}{\frac{v}{t1}}}{-1 - \frac{u}{t1}} \]

   5. Taylor expanded in t1 around 0 32.3%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{u}} \]
   6. Step-by-step derivation

      1. associate-*r/32.3%

         \[\leadsto \color{blue}{\frac{-1 \cdot v}{u}} \]

      2. neg-mul-132.3%

         \[\leadsto \frac{\color{blue}{-v}}{u} \]

   7. Simplified32.3%

      \[\leadsto \color{blue}{\frac{-v}{u}} \]

   if -5.1999999999999998e113 < u < 3.00000000000000026e154

   1. Initial program 72.6%

      \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
   2. Step-by-step derivation

      1. times-frac97.2%

         \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   3. Simplified97.2%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

   4. Taylor expanded in t1 around inf 62.6%

      \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
   5. Step-by-step derivation

      1. associate-*r/62.6%

         \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]

      2. neg-mul-162.6%

         \[\leadsto \frac{\color{blue}{-v}}{t1} \]

   6. Simplified62.6%

      \[\leadsto \color{blue}{\frac{-v}{t1}} \]
3. Recombined 2 regimes into one program.

4. Final simplification54.3%

   \[\leadsto \begin{array}{l} \mathbf{if}\;u \leq -5.2 \cdot 10^{+113} \lor \neg \left(u \leq 3 \cdot 10^{+154}\right):\\ \;\;\;\;\frac{-v}{u}\\ \mathbf{else}:\\ \;\;\;\;\frac{-v}{t1}\\ \end{array} \]

1. Initial program 73.2%

   \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
2. Step-by-step derivation

   1. associate-/l*75.0%

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

   2. associate-/l*85.0%

      \[\leadsto \frac{-t1}{\color{blue}{\frac{t1 + u}{\frac{v}{t1 + u}}}} \]

3. Simplified85.0%

   \[\leadsto \color{blue}{\frac{-t1}{\frac{t1 + u}{\frac{v}{t1 + u}}}} \]

4. Taylor expanded in t1 around inf 48.2%

   \[\leadsto \frac{-t1}{\frac{t1 + u}{\color{blue}{\frac{v}{t1}}}} \]

5. Taylor expanded in v around 0 56.4%

   \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1 + u}} \]
6. Step-by-step derivation

   1. neg-mul-156.4%

      \[\leadsto \color{blue}{-\frac{v}{t1 + u}} \]

   2. distribute-neg-frac56.4%

      \[\leadsto \color{blue}{\frac{-v}{t1 + u}} \]

7. Simplified56.4%

   \[\leadsto \color{blue}{\frac{-v}{t1 + u}} \]

8. Final simplification56.4%

   \[\leadsto \frac{-v}{t1 + u} \]

1. Initial program 73.2%

   \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
2. Step-by-step derivation

   1. times-frac97.5%

      \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

3. Simplified97.5%

   \[\leadsto \color{blue}{\frac{-t1}{t1 + u} \cdot \frac{v}{t1 + u}} \]

4. Taylor expanded in t1 around inf 48.8%

   \[\leadsto \color{blue}{-1 \cdot \frac{v}{t1}} \]
5. Step-by-step derivation

   1. associate-*r/48.8%

      \[\leadsto \color{blue}{\frac{-1 \cdot v}{t1}} \]

   2. neg-mul-148.8%

      \[\leadsto \frac{\color{blue}{-v}}{t1} \]

6. Simplified48.8%

   \[\leadsto \color{blue}{\frac{-v}{t1}} \]

7. Final simplification48.8%

   \[\leadsto \frac{-v}{t1} \]

1. Initial program 73.2%

   \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)} \]
2. Step-by-step derivation

   1. associate-/l*75.0%

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

3. Simplified75.0%

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

4. Taylor expanded in t1 around inf 35.6%

   \[\leadsto \frac{-t1}{\color{blue}{\frac{{t1}^{2}}{v}}} \]
5. Step-by-step derivation

   1. unpow235.6%

      \[\leadsto \frac{-t1}{\frac{\color{blue}{t1 \cdot t1}}{v}} \]

6. Simplified35.6%

   \[\leadsto \frac{-t1}{\color{blue}{\frac{t1 \cdot t1}{v}}} \]
7. Step-by-step derivation

   1. div-inv35.5%

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

   2. clear-num35.2%

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

   3. add-sqr-sqrt15.3%

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

   4. sqrt-unprod10.8%

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

   5. sqr-neg10.8%

      \[\leadsto \sqrt{\color{blue}{t1 \cdot t1}} \cdot \frac{v}{t1 \cdot t1} \]

   6. sqrt-prod5.1%

      \[\leadsto \color{blue}{\left(\sqrt{t1} \cdot \sqrt{t1}\right)} \cdot \frac{v}{t1 \cdot t1} \]

   7. add-sqr-sqrt11.2%

      \[\leadsto \color{blue}{t1} \cdot \frac{v}{t1 \cdot t1} \]

8. Applied egg-rr11.2%

   \[\leadsto \color{blue}{t1 \cdot \frac{v}{t1 \cdot t1}} \]

9. Taylor expanded in t1 around 0 9.8%

   \[\leadsto \color{blue}{\frac{v}{t1}} \]

10. Final simplification9.8%

    \[\leadsto \frac{v}{t1} \]

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