Initial program 16.1
\[{\left(x + \varepsilon\right)}^{2} - {x}^{2}
\]
Simplified0.0
\[\leadsto \color{blue}{\varepsilon \cdot \mathsf{fma}\left(2, x, \varepsilon\right)}
\]
Proof
(*.f64 eps (fma.f64 2 x eps)): 0 points increase in error, 0 points decrease in error
(*.f64 eps (Rewrite<= fma-def_binary64 (+.f64 (*.f64 2 x) eps))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (Rewrite<= count-2_binary64 (+.f64 x x)) eps)): 0 points increase in error, 0 points decrease in error
(*.f64 eps (Rewrite<= associate-+r+_binary64 (+.f64 x (+.f64 x eps)))): 5 points increase in error, 3 points decrease in error
(Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 x eps) (*.f64 (+.f64 x eps) eps))): 7 points increase in error, 2 points decrease in error
(Rewrite<= +-rgt-identity_binary64 (+.f64 (+.f64 (*.f64 x eps) (*.f64 (+.f64 x eps) eps)) 0)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 x eps) (*.f64 (+.f64 x eps) eps)) (Rewrite<= +-inverses_binary64 (-.f64 (pow.f64 x 2) (pow.f64 x 2)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (+.f64 (*.f64 x eps) (*.f64 (+.f64 x eps) eps)) (pow.f64 x 2)) (pow.f64 x 2))): 79 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 (pow.f64 x 2) (+.f64 (*.f64 x eps) (*.f64 (+.f64 x eps) eps)))) (pow.f64 x 2)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (pow.f64 x 2) (*.f64 x eps)) (*.f64 (+.f64 x eps) eps))) (pow.f64 x 2)): 5 points increase in error, 1 points decrease in error
(-.f64 (+.f64 (+.f64 (Rewrite=> unpow2_binary64 (*.f64 x x)) (*.f64 x eps)) (*.f64 (+.f64 x eps) eps)) (pow.f64 x 2)): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 x (+.f64 x eps))) (*.f64 (+.f64 x eps) eps)) (pow.f64 x 2)): 2 points increase in error, 1 points decrease in error
(-.f64 (+.f64 (*.f64 x (+.f64 x eps)) (Rewrite=> *-commutative_binary64 (*.f64 eps (+.f64 x eps)))) (pow.f64 x 2)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 (+.f64 x eps) (+.f64 x eps))) (pow.f64 x 2)): 1 points increase in error, 2 points decrease in error
(-.f64 (Rewrite<= unpow2_binary64 (pow.f64 (+.f64 x eps) 2)) (pow.f64 x 2)): 0 points increase in error, 0 points decrease in error
Applied egg-rr9.4
\[\leadsto \color{blue}{{\left(\sqrt{\varepsilon \cdot \mathsf{fma}\left(2, x, \varepsilon\right)}\right)}^{2}}
\]
Taylor expanded in eps around inf 0.0
\[\leadsto \color{blue}{{\varepsilon}^{2} + 2 \cdot \left(\varepsilon \cdot x\right)}
\]
Simplified0.0
\[\leadsto \color{blue}{\varepsilon \cdot \left(\varepsilon + x \cdot 2\right)}
\]
Proof
(*.f64 eps (+.f64 eps (*.f64 x 2))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 eps eps) (*.f64 eps (*.f64 x 2)))): 5 points increase in error, 1 points decrease in error
(+.f64 (Rewrite<= unpow2_binary64 (pow.f64 eps 2)) (*.f64 eps (*.f64 x 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (pow.f64 eps 2) (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 eps x) 2))): 3 points increase in error, 0 points decrease in error
(+.f64 (pow.f64 eps 2) (Rewrite<= *-commutative_binary64 (*.f64 2 (*.f64 eps x)))): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \varepsilon \cdot \left(\varepsilon + x \cdot 2\right)
\]