Initial program 2.0
\[\left(\left(x + y \cdot z\right) + t \cdot a\right) + \left(a \cdot z\right) \cdot b
\]
Simplified2.6
\[\leadsto \color{blue}{\mathsf{fma}\left(a, t + z \cdot b, \mathsf{fma}\left(y, z, x\right)\right)}
\]
Proof
(fma.f64 a (+.f64 t (*.f64 z b)) (fma.f64 y z x)): 0 points increase in error, 0 points decrease in error
(fma.f64 a (+.f64 t (*.f64 z b)) (Rewrite<= fma-def_binary64 (+.f64 (*.f64 y z) x))): 0 points increase in error, 0 points decrease in error
(fma.f64 a (+.f64 t (*.f64 z b)) (Rewrite<= +-commutative_binary64 (+.f64 x (*.f64 y z)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-def_binary64 (+.f64 (*.f64 a (+.f64 t (*.f64 z b))) (+.f64 x (*.f64 y z)))): 5 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 a t) (*.f64 a (*.f64 z b)))) (+.f64 x (*.f64 y z))): 0 points increase in error, 5 points decrease in error
(+.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 t a)) (*.f64 a (*.f64 z b))) (+.f64 x (*.f64 y z))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 t a) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 a z) b))) (+.f64 x (*.f64 y z))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (+.f64 x (*.f64 y z)) (+.f64 (*.f64 t a) (*.f64 (*.f64 a z) b)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 x (*.f64 y z)) (*.f64 t a)) (*.f64 (*.f64 a z) b))): 0 points increase in error, 0 points decrease in error
Final simplification2.6
\[\leadsto \mathsf{fma}\left(a, t + z \cdot b, \mathsf{fma}\left(y, z, x\right)\right)
\]