Simplified0.0
\[\leadsto \color{blue}{\frac{-1}{{x}^{4}} + \left(\left(\frac{-3}{x} - \frac{\frac{1}{x}}{x}\right) + \frac{-3}{{x}^{3}}\right)}
\]
Proof
(+.f64 (/.f64 -1 (pow.f64 x 4)) (+.f64 (-.f64 (/.f64 -3 x) (/.f64 (/.f64 1 x) x)) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) (pow.f64 x 4)) (+.f64 (-.f64 (/.f64 -3 x) (/.f64 (/.f64 1 x) x)) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 1 (pow.f64 x 4)))) (+.f64 (-.f64 (/.f64 -3 x) (/.f64 (/.f64 1 x) x)) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (-.f64 (/.f64 (Rewrite<= metadata-eval (neg.f64 3)) x) (/.f64 (/.f64 1 x) x)) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (-.f64 (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 3 x))) (/.f64 (/.f64 1 x) x)) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (-.f64 (neg.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 3 1)) x)) (/.f64 (/.f64 1 x) x)) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (-.f64 (neg.f64 (Rewrite<= associate-*r/_binary64 (*.f64 3 (/.f64 1 x)))) (/.f64 (/.f64 1 x) x)) (/.f64 -3 (pow.f64 x 3)))): 43 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (-.f64 (neg.f64 (*.f64 3 (/.f64 1 x))) (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 x x)))) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (-.f64 (neg.f64 (*.f64 3 (/.f64 1 x))) (/.f64 1 (Rewrite<= unpow2_binary64 (pow.f64 x 2)))) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (neg.f64 (*.f64 3 (/.f64 1 x))) (neg.f64 (/.f64 1 (pow.f64 x 2))))) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 1 (pow.f64 x 2))) (neg.f64 (*.f64 3 (/.f64 1 x))))) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (/.f64 1 (pow.f64 x 2)) (*.f64 3 (/.f64 1 x))))) (/.f64 -3 (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (neg.f64 (+.f64 (/.f64 1 (pow.f64 x 2)) (*.f64 3 (/.f64 1 x)))) (/.f64 (Rewrite<= metadata-eval (neg.f64 3)) (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (neg.f64 (+.f64 (/.f64 1 (pow.f64 x 2)) (*.f64 3 (/.f64 1 x)))) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 3 (pow.f64 x 3)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (neg.f64 (+.f64 (/.f64 1 (pow.f64 x 2)) (*.f64 3 (/.f64 1 x)))) (neg.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 3 1)) (pow.f64 x 3))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (+.f64 (neg.f64 (+.f64 (/.f64 1 (pow.f64 x 2)) (*.f64 3 (/.f64 1 x)))) (neg.f64 (Rewrite<= associate-*r/_binary64 (*.f64 3 (/.f64 1 (pow.f64 x 3))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (+.f64 (/.f64 1 (pow.f64 x 2)) (*.f64 3 (/.f64 1 x))) (*.f64 3 (/.f64 1 (pow.f64 x 3))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (neg.f64 (Rewrite=> associate-+l+_binary64 (+.f64 (/.f64 1 (pow.f64 x 2)) (+.f64 (*.f64 3 (/.f64 1 x)) (*.f64 3 (/.f64 1 (pow.f64 x 3)))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (neg.f64 (/.f64 1 (pow.f64 x 4))) (neg.f64 (+.f64 (/.f64 1 (pow.f64 x 2)) (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 3 (/.f64 1 (pow.f64 x 3))) (*.f64 3 (/.f64 1 x))))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= distribute-neg-in_binary64 (neg.f64 (+.f64 (/.f64 1 (pow.f64 x 4)) (+.f64 (/.f64 1 (pow.f64 x 2)) (+.f64 (*.f64 3 (/.f64 1 (pow.f64 x 3))) (*.f64 3 (/.f64 1 x))))))): 0 points increase in error, 0 points decrease in error