Initial program 49.9
\[x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}
\]
Taylor expanded in z around inf 23.8
\[\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}}
\]
Simplified6.8
\[\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))))): 19 points increase in error, 33 points decrease in error
(-.f64 t (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 t x) (-.f64 y a)) z))): 30 points increase in error, 26 points decrease in error
(-.f64 t (/.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 y (-.f64 t x)) (*.f64 a (-.f64 t x)))) z)): 1 points increase in error, 0 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, 1 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-rr5.7
\[\leadsto t - \color{blue}{\frac{t - x}{\frac{z}{y - a}}}
\]
Initial program 17.6
\[x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}
\]
Simplified10.8
\[\leadsto \color{blue}{\mathsf{fma}\left(y - z, \frac{x - t}{z - a}, x\right)}
\]
Proof
(fma.f64 (-.f64 y z) (/.f64 (-.f64 x t) (-.f64 z a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (-.f64 x t)))) (-.f64 z a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (neg.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 x t)))) (-.f64 z a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (neg.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 x) t))) (-.f64 z a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (neg.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 x)) t)) (-.f64 z a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 t (neg.f64 x)))) (-.f64 z a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 t x))) (-.f64 z a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (neg.f64 (-.f64 t x)) (-.f64 z a)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (/.f64 (neg.f64 (-.f64 t x)) (-.f64 z a))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 -1 (neg.f64 (-.f64 t x))) (*.f64 -1 (-.f64 z a)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (neg.f64 (-.f64 t x)))) (*.f64 -1 (-.f64 z a))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (Rewrite=> remove-double-neg_binary64 (-.f64 t x)) (*.f64 -1 (-.f64 z a))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (-.f64 t x) (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 z a)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (-.f64 t x) (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 z a)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (-.f64 t x) (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 z) a))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (-.f64 t x) (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 z)) a)) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (-.f64 t x) (Rewrite<= +-commutative_binary64 (+.f64 a (neg.f64 z)))) x): 0 points increase in error, 0 points decrease in error
(fma.f64 (-.f64 y z) (/.f64 (-.f64 t x) (Rewrite<= sub-neg_binary64 (-.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)): 19 points increase in error, 22 points decrease in error
(+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (-.f64 y z) (-.f64 t x)) (-.f64 a z))) x): 77 points increase in error, 28 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 x (/.f64 (*.f64 (-.f64 y z) (-.f64 t x)) (-.f64 a z)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in t around 0 16.0
\[\leadsto \color{blue}{-1 \cdot \frac{t \cdot \left(y - z\right)}{z - a} + \left(\frac{\left(y - z\right) \cdot x}{z - a} + x\right)}
\]
Simplified8.3
\[\leadsto \color{blue}{x + \frac{y - z}{z - a} \cdot \left(x - t\right)}
\]
Proof
(+.f64 x (*.f64 (/.f64 (-.f64 y z) (-.f64 z a)) (-.f64 x t))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 (-.f64 y z) (-.f64 z a)) x) (*.f64 (/.f64 (-.f64 y z) (-.f64 z a)) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (-.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 y z) (/.f64 (-.f64 z a) x))) (*.f64 (/.f64 (-.f64 y z) (-.f64 z a)) t))): 11 points increase in error, 7 points decrease in error
(+.f64 x (-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a))) (*.f64 (/.f64 (-.f64 y z) (-.f64 z a)) t))): 44 points increase in error, 10 points decrease in error
(+.f64 x (-.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (Rewrite<= *-commutative_binary64 (*.f64 t (/.f64 (-.f64 y z) (-.f64 z a)))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (-.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (*.f64 t (Rewrite=> div-sub_binary64 (-.f64 (/.f64 y (-.f64 z a)) (/.f64 z (-.f64 z a))))))): 1 points increase in error, 2 points decrease in error
(+.f64 x (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (neg.f64 (*.f64 t (-.f64 (/.f64 y (-.f64 z a)) (/.f64 z (-.f64 z a)))))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 t (-.f64 (/.f64 y (-.f64 z a)) (/.f64 z (-.f64 z a)))))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 t (-.f64 (/.f64 y (-.f64 z a)) (/.f64 z (-.f64 z a)))))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite=> unsub-neg_binary64 (-.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (*.f64 t (-.f64 (/.f64 y (-.f64 z a)) (/.f64 z (-.f64 z a))))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (-.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (*.f64 t (Rewrite<= div-sub_binary64 (/.f64 (-.f64 y z) (-.f64 z a)))))): 2 points increase in error, 1 points decrease in error
(+.f64 x (-.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (-.f64 y z) (-.f64 z a)) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (-.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (-.f64 y z) t) (-.f64 z a))))): 36 points increase in error, 10 points decrease in error
(+.f64 x (-.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 t (-.f64 y z))) (-.f64 z a)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (neg.f64 (/.f64 (*.f64 t (-.f64 y z)) (-.f64 z a)))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 t (-.f64 y z)) (-.f64 z a)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 x (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a))) (*.f64 -1 (/.f64 (*.f64 t (-.f64 y z)) (-.f64 z a))))): 8 points increase in error, 13 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) x)) (*.f64 -1 (/.f64 (*.f64 t (-.f64 y z)) (-.f64 z a)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 t (-.f64 y z)) (-.f64 z a))) (+.f64 (/.f64 (*.f64 (-.f64 y z) x) (-.f64 z a)) x))): 0 points increase in error, 0 points decrease in error
Initial program 50.1
\[x + \frac{\left(y - z\right) \cdot \left(t - x\right)}{a - z}
\]
Taylor expanded in z around inf 23.7
\[\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}}
\]
Simplified8.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))))): 19 points increase in error, 33 points decrease in error
(-.f64 t (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 t x) (-.f64 y a)) z))): 30 points increase in error, 26 points decrease in error
(-.f64 t (/.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 y (-.f64 t x)) (*.f64 a (-.f64 t x)))) z)): 1 points increase in error, 0 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, 1 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
Taylor expanded in t around 0 19.7
\[\leadsto t - \color{blue}{-1 \cdot \frac{\left(y - a\right) \cdot x}{z}}
\]
Simplified10.5
\[\leadsto t - \color{blue}{x \cdot \frac{a - y}{z}}
\]
Proof
(*.f64 x (/.f64 (-.f64 a y) z)): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite=> div-sub_binary64 (-.f64 (/.f64 a z) (/.f64 y z)))): 1 points increase in error, 1 points decrease in error
(*.f64 x (Rewrite=> sub-neg_binary64 (+.f64 (/.f64 a z) (neg.f64 (/.f64 y z))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (/.f64 a z)))) (neg.f64 (/.f64 y z)))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 (/.f64 a z)) (/.f64 y z))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 y z) (neg.f64 (/.f64 a z)))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (neg.f64 (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 y z) (/.f64 a z))))): 0 points increase in error, 0 points decrease in error
(*.f64 x (neg.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 y a) z)))): 1 points increase in error, 1 points decrease in error
(*.f64 x (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 y a) z)))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite=> *-commutative_binary64 (*.f64 (/.f64 (-.f64 y a) z) -1))): 0 points increase in error, 0 points decrease in error
(*.f64 x (Rewrite<= associate-/r/_binary64 (/.f64 (-.f64 y a) (/.f64 z -1)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 x (-.f64 y a)) (/.f64 z -1))): 35 points increase in error, 52 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 y a) x)) (/.f64 z -1)): 0 points increase in error, 0 points decrease in error
(Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (*.f64 (-.f64 y a) x) z) -1)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 (*.f64 (-.f64 y a) x) z))): 0 points increase in error, 0 points decrease in error