Initial program 43.8
\[\frac{x + \frac{y \cdot z}{t}}{\left(a + 1\right) + \frac{y \cdot b}{t}}
\]
Simplified35.9
\[\leadsto \color{blue}{\frac{\mathsf{fma}\left(z, \frac{y}{t}, x\right)}{a + \mathsf{fma}\left(y, \frac{b}{t}, 1\right)}}
\]
Proof
(/.f64 (fma.f64 z (/.f64 y t) x) (+.f64 a (fma.f64 y (/.f64 b t) 1))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 z (/.f64 y t)) x)) (+.f64 a (fma.f64 y (/.f64 b t) 1))): 2 points increase in error, 1 points decrease in error
(/.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 y t) z)) x) (+.f64 a (fma.f64 y (/.f64 b t) 1))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 y z) t)) x) (+.f64 a (fma.f64 y (/.f64 b t) 1))): 17 points increase in error, 25 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 x (/.f64 (*.f64 y z) t))) (+.f64 a (fma.f64 y (/.f64 b t) 1))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (*.f64 y z) t)) (+.f64 a (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (/.f64 b t)) 1)))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (*.f64 y z) t)) (+.f64 a (+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 y b) t)) 1))): 14 points increase in error, 10 points decrease in error
(/.f64 (+.f64 x (/.f64 (*.f64 y z) t)) (+.f64 a (Rewrite<= +-commutative_binary64 (+.f64 1 (/.f64 (*.f64 y b) t))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 x (/.f64 (*.f64 y z) t)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 a 1) (/.f64 (*.f64 y b) t)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in y around inf 28.7
\[\leadsto \color{blue}{\left(\frac{t \cdot x}{y \cdot b} + \frac{z}{b}\right) - \frac{t \cdot \left(\left(1 + a\right) \cdot z\right)}{y \cdot {b}^{2}}}
\]
Simplified23.6
\[\leadsto \color{blue}{\frac{z}{b} + \frac{\frac{t}{b} \cdot x - \frac{\left(1 + a\right) \cdot \left(z \cdot t\right)}{b \cdot b}}{y}}
\]
Proof
(+.f64 (/.f64 z b) (/.f64 (-.f64 (*.f64 (/.f64 t b) x) (/.f64 (*.f64 (+.f64 1 a) (*.f64 z t)) (*.f64 b b))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (/.f64 (-.f64 (Rewrite<= associate-/r/_binary64 (/.f64 t (/.f64 b x))) (/.f64 (*.f64 (+.f64 1 a) (*.f64 z t)) (*.f64 b b))) y)): 12 points increase in error, 8 points decrease in error
(+.f64 (/.f64 z b) (/.f64 (-.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 t x) b)) (/.f64 (*.f64 (+.f64 1 a) (*.f64 z t)) (*.f64 b b))) y)): 8 points increase in error, 10 points decrease in error
(+.f64 (/.f64 z b) (/.f64 (-.f64 (/.f64 (*.f64 t x) b) (/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (+.f64 1 a) z) t)) (*.f64 b b))) y)): 14 points increase in error, 2 points decrease in error
(+.f64 (/.f64 z b) (/.f64 (-.f64 (/.f64 (*.f64 t x) b) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 t (*.f64 (+.f64 1 a) z))) (*.f64 b b))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (/.f64 (-.f64 (/.f64 (*.f64 t x) b) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (Rewrite<= unpow2_binary64 (pow.f64 b 2)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (/.f64 (*.f64 t x) b) y) (/.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (-.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 t x) (*.f64 b y))) (/.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) y))): 7 points increase in error, 7 points decrease in error
(+.f64 (/.f64 z b) (-.f64 (/.f64 (*.f64 t x) (Rewrite<= *-commutative_binary64 (*.f64 y b))) (/.f64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (pow.f64 b 2)) y))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 z b) (-.f64 (/.f64 (*.f64 t x) (*.f64 y b)) (Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (*.f64 (pow.f64 b 2) y))))): 5 points increase in error, 6 points decrease in error
(+.f64 (/.f64 z b) (-.f64 (/.f64 (*.f64 t x) (*.f64 y b)) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (Rewrite<= *-commutative_binary64 (*.f64 y (pow.f64 b 2)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 z b) (/.f64 (*.f64 t x) (*.f64 y b))) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (*.f64 y (pow.f64 b 2))))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 (*.f64 t x) (*.f64 y b)) (/.f64 z b))) (/.f64 (*.f64 t (*.f64 (+.f64 1 a) z)) (*.f64 y (pow.f64 b 2)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in a around 0 21.9
\[\leadsto \frac{z}{b} + \frac{\color{blue}{\frac{t \cdot x}{b} - \frac{t \cdot z}{{b}^{2}}}}{y}
\]
Simplified18.1
\[\leadsto \frac{z}{b} + \frac{\color{blue}{\frac{t}{b} \cdot \left(x - \frac{z}{b}\right)}}{y}
\]
Proof
(*.f64 (/.f64 t b) (-.f64 x (/.f64 z b))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 (/.f64 t b) x) (*.f64 (/.f64 t b) (/.f64 z b)))): 1 points increase in error, 0 points decrease in error
(-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 t x) b)) (*.f64 (/.f64 t b) (/.f64 z b))): 32 points increase in error, 18 points decrease in error
(-.f64 (/.f64 (*.f64 t x) b) (Rewrite<= times-frac_binary64 (/.f64 (*.f64 t z) (*.f64 b b)))): 29 points increase in error, 18 points decrease in error
(-.f64 (/.f64 (*.f64 t x) b) (/.f64 (*.f64 t z) (Rewrite<= unpow2_binary64 (pow.f64 b 2)))): 0 points increase in error, 0 points decrease in error
Taylor expanded in b around inf 19.1
\[\leadsto \frac{z}{b} + \frac{\color{blue}{\frac{t \cdot x}{b}}}{y}
\]
Simplified17.8
\[\leadsto \frac{z}{b} + \frac{\color{blue}{\frac{x}{\frac{b}{t}}}}{y}
\]
Proof
(/.f64 x (/.f64 b t)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 x t) b)): 44 points increase in error, 44 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 t x)) b): 0 points increase in error, 0 points decrease in error