Simplified10.2
\[\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)): 25 points increase in error, 25 points decrease in error
(+.f64 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 (-.f64 y z) (-.f64 t x)) (-.f64 a z))) x): 95 points increase in error, 38 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
Simplified5.9
\[\leadsto \color{blue}{x \cdot \left(1 + \frac{y - z}{z - a}\right) - t \cdot \frac{y - z}{z - a}}
\]
Proof
(-.f64 (*.f64 x (+.f64 1 (/.f64 (-.f64 y z) (-.f64 z a)))) (*.f64 t (/.f64 (-.f64 y z) (-.f64 z a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 x (+.f64 1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 y (-.f64 z a)) (/.f64 z (-.f64 z a)))))) (*.f64 t (/.f64 (-.f64 y z) (-.f64 z a)))): 0 points increase in error, 1 points decrease in error
(-.f64 (*.f64 x (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 1 (/.f64 y (-.f64 z a))) (/.f64 z (-.f64 z a))))) (*.f64 t (/.f64 (-.f64 y z) (-.f64 z a)))): 0 points increase in error, 1 points decrease in error
(-.f64 (*.f64 x (-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (/.f64 y (-.f64 z a)) 1)) (/.f64 z (-.f64 z a)))) (*.f64 t (/.f64 (-.f64 y z) (-.f64 z a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 (+.f64 (/.f64 y (-.f64 z a)) 1) (/.f64 z (-.f64 z a))) x)) (*.f64 t (/.f64 (-.f64 y z) (-.f64 z a)))): 0 points increase in error, 0 points decrease in error
(-.f64 (*.f64 (-.f64 (+.f64 (/.f64 y (-.f64 z a)) 1) (/.f64 z (-.f64 z a))) x) (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 t (-.f64 y z)) (-.f64 z a)))): 60 points increase in error, 13 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (*.f64 (-.f64 (+.f64 (/.f64 y (-.f64 z a)) 1) (/.f64 z (-.f64 z a))) x) (neg.f64 (/.f64 (*.f64 t (-.f64 y z)) (-.f64 z a))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (-.f64 (+.f64 (/.f64 y (-.f64 z a)) 1) (/.f64 z (-.f64 z a))) x) (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<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 t (-.f64 y z)) (-.f64 z a))) (*.f64 (-.f64 (+.f64 (/.f64 y (-.f64 z a)) 1) (/.f64 z (-.f64 z a))) x))): 0 points increase in error, 0 points decrease in error