Initial program 7.3
\[x + \left(y - z\right) \cdot \frac{t - x}{a - z}
\]
Simplified3.9
\[\leadsto \color{blue}{\mathsf{fma}\left(t - x, \frac{y - z}{a - z}, x\right)}
\]
Proof
(fma.f64 (-.f64 t x) (/.f64 (-.f64 y z) (-.f64 a z)) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 (-.f64 t x) (/.f64 (-.f64 y z) (-.f64 a z))) x)): 0 points increase in error, 1 points decrease in error
(+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (-.f64 t x) (-.f64 y z)) (-.f64 a z))) x): 94 points increase in error, 23 points decrease in error
(+.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 y z) (-.f64 t x))) (-.f64 a z)) x): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (-.f64 y z) (/.f64 (-.f64 t x) (-.f64 a z)))) x): 36 points increase in error, 97 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
Initial program 60.7
\[x + \left(y - z\right) \cdot \frac{t - x}{a - z}
\]
Taylor expanded in z around inf 11.4
\[\leadsto \color{blue}{\left(-1 \cdot \frac{y \cdot \left(t - x\right)}{z} + t\right) - -1 \cdot \frac{a \cdot \left(t - x\right)}{z}}
\]
Simplified1.5
\[\leadsto \color{blue}{t - \frac{t - x}{z} \cdot \left(y - a\right)}
\]
Proof
(-.f64 t (*.f64 (/.f64 (-.f64 t x) z) (-.f64 y a))): 0 points increase in error, 0 points decrease in error
(-.f64 t (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 t x) (/.f64 z (-.f64 y a))))): 33 points increase in error, 22 points decrease in error
(-.f64 t (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 t x) (-.f64 y a)) z))): 43 points increase in error, 21 points decrease in error
(-.f64 t (/.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 y (-.f64 t x)) (*.f64 a (-.f64 t x)))) z)): 2 points increase in error, 2 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 t (neg.f64 (/.f64 (-.f64 (*.f64 y (-.f64 t x)) (*.f64 a (-.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 y (-.f64 t x)) (*.f64 a (-.f64 t x))) z)))): 0 points increase in error, 0 points decrease in error
(+.f64 t (*.f64 -1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 y (-.f64 t x)) z) (/.f64 (*.f64 a (-.f64 t x)) z))))): 0 points increase in error, 3 points decrease in error
(+.f64 t (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y (-.f64 t x)) z)) (*.f64 -1 (/.f64 (*.f64 a (-.f64 t x)) z))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 t (*.f64 -1 (/.f64 (*.f64 y (-.f64 t x)) z))) (*.f64 -1 (/.f64 (*.f64 a (-.f64 t x)) z)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 y (-.f64 t x)) z)) t)) (*.f64 -1 (/.f64 (*.f64 a (-.f64 t x)) z))): 0 points increase in error, 0 points decrease in error
Applied egg-rr2.8
\[\leadsto t - \color{blue}{\frac{t - x}{\frac{z}{y - a}}}
\]
Taylor expanded in t around 0 11.4
\[\leadsto t - \color{blue}{-1 \cdot \frac{\left(y - a\right) \cdot x}{z}}
\]
Simplified1.5
\[\leadsto t - \color{blue}{\frac{x}{z} \cdot \left(a - y\right)}
\]
Proof
(*.f64 (/.f64 x z) (-.f64 a y)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 x z) (Rewrite<= unsub-neg_binary64 (+.f64 a (neg.f64 y)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 x z) (+.f64 a (Rewrite=> neg-mul-1_binary64 (*.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 x z) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 y) a))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 x z) (+.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 y)) a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 x z) (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 y)) a)): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 x z) (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 y a)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 x z) (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 y a)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (/.f64 x z) (-.f64 y a)))): 0 points increase in error, 0 points decrease in error
(neg.f64 (Rewrite<= associate-/r/_binary64 (/.f64 x (/.f64 z (-.f64 y a))))): 51 points increase in error, 55 points decrease in error
(neg.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x (-.f64 y a)) z))): 44 points increase in error, 40 points decrease in error
(neg.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 y a) x)) z)): 0 points increase in error, 0 points decrease in error
(Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 y a) x) z))): 0 points increase in error, 0 points decrease in error