Simplified12.7
\[\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-/r/_binary64 (/.f64 y (/.f64 t (-.f64 z a)))) x): 27 points increase in error, 23 points decrease in error
(+.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 y (-.f64 z a)) t)) x): 35 points increase in error, 29 points decrease in error
(+.f64 (/.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 y z) (*.f64 y a))) t) x): 2 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (/.f64 (-.f64 (*.f64 y z) (*.f64 y a)) t)))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 (*.f64 y z) (*.f64 y a)) t)))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (*.f64 -1 (/.f64 (-.f64 (*.f64 y z) (*.f64 y a)) t)))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (Rewrite=> associate-*r/_binary64 (/.f64 (*.f64 -1 (-.f64 (*.f64 y z) (*.f64 y a))) t))) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (*.f64 y z)) (*.f64 -1 (*.f64 y a)))) t)) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 (*.f64 -1 (*.f64 y z)) (*.f64 (neg.f64 -1) (*.f64 y a)))) t)) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (+.f64 (*.f64 -1 (*.f64 y z)) (*.f64 (Rewrite=> metadata-eval 1) (*.f64 y a))) t)) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (+.f64 (*.f64 -1 (*.f64 y z)) (Rewrite=> *-lft-identity_binary64 (*.f64 y a))) t)) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 y a) (*.f64 -1 (*.f64 y z)))) t)) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (+.f64 (*.f64 y a) (Rewrite=> mul-1-neg_binary64 (neg.f64 (*.f64 y z)))) t)) x): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 -1 (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 (*.f64 y a) (*.f64 y z))) t)) x): 0 points increase in error, 0 points decrease in error
(Rewrite=> +-commutative_binary64 (+.f64 x (*.f64 -1 (/.f64 (-.f64 (*.f64 y a) (*.f64 y z)) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite=> mul-1-neg_binary64 (neg.f64 (/.f64 (-.f64 (*.f64 y a) (*.f64 y z)) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (-.f64 (*.f64 y a) (*.f64 y z)) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (*.f64 -1 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 (*.f64 y a) t) (/.f64 (*.f64 y z) t))))): 0 points increase in error, 2 points decrease in error
(+.f64 x (Rewrite<= distribute-lft-out--_binary64 (-.f64 (*.f64 -1 (/.f64 (*.f64 y a) t)) (*.f64 -1 (/.f64 (*.f64 y z) t))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite=> cancel-sign-sub-inv_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 y a) t)) (*.f64 (neg.f64 -1) (/.f64 (*.f64 y z) t))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (*.f64 -1 (/.f64 (*.f64 y a) t)) (*.f64 (Rewrite=> metadata-eval 1) (/.f64 (*.f64 y z) t)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (+.f64 (*.f64 -1 (/.f64 (*.f64 y a) t)) (Rewrite=> *-lft-identity_binary64 (/.f64 (*.f64 y z) t)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 x (*.f64 -1 (/.f64 (*.f64 y a) t))) (/.f64 (*.f64 y z) t))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 -1 (/.f64 (*.f64 y a) t)) x)) (/.f64 (*.f64 y z) t)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (/.f64 (*.f64 y a) t)) x) (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (/.f64 (*.f64 y z) t))))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 -1 (/.f64 (*.f64 y a) t)) x) (neg.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (/.f64 (*.f64 y z) t))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub-neg_binary64 (-.f64 (+.f64 (*.f64 -1 (/.f64 (*.f64 y a) t)) x) (*.f64 -1 (/.f64 (*.f64 y z) t)))): 0 points increase in error, 0 points decrease in error