Initial program 6.5
\[2 \cdot \left(\left(x \cdot y + z \cdot t\right) - \left(\left(a + b \cdot c\right) \cdot c\right) \cdot i\right)\]
Simplified1.9
\[\leadsto \color{blue}{\mathsf{fma}\left(2, \mathsf{fma}\left(x, y, z \cdot t\right), 2 \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)}\]
Taylor expanded around inf 1.9
\[\leadsto \mathsf{fma}\left(2, \color{blue}{t \cdot z + x \cdot y}, 2 \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)\]
Simplified1.9
\[\leadsto \mathsf{fma}\left(2, \color{blue}{\mathsf{fma}\left(t, z, x \cdot y\right)}, 2 \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)\]
- Using strategy
rm Applied add-sqr-sqrt2.2
\[\leadsto \mathsf{fma}\left(2, \mathsf{fma}\left(t, z, x \cdot y\right), \color{blue}{\left(\sqrt{2} \cdot \sqrt{2}\right)} \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)\]
Applied associate-*l*2.1
\[\leadsto \mathsf{fma}\left(2, \mathsf{fma}\left(t, z, x \cdot y\right), \color{blue}{\sqrt{2} \cdot \left(\sqrt{2} \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)}\right)\]
- Using strategy
rm Applied add-sqr-sqrt2.1
\[\leadsto \mathsf{fma}\left(2, \mathsf{fma}\left(t, z, x \cdot y\right), \sqrt{\color{blue}{\sqrt{2} \cdot \sqrt{2}}} \cdot \left(\sqrt{2} \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)\right)\]
Applied sqrt-prod1.9
\[\leadsto \mathsf{fma}\left(2, \mathsf{fma}\left(t, z, x \cdot y\right), \color{blue}{\left(\sqrt{\sqrt{2}} \cdot \sqrt{\sqrt{2}}\right)} \cdot \left(\sqrt{2} \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)\right)\]
Applied associate-*l*1.9
\[\leadsto \mathsf{fma}\left(2, \mathsf{fma}\left(t, z, x \cdot y\right), \color{blue}{\sqrt{\sqrt{2}} \cdot \left(\sqrt{\sqrt{2}} \cdot \left(\sqrt{2} \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)\right)}\right)\]
- Using strategy
rm Applied *-un-lft-identity1.9
\[\leadsto \mathsf{fma}\left(2, \mathsf{fma}\left(t, z, x \cdot y\right), \color{blue}{\left(1 \cdot \sqrt{\sqrt{2}}\right)} \cdot \left(\sqrt{\sqrt{2}} \cdot \left(\sqrt{2} \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)\right)\right)\]
Applied associate-*l*1.9
\[\leadsto \mathsf{fma}\left(2, \mathsf{fma}\left(t, z, x \cdot y\right), \color{blue}{1 \cdot \left(\sqrt{\sqrt{2}} \cdot \left(\sqrt{\sqrt{2}} \cdot \left(\sqrt{2} \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)\right)\right)}\right)\]
Simplified1.9
\[\leadsto \mathsf{fma}\left(2, \mathsf{fma}\left(t, z, x \cdot y\right), 1 \cdot \color{blue}{\left(2 \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)}\right)\]
Final simplification1.9
\[\leadsto \mathsf{fma}\left(2, \mathsf{fma}\left(t, z, x \cdot y\right), 1 \cdot \left(2 \cdot \left(\left(-\mathsf{fma}\left(c, b, a\right)\right) \cdot \left(c \cdot i\right)\right)\right)\right)\]