Initial program 8.0
\[x + \left(y - z\right) \cdot \frac{t - x}{a - z}
\]
Simplified4.3
\[\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)): 4 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): 90 points increase in error, 14 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): 35 points increase in error, 85 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 61.8
\[x + \left(y - z\right) \cdot \frac{t - x}{a - z}
\]
Simplified61.8
\[\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)): 4 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): 90 points increase in error, 14 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): 35 points increase in error, 85 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 11.0
\[\leadsto \color{blue}{\frac{\left(-1 \cdot y - -1 \cdot a\right) \cdot \left(t - x\right)}{z} + t}
\]
Simplified1.7
\[\leadsto \color{blue}{t + \frac{a - y}{z} \cdot \left(t - x\right)}
\]
Proof
(+.f64 t (*.f64 (/.f64 (-.f64 a y) z) (-.f64 t x))): 0 points increase in error, 0 points decrease in error
(+.f64 t (*.f64 (/.f64 (Rewrite<= unsub-neg_binary64 (+.f64 a (neg.f64 y))) z) (-.f64 t x))): 0 points increase in error, 0 points decrease in error
(+.f64 t (*.f64 (/.f64 (+.f64 a (Rewrite<= mul-1-neg_binary64 (*.f64 -1 y))) z) (-.f64 t x))): 0 points increase in error, 0 points decrease in error
(+.f64 t (*.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 y) a)) z) (-.f64 t x))): 0 points increase in error, 0 points decrease in error
(+.f64 t (*.f64 (/.f64 (+.f64 (*.f64 -1 y) (Rewrite<= *-lft-identity_binary64 (*.f64 1 a))) z) (-.f64 t x))): 0 points increase in error, 0 points decrease in error
(+.f64 t (*.f64 (/.f64 (+.f64 (*.f64 -1 y) (*.f64 (Rewrite<= metadata-eval (neg.f64 -1)) a)) z) (-.f64 t x))): 0 points increase in error, 0 points decrease in error
(+.f64 t (*.f64 (/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (*.f64 -1 y) (*.f64 -1 a))) z) (-.f64 t x))): 0 points increase in error, 0 points decrease in error
(+.f64 t (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 (*.f64 -1 y) (*.f64 -1 a)) (/.f64 z (-.f64 t x))))): 30 points increase in error, 26 points decrease in error
(+.f64 t (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 (*.f64 -1 y) (*.f64 -1 a)) (-.f64 t x)) z))): 39 points increase in error, 27 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 (-.f64 (*.f64 -1 y) (*.f64 -1 a)) (-.f64 t x)) z) t)): 0 points increase in error, 0 points decrease in error
Taylor expanded in t around 0 11.0
\[\leadsto t + \color{blue}{-1 \cdot \frac{x \cdot \left(a - y\right)}{z}}
\]
Simplified0.2
\[\leadsto t + \color{blue}{\frac{a - y}{\frac{z}{-x}}}
\]
Proof
(/.f64 (-.f64 a y) (/.f64 z (neg.f64 x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 a y) (neg.f64 x)) z)): 47 points increase in error, 45 points decrease in error
(/.f64 (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 (-.f64 a y) x))) z): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (-.f64 a y) x))) z): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 -1 (Rewrite=> *-commutative_binary64 (*.f64 x (-.f64 a y)))) z): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 x (-.f64 a y)) z))): 0 points increase in error, 0 points decrease in error