Simplified0.0
\[\leadsto \color{blue}{\left(\mathsf{fma}\left(\mathsf{fma}\left(4, 1 + a \cdot -3, 2 \cdot \left(a \cdot a\right)\right), b \cdot b, {b}^{4}\right) + \left({a}^{4} + \left(4 \cdot \left(a \cdot a\right)\right) \cdot \left(1 + a\right)\right)\right)} - 1
\]
Proof
(-.f64 (+.f64 (fma.f64 (fma.f64 4 (+.f64 1 (*.f64 a -3)) (*.f64 2 (*.f64 a a))) (*.f64 b b) (pow.f64 b 4)) (+.f64 (pow.f64 a 4) (*.f64 (*.f64 4 (*.f64 a a)) (+.f64 1 a)))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (fma.f64 (fma.f64 4 (+.f64 1 (*.f64 a -3)) (*.f64 2 (Rewrite<= unpow2_binary64 (pow.f64 a 2)))) (*.f64 b b) (pow.f64 b 4)) (+.f64 (pow.f64 a 4) (*.f64 (*.f64 4 (*.f64 a a)) (+.f64 1 a)))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (fma.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 4 (+.f64 1 (*.f64 a -3))) (*.f64 2 (pow.f64 a 2)))) (*.f64 b b) (pow.f64 b 4)) (+.f64 (pow.f64 a 4) (*.f64 (*.f64 4 (*.f64 a a)) (+.f64 1 a)))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (fma.f64 (+.f64 (*.f64 4 (+.f64 1 (Rewrite=> *-commutative_binary64 (*.f64 -3 a)))) (*.f64 2 (pow.f64 a 2))) (*.f64 b b) (pow.f64 b 4)) (+.f64 (pow.f64 a 4) (*.f64 (*.f64 4 (*.f64 a a)) (+.f64 1 a)))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (fma.f64 (+.f64 (*.f64 4 (+.f64 1 (*.f64 (Rewrite<= metadata-eval (neg.f64 3)) a))) (*.f64 2 (pow.f64 a 2))) (*.f64 b b) (pow.f64 b 4)) (+.f64 (pow.f64 a 4) (*.f64 (*.f64 4 (*.f64 a a)) (+.f64 1 a)))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (fma.f64 (+.f64 (*.f64 4 (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 1 (*.f64 3 a)))) (*.f64 2 (pow.f64 a 2))) (*.f64 b b) (pow.f64 b 4)) (+.f64 (pow.f64 a 4) (*.f64 (*.f64 4 (*.f64 a a)) (+.f64 1 a)))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 (+.f64 (*.f64 4 (-.f64 1 (*.f64 3 a))) (*.f64 2 (pow.f64 a 2))) (*.f64 b b)) (pow.f64 b 4))) (+.f64 (pow.f64 a 4) (*.f64 (*.f64 4 (*.f64 a a)) (+.f64 1 a)))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (+.f64 (*.f64 (+.f64 (*.f64 4 (-.f64 1 (*.f64 3 a))) (*.f64 2 (pow.f64 a 2))) (Rewrite<= unpow2_binary64 (pow.f64 b 2))) (pow.f64 b 4)) (+.f64 (pow.f64 a 4) (*.f64 (*.f64 4 (*.f64 a a)) (+.f64 1 a)))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (+.f64 (*.f64 (+.f64 (*.f64 4 (-.f64 1 (*.f64 3 a))) (*.f64 2 (pow.f64 a 2))) (pow.f64 b 2)) (pow.f64 b 4)) (+.f64 (pow.f64 a 4) (*.f64 (*.f64 4 (Rewrite<= unpow2_binary64 (pow.f64 a 2))) (+.f64 1 a)))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (+.f64 (+.f64 (*.f64 (+.f64 (*.f64 4 (-.f64 1 (*.f64 3 a))) (*.f64 2 (pow.f64 a 2))) (pow.f64 b 2)) (pow.f64 b 4)) (+.f64 (pow.f64 a 4) (Rewrite<= associate-*r*_binary64 (*.f64 4 (*.f64 (pow.f64 a 2) (+.f64 1 a)))))) 1): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 (+.f64 (*.f64 4 (-.f64 1 (*.f64 3 a))) (*.f64 2 (pow.f64 a 2))) (pow.f64 b 2)) (+.f64 (pow.f64 b 4) (+.f64 (pow.f64 a 4) (*.f64 4 (*.f64 (pow.f64 a 2) (+.f64 1 a))))))) 1): 0 points increase in error, 0 points decrease in error