Simplified18.6
\[\leadsto \color{blue}{x + \mathsf{fma}\left(y, \frac{z - t}{t - a}, y\right)}
\]
Proof
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (-.f64 t a)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= *-lft-identity_binary64 (*.f64 1 (-.f64 t a)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (*.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (-.f64 t a))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 -1 (-.f64 t a))))) y)): 6 points increase in error, 6 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (-.f64 t a)) -1))) y)): 6 points increase in error, 6 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (-.f64 t a))) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= sub0-neg_binary64 (-.f64 0 (-.f64 t a))) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= associate-+l-_binary64 (+.f64 (-.f64 0 t) a)) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (+.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 t)) a) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 a (neg.f64 t))) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (/.f64 (-.f64 z t) (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 a t)) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (-.f64 z t) (-.f64 a t)) -1)) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (Rewrite<= *-commutative_binary64 (*.f64 -1 (/.f64 (-.f64 z t) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (fma.f64 y (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (-.f64 z t) (-.f64 a t)))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y (neg.f64 (/.f64 (-.f64 z t) (-.f64 a t)))) y))): 1 points increase in error, 1 points decrease in error
(+.f64 x (+.f64 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 y (/.f64 (-.f64 z t) (-.f64 a t))))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 (-.f64 z t) (-.f64 a t)) y))) y)): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (neg.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))) y)): 49 points increase in error, 10 points decrease in error
(+.f64 x (Rewrite<= +-commutative_binary64 (+.f64 y (neg.f64 (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= sub-neg_binary64 (-.f64 y (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 x y) (/.f64 (*.f64 (-.f64 z t) y) (-.f64 a t)))): 21 points increase in error, 7 points decrease in error
Simplified19.8
\[\leadsto \color{blue}{\frac{y}{t} \cdot \left(z - a\right) + x}
\]
Proof
(+.f64 (*.f64 (/.f64 y t) (-.f64 z a)) x): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 y (-.f64 z a)) t)) x): 27 points increase in error, 20 points decrease in error
(+.f64 (/.f64 (*.f64 y (-.f64 z a)) t) (Rewrite<= +-lft-identity_binary64 (+.f64 0 x))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 y (-.f64 z a)) t) (+.f64 (Rewrite<= mul0-lft_binary64 (*.f64 0 y)) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 y (-.f64 z a)) t) (+.f64 (*.f64 (Rewrite<= metadata-eval (+.f64 -1 1)) y) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 y (-.f64 z a)) t) (+.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 y (*.f64 -1 y))) x)): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 y (-.f64 z a)) t) (Rewrite=> associate-+l+_binary64 (+.f64 y (+.f64 (*.f64 -1 y) x)))): 23 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (*.f64 y (-.f64 z a)) t) (Rewrite=> +-commutative_binary64 (+.f64 (+.f64 (*.f64 -1 y) x) y))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (/.f64 (*.f64 y (-.f64 z a)) t) (+.f64 (*.f64 -1 y) x)) y)): 27 points increase in error, 11 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 y (+.f64 (/.f64 (*.f64 y (-.f64 z a)) t) (+.f64 (*.f64 -1 y) x)))): 0 points increase in error, 0 points decrease in error