if (+ x (* (/ (- y z) (- (+ t 1.0) z)) (- a x))) < -1.4776331f-37 or 0.0f0 < (+ x (* (/ (- y z) (- (+ t 1.0) z)) (- a x)))

1. Started with
   \[x + \frac{y - z}{\left(t + 1.0\right) - z} \cdot \left(a - x\right)\]
   0.9
2. Applied simplify to get
   \[\color{red}{x + \frac{y - z}{\left(t + 1.0\right) - z} \cdot \left(a - x\right)} \leadsto \color{blue}{(\left(a - x\right) * \left(\frac{y - z}{\left(1.0 + t\right) - z}\right) + x)_*}\]
   0.9
3. Using strategy rm
   0.9
4. Applied fma-udef to get
   \[\color{red}{(\left(a - x\right) * \left(\frac{y - z}{\left(1.0 + t\right) - z}\right) + x)_*} \leadsto \color{blue}{\left(a - x\right) \cdot \frac{y - z}{\left(1.0 + t\right) - z} + x}\]
   0.9
5. Using strategy rm
   0.9
6. Applied pow1 to get
   \[\left(a - x\right) \cdot \frac{y - z}{\color{red}{\left(1.0 + t\right) - z}} + x \leadsto \left(a - x\right) \cdot \frac{y - z}{\color{blue}{{\left(\left(1.0 + t\right) - z\right)}^{1}}} + x\]
   0.7

if -1.4776331f-37 < (+ x (* (/ (- y z) (- (+ t 1.0) z)) (- a x))) < 0.0f0

1. Started with
   \[x + \frac{y - z}{\left(t + 1.0\right) - z} \cdot \left(a - x\right)\]
   29.5
2. Applied simplify to get
   \[\color{red}{x + \frac{y - z}{\left(t + 1.0\right) - z} \cdot \left(a - x\right)} \leadsto \color{blue}{(\left(a - x\right) * \left(\frac{y - z}{\left(1.0 + t\right) - z}\right) + x)_*}\]
   29.5
3. Using strategy rm
   29.5
4. Applied fma-udef to get
   \[\color{red}{(\left(a - x\right) * \left(\frac{y - z}{\left(1.0 + t\right) - z}\right) + x)_*} \leadsto \color{blue}{\left(a - x\right) \cdot \frac{y - z}{\left(1.0 + t\right) - z} + x}\]
   29.5
5. Using strategy rm
   29.5
6. Applied add-sqr-sqrt to get
   \[\left(a - x\right) \cdot \frac{y - z}{\color{red}{\left(1.0 + t\right) - z}} + x \leadsto \left(a - x\right) \cdot \frac{y - z}{\color{blue}{{\left(\sqrt{\left(1.0 + t\right) - z}\right)}^2}} + x\]
   29.9
7. Applied add-sqr-sqrt to get
   \[\left(a - x\right) \cdot \frac{\color{red}{y - z}}{{\left(\sqrt{\left(1.0 + t\right) - z}\right)}^2} + x \leadsto \left(a - x\right) \cdot \frac{\color{blue}{{\left(\sqrt{y - z}\right)}^2}}{{\left(\sqrt{\left(1.0 + t\right) - z}\right)}^2} + x\]
   30.2
8. Applied square-undiv to get
   \[\left(a - x\right) \cdot \color{red}{\frac{{\left(\sqrt{y - z}\right)}^2}{{\left(\sqrt{\left(1.0 + t\right) - z}\right)}^2}} + x \leadsto \left(a - x\right) \cdot \color{blue}{{\left(\frac{\sqrt{y - z}}{\sqrt{\left(1.0 + t\right) - z}}\right)}^2} + x\]
   30.2
9. Applied taylor to get
   \[\left(a - x\right) \cdot {\left(\frac{\sqrt{y - z}}{\sqrt{\left(1.0 + t\right) - z}}\right)}^2 + x \leadsto \left(a - \left(1.0 \cdot \frac{x}{z} + x\right)\right) + x\]
   29.1
10. Taylor expanded around inf to get
    \[\color{red}{\left(a - \left(1.0 \cdot \frac{x}{z} + x\right)\right)} + x \leadsto \color{blue}{\left(a - \left(1.0 \cdot \frac{x}{z} + x\right)\right)} + x\]
    29.1
11. Applied simplify to get
    \[\left(a - \left(1.0 \cdot \frac{x}{z} + x\right)\right) + x \leadsto a - (1.0 * \left(\frac{x}{z}\right) + 0)_*\]
    12.0

---

12. Applied final simplification