Initial program 52.4
\[x + \left(y - z\right) \cdot \frac{t - x}{a - z}
\]
Simplified52.1
\[\leadsto \color{blue}{\mathsf{fma}\left(y - z, \frac{t - x}{a - z}, x\right)}
\]
Proof
(fma.f64 (-.f64 y z) (/.f64 (-.f64 t x) (-.f64 a z)) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (-.f64 y z) (/.f64 (-.f64 t x) (-.f64 a z))) x)): 0 points increase in error, 3 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 x (*.f64 (-.f64 y z) (/.f64 (-.f64 t x) (-.f64 a z))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in z around -inf 18.5
\[\leadsto \color{blue}{-1 \cdot \frac{-1 \cdot \left(a \cdot \left(t - x\right)\right) + y \cdot \left(t - x\right)}{z} + t}
\]
Simplified11.5
\[\leadsto \color{blue}{t - \frac{t - x}{\frac{z}{y + \left(-a\right)}}}
\]
Proof
(-.f64 t (/.f64 (-.f64 t x) (/.f64 z (+.f64 y (neg.f64 a))))): 0 points increase in error, 0 points decrease in error
(-.f64 t (/.f64 (-.f64 t x) (/.f64 z (+.f64 y (Rewrite<= mul-1-neg_binary64 (*.f64 -1 a)))))): 0 points increase in error, 0 points decrease in error
(-.f64 t (/.f64 (-.f64 t x) (/.f64 z (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 a) y))))): 9 points increase in error, 0 points decrease in error
(-.f64 t (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 t x) (+.f64 (*.f64 -1 a) y)) z))): 0 points increase in error, 3 points decrease in error
(-.f64 t (/.f64 (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (*.f64 -1 a) (-.f64 t x)) (*.f64 y (-.f64 t x)))) z)): 3 points increase in error, 0 points decrease in error
(-.f64 t (/.f64 (+.f64 (Rewrite<= associate-*r*_binary64 (*.f64 -1 (*.f64 a (-.f64 t x)))) (*.f64 y (-.f64 t x))) z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 t (neg.f64 (/.f64 (+.f64 (*.f64 -1 (*.f64 a (-.f64 t x))) (*.f64 y (-.f64 t x))) z)))): 0 points increase in error, 0 points decrease in error
(+.f64 t (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (+.f64 (*.f64 -1 (*.f64 a (-.f64 t x))) (*.f64 y (-.f64 t x))) z)))): 0 points increase in error, 9 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (+.f64 (*.f64 -1 (*.f64 a (-.f64 t x))) (*.f64 y (-.f64 t x))) z)) t)): 9 points increase in error, 0 points decrease in error
Taylor expanded in z around 0 18.5
\[\leadsto t - \color{blue}{\frac{\left(y - a\right) \cdot \left(t - x\right)}{z}}
\]
Simplified11.0
\[\leadsto t - \color{blue}{\left(y - a\right) \cdot \frac{t - x}{z}}
\]
Proof
(-.f64 t (*.f64 (-.f64 y a) (/.f64 (-.f64 t x) z))): 0 points increase in error, 0 points decrease in error
(-.f64 t (*.f64 (Rewrite=> sub-neg_binary64 (+.f64 y (neg.f64 a))) (/.f64 (-.f64 t x) z))): 0 points increase in error, 0 points decrease in error
(-.f64 t (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 (neg.f64 a) y)) (/.f64 (-.f64 t x) z))): 12 points increase in error, 0 points decrease in error
(-.f64 t (*.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 a)) y) (/.f64 (-.f64 t x) z))): 0 points increase in error, 6 points decrease in error
(-.f64 t (*.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 a y))) (/.f64 (-.f64 t x) z))): 6 points increase in error, 0 points decrease in error
(-.f64 t (*.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 a y))) (/.f64 (-.f64 t x) z))): 0 points increase in error, 0 points decrease in error
(-.f64 t (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (neg.f64 (-.f64 a y)) (-.f64 t x)) z))): 0 points increase in error, 0 points decrease in error
(-.f64 t (/.f64 (*.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (-.f64 a y))) (-.f64 t x)) z)): 0 points increase in error, 12 points decrease in error
(-.f64 t (/.f64 (*.f64 (Rewrite=> associate--r-_binary64 (+.f64 (-.f64 0 a) y)) (-.f64 t x)) z)): 12 points increase in error, 0 points decrease in error
(-.f64 t (/.f64 (*.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 a)) y) (-.f64 t x)) z)): 0 points increase in error, 6 points decrease in error
(-.f64 t (/.f64 (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 y (neg.f64 a))) (-.f64 t x)) z)): 6 points increase in error, 0 points decrease in error
(-.f64 t (/.f64 (*.f64 (Rewrite<= sub-neg_binary64 (-.f64 y a)) (-.f64 t x)) z)): 0 points increase in error, 0 points decrease in error
Taylor expanded in t around 0 19.0
\[\leadsto t - \color{blue}{-1 \cdot \frac{\left(y - a\right) \cdot x}{z}}
\]
Simplified11.0
\[\leadsto t - \color{blue}{\left(y - a\right) \cdot \frac{-x}{z}}
\]
Proof
(-.f64 t (*.f64 (-.f64 y a) (/.f64 (neg.f64 x) z))): 0 points increase in error, 0 points decrease in error
(-.f64 t (*.f64 (-.f64 y a) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 x z))))): 0 points increase in error, 0 points decrease in error
(-.f64 t (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (-.f64 y a) (/.f64 x z))))): 5 points increase in error, 0 points decrease in error
(-.f64 t (neg.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (-.f64 y a) x) z)))): 0 points increase in error, 3 points decrease in error
(-.f64 t (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 y a) x) z)))): 3 points increase in error, 0 points decrease in error