Simplified0.2
\[\leadsto \color{blue}{\varepsilon \cdot \left(5 \cdot {x}^{4} + \varepsilon \cdot \left({x}^{3} \cdot 10\right)\right)}
\]
Proof
(*.f64 eps (+.f64 (*.f64 5 (pow.f64 x 4)) (*.f64 eps (*.f64 (pow.f64 x 3) 10)))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (*.f64 (Rewrite<= metadata-eval (+.f64 4 1)) (pow.f64 x 4)) (*.f64 eps (*.f64 (pow.f64 x 3) 10)))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4))) (*.f64 eps (*.f64 (pow.f64 x 3) 10)))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (*.f64 eps (*.f64 (pow.f64 x 3) (Rewrite<= metadata-eval (+.f64 4 6)))))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (*.f64 eps (*.f64 (pow.f64 x 3) (+.f64 4 (Rewrite<= metadata-eval (+.f64 2 4))))))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (*.f64 eps (Rewrite<= distribute-lft-out_binary64 (+.f64 (*.f64 (pow.f64 x 3) 4) (*.f64 (pow.f64 x 3) (+.f64 2 4))))))): 1 points increase in error, 1 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (*.f64 eps (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 (pow.f64 x 3))) (*.f64 (pow.f64 x 3) (+.f64 2 4)))))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (*.f64 eps (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (Rewrite=> cube-mult_binary64 (*.f64 x (*.f64 x x))) (+.f64 2 4)))))): 1 points increase in error, 2 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (*.f64 eps (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (*.f64 x (Rewrite<= unpow2_binary64 (pow.f64 x 2))) (+.f64 2 4)))))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (*.f64 eps (+.f64 (*.f64 4 (pow.f64 x 3)) (Rewrite<= associate-*r*_binary64 (*.f64 x (*.f64 (pow.f64 x 2) (+.f64 2 4)))))))): 1 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (*.f64 eps (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 x (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))))))))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (*.f64 eps (+.f64 (*.f64 4 (pow.f64 x 3)) (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)))))): 0 points increase in error, 0 points decrease in error
(*.f64 eps (+.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) (Rewrite=> *-commutative_binary64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) eps)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)) eps) (*.f64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) eps) eps))): 2 points increase in error, 1 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 eps (+.f64 (*.f64 4 (pow.f64 x 4)) (pow.f64 x 4)))) (*.f64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) eps) eps)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 eps (*.f64 4 (pow.f64 x 4))) (*.f64 eps (pow.f64 x 4)))) (*.f64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) eps) eps)): 4 points increase in error, 1 points decrease in error
(+.f64 (+.f64 (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 eps 4) (pow.f64 x 4))) (*.f64 eps (pow.f64 x 4))) (*.f64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) eps) eps)): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 4 eps)) (pow.f64 x 4)) (*.f64 eps (pow.f64 x 4))) (*.f64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) eps) eps)): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 (pow.f64 x 4) (+.f64 (*.f64 4 eps) eps))) (*.f64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) eps) eps)): 1 points increase in error, 6 points decrease in error
(+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4))) (*.f64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) eps) eps)): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (Rewrite<= associate-*r*_binary64 (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) (*.f64 eps eps)))): 2 points increase in error, 4 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (+.f64 (*.f64 4 (pow.f64 x 3)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) (Rewrite<= unpow2_binary64 (pow.f64 eps 2)))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (+.f64 (Rewrite=> *-commutative_binary64 (*.f64 (pow.f64 x 3) 4)) (*.f64 (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2))) x)) (pow.f64 eps 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (+.f64 (*.f64 (pow.f64 x 3) 4) (Rewrite=> *-commutative_binary64 (*.f64 x (+.f64 (*.f64 2 (pow.f64 x 2)) (*.f64 4 (pow.f64 x 2)))))) (pow.f64 eps 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (+.f64 (*.f64 (pow.f64 x 3) 4) (*.f64 x (Rewrite=> distribute-rgt-out_binary64 (*.f64 (pow.f64 x 2) (+.f64 2 4))))) (pow.f64 eps 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (+.f64 (*.f64 (pow.f64 x 3) 4) (Rewrite=> associate-*r*_binary64 (*.f64 (*.f64 x (pow.f64 x 2)) (+.f64 2 4)))) (pow.f64 eps 2))): 0 points increase in error, 2 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (+.f64 (*.f64 (pow.f64 x 3) 4) (*.f64 (*.f64 x (Rewrite=> unpow2_binary64 (*.f64 x x))) (+.f64 2 4))) (pow.f64 eps 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (+.f64 (*.f64 (pow.f64 x 3) 4) (*.f64 (Rewrite<= cube-mult_binary64 (pow.f64 x 3)) (+.f64 2 4))) (pow.f64 eps 2))): 3 points increase in error, 1 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (Rewrite=> distribute-lft-out_binary64 (*.f64 (pow.f64 x 3) (+.f64 4 (+.f64 2 4)))) (pow.f64 eps 2))): 1 points increase in error, 1 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (*.f64 (pow.f64 x 3) (+.f64 4 (Rewrite=> metadata-eval 6))) (pow.f64 eps 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (*.f64 (pow.f64 x 3) (Rewrite=> metadata-eval 10)) (pow.f64 eps 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (*.f64 (pow.f64 x 3) (Rewrite<= metadata-eval (+.f64 2 8))) (pow.f64 eps 2))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (Rewrite<= associate-*r*_binary64 (*.f64 (pow.f64 x 3) (*.f64 (+.f64 2 8) (pow.f64 eps 2))))): 4 points increase in error, 2 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (pow.f64 x 3) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 eps 2) (+.f64 2 8))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (*.f64 (pow.f64 x 3) (Rewrite<= distribute-rgt-out_binary64 (+.f64 (*.f64 2 (pow.f64 eps 2)) (*.f64 8 (pow.f64 eps 2)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (*.f64 (+.f64 (*.f64 4 eps) eps) (pow.f64 x 4)) (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 (*.f64 2 (pow.f64 eps 2)) (*.f64 8 (pow.f64 eps 2))) (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error