Initial program 39.5
\[\frac{x - y \cdot z}{t - a \cdot z}
\]
Simplified39.5
\[\leadsto \color{blue}{\frac{x - y \cdot z}{t - z \cdot a}}
\]
Proof
(/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (*.f64 z a))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (*.f64 y z)) (-.f64 t (Rewrite<= *-commutative_binary64 (*.f64 a z)))): 0 points increase in error, 0 points decrease in error
Applied egg-rr30.1
\[\leadsto \color{blue}{\frac{x}{t - z \cdot a} - \frac{y}{\frac{t - z \cdot a}{z}}}
\]
Taylor expanded in x around 0 40.3
\[\leadsto \color{blue}{-1 \cdot \frac{y \cdot z}{t - a \cdot z}}
\]
Simplified7.2
\[\leadsto \color{blue}{\frac{-y}{\frac{t}{z} - a}}
\]
Proof
(/.f64 (neg.f64 y) (-.f64 (/.f64 t z) a)): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 y) (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 t z) (neg.f64 a)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 y) (+.f64 (/.f64 t z) (Rewrite<= mul-1-neg_binary64 (*.f64 -1 a)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 y) (+.f64 (/.f64 t z) (*.f64 (Rewrite<= metadata-eval (neg.f64 1)) a))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 y) (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 (/.f64 t z) (*.f64 1 a)))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 y) (-.f64 (/.f64 t z) (*.f64 (Rewrite<= *-inverses_binary64 (/.f64 z z)) a))): 0 points increase in error, 0 points decrease in error
(/.f64 (neg.f64 y) (-.f64 (/.f64 t z) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 z a) z)))): 41 points increase in error, 3 points decrease in error
(/.f64 (neg.f64 y) (Rewrite<= div-sub_binary64 (/.f64 (-.f64 t (*.f64 z a)) z))): 1 points increase in error, 1 points decrease in error
(Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 y (/.f64 (-.f64 t (*.f64 z a)) z)))): 0 points increase in error, 0 points decrease in error
(neg.f64 (/.f64 y (/.f64 (-.f64 t (Rewrite<= *-commutative_binary64 (*.f64 a z))) z))): 0 points increase in error, 0 points decrease in error
(neg.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y z) (-.f64 t (*.f64 a z))))): 57 points increase in error, 31 points decrease in error
(Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 y z) (-.f64 t (*.f64 a z))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in y around 0 7.2
\[\leadsto \color{blue}{-1 \cdot \frac{y}{\frac{t}{z} - a}}
\]
Simplified7.2
\[\leadsto \color{blue}{\frac{y}{a - \frac{t}{z}}}
\]
Proof
(/.f64 y (-.f64 a (/.f64 t z))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 y 1)) (-.f64 a (/.f64 t z))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 y 1) (Rewrite<= unsub-neg_binary64 (+.f64 a (neg.f64 (/.f64 t z))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 y 1) (+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 a))) (neg.f64 (/.f64 t z)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 y 1) (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (neg.f64 a) (/.f64 t z))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 y 1) (neg.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 t z) (neg.f64 a))))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 y 1) (neg.f64 (Rewrite=> unsub-neg_binary64 (-.f64 (/.f64 t z) a)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 y (/.f64 1 (neg.f64 (-.f64 (/.f64 t z) a))))): 38 points increase in error, 14 points decrease in error
(*.f64 y (/.f64 1 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 (/.f64 t z) a))))): 0 points increase in error, 0 points decrease in error
(*.f64 y (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 1 -1) (-.f64 (/.f64 t z) a)))): 0 points increase in error, 0 points decrease in error
(*.f64 y (/.f64 (Rewrite=> metadata-eval -1) (-.f64 (/.f64 t z) a))): 0 points increase in error, 0 points decrease in error
(*.f64 y (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) (-.f64 (/.f64 t z) a))): 0 points increase in error, 0 points decrease in error
(*.f64 y (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 1 (-.f64 (/.f64 t z) a))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y (/.f64 1 (-.f64 (/.f64 t z) a))))): 0 points increase in error, 0 points decrease in error
(neg.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 y 1) (-.f64 (/.f64 t z) a)))): 14 points increase in error, 38 points decrease in error
(neg.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 y (-.f64 (/.f64 t z) a)) 1))): 0 points increase in error, 0 points decrease in error
(neg.f64 (Rewrite=> *-rgt-identity_binary64 (/.f64 y (-.f64 (/.f64 t z) a)))): 0 points increase in error, 0 points decrease in error
(Rewrite=> neg-mul-1_binary64 (*.f64 -1 (/.f64 y (-.f64 (/.f64 t z) a)))): 0 points increase in error, 0 points decrease in error
Initial program 0.2
\[\frac{x - y \cdot z}{t - a \cdot z}
\]
Simplified0.2
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(z, -y, x\right)}{\mathsf{fma}\left(z, -a, t\right)}}
\]
Proof
(/.f64 (fma.f64 z (neg.f64 y) x) (fma.f64 z (neg.f64 a) t)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z (neg.f64 y)) x)) (fma.f64 z (neg.f64 a) t)): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 y) z)) x) (fma.f64 z (neg.f64 a) t)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x (*.f64 (neg.f64 y) z))) (fma.f64 z (neg.f64 a) t)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 x (*.f64 y z))) (fma.f64 z (neg.f64 a) t)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (*.f64 y z)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z (neg.f64 a)) t))): 2 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (*.f64 y z)) (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (neg.f64 a) z)) t)): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (*.f64 y z)) (Rewrite<= +-commutative_binary64 (+.f64 t (*.f64 (neg.f64 a) z)))): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 x (*.f64 y z)) (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 t (*.f64 a z)))): 0 points increase in error, 0 points decrease in error