Simplified0.0
\[\leadsto \color{blue}{\frac{1 - {x}^{-2}}{x}}
\]
Proof
(/.f64 (-.f64 1 (pow.f64 x -2)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite<= *-inverses_binary64 (/.f64 (pow.f64 x 3) (pow.f64 x 3))) (pow.f64 x -2)) x): 86 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (pow.f64 x 3) (Rewrite=> cube-mult_binary64 (*.f64 x (*.f64 x x)))) (pow.f64 x -2)) x): 7 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (pow.f64 x 3) x) (*.f64 x x))) (pow.f64 x -2)) x): 6 points increase in error, 5 points decrease in error
(/.f64 (-.f64 (/.f64 (/.f64 (pow.f64 x 3) x) (*.f64 x x)) (pow.f64 x (Rewrite<= metadata-eval (*.f64 2 -1)))) x): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (/.f64 (pow.f64 x 3) x) (*.f64 x x)) (Rewrite<= pow-sqr_binary64 (*.f64 (pow.f64 x -1) (pow.f64 x -1)))) x): 7 points increase in error, 9 points decrease in error
(/.f64 (-.f64 (/.f64 (/.f64 (pow.f64 x 3) x) (*.f64 x x)) (*.f64 (Rewrite=> unpow-1_binary64 (/.f64 1 x)) (pow.f64 x -1))) x): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (/.f64 (pow.f64 x 3) x) (*.f64 x x)) (*.f64 (/.f64 1 x) (Rewrite=> unpow-1_binary64 (/.f64 1 x)))) x): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (/.f64 (pow.f64 x 3) x) (*.f64 x x)) (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 (/.f64 1 x)) x))) x): 6 points increase in error, 1 points decrease in error
(/.f64 (-.f64 (/.f64 (/.f64 (pow.f64 x 3) x) (*.f64 x x)) (/.f64 (Rewrite=> *-lft-identity_binary64 (/.f64 1 x)) x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (-.f64 (/.f64 (/.f64 (pow.f64 x 3) x) (*.f64 x x)) (Rewrite=> associate-/l/_binary64 (/.f64 1 (*.f64 x x)))) x): 3 points increase in error, 10 points decrease in error
(/.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (/.f64 (pow.f64 x 3) x) 1) (*.f64 x x))) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (-.f64 (/.f64 (pow.f64 x 3) x) (Rewrite<= *-inverses_binary64 (/.f64 x x))) (*.f64 x x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 (pow.f64 x 3) x) x)) (*.f64 x x)) x): 0 points increase in error, 1 points decrease in error
(/.f64 (Rewrite=> associate-/l/_binary64 (/.f64 (-.f64 (pow.f64 x 3) x) (*.f64 (*.f64 x x) x))) x): 14 points increase in error, 11 points decrease in error
(/.f64 (/.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 (-.f64 (pow.f64 x 3) x) 1)) (*.f64 (*.f64 x x) x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (-.f64 (pow.f64 x 3) x) (Rewrite<= metadata-eval (/.f64 -1 -1))) (*.f64 (*.f64 x x) x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (-.f64 (pow.f64 x 3) x) -1) -1)) (*.f64 (*.f64 x x) x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (-.f64 (pow.f64 x 3) x))) -1) (*.f64 (*.f64 x x) x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (Rewrite<= distribute-rgt-out--_binary64 (-.f64 (*.f64 (pow.f64 x 3) -1) (*.f64 x -1))) -1) (*.f64 (*.f64 x x) x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (-.f64 (Rewrite<= *-commutative_binary64 (*.f64 -1 (pow.f64 x 3))) (*.f64 x -1)) -1) (*.f64 (*.f64 x x) x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (-.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (pow.f64 x 3))) (*.f64 x -1)) -1) (*.f64 (*.f64 x x) x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (/.f64 (-.f64 (neg.f64 (pow.f64 x 3)) (*.f64 x -1)) -1) x) (*.f64 x x))) x): 11 points increase in error, 14 points decrease in error
(/.f64 (/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (-.f64 (neg.f64 (pow.f64 x 3)) (*.f64 x -1)) (*.f64 -1 x))) (*.f64 x x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (-.f64 (neg.f64 (pow.f64 x 3)) (Rewrite=> *-commutative_binary64 (*.f64 -1 x))) (*.f64 -1 x)) (*.f64 x x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (-.f64 (neg.f64 (pow.f64 x 3)) (Rewrite<= neg-mul-1_binary64 (neg.f64 x))) (*.f64 -1 x)) (*.f64 x x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (-.f64 (neg.f64 (pow.f64 x 3)) (Rewrite<= *-rgt-identity_binary64 (*.f64 (neg.f64 x) 1))) (*.f64 -1 x)) (*.f64 x x)) x): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (-.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) 1)) (Rewrite<= neg-mul-1_binary64 (neg.f64 x))) (*.f64 x x)) x): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (/.f64 (-.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) 1)) (neg.f64 x)) (*.f64 (*.f64 x x) x))): 22 points increase in error, 12 points decrease in error
(/.f64 (/.f64 (-.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) 1)) (neg.f64 x)) (Rewrite<= unpow3_binary64 (pow.f64 x 3))): 6 points increase in error, 11 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (-.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) 1)) (*.f64 (neg.f64 x) (pow.f64 x 3)))): 27 points increase in error, 14 points decrease in error
(Rewrite=> div-sub_binary64 (-.f64 (/.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) (pow.f64 x 3))) (/.f64 (*.f64 (neg.f64 x) 1) (*.f64 (neg.f64 x) (pow.f64 x 3))))): 1 points increase in error, 2 points decrease in error
(-.f64 (/.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) (pow.f64 x 3))) (/.f64 (Rewrite=> *-rgt-identity_binary64 (neg.f64 x)) (*.f64 (neg.f64 x) (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) (pow.f64 x 3))) (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 x)) (*.f64 (neg.f64 x) (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) (pow.f64 x 3))) (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 x -1)) (*.f64 (neg.f64 x) (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) (pow.f64 x 3))) (/.f64 (*.f64 x -1) (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 x (pow.f64 x 3)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (neg.f64 (pow.f64 x 3)) (*.f64 (neg.f64 x) (pow.f64 x 3))) (/.f64 (*.f64 x -1) (Rewrite<= distribute-rgt-neg-out_binary64 (*.f64 x (neg.f64 (pow.f64 x 3)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (neg.f64 (pow.f64 x 3)) (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 x (pow.f64 x 3))))) (/.f64 (*.f64 x -1) (*.f64 x (neg.f64 (pow.f64 x 3))))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 (neg.f64 (pow.f64 x 3)) (Rewrite<= distribute-rgt-neg-out_binary64 (*.f64 x (neg.f64 (pow.f64 x 3))))) (/.f64 (*.f64 x -1) (*.f64 x (neg.f64 (pow.f64 x 3))))): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (neg.f64 (pow.f64 x 3)) (neg.f64 (pow.f64 x 3))) x)) (/.f64 (*.f64 x -1) (*.f64 x (neg.f64 (pow.f64 x 3))))): 1 points increase in error, 11 points decrease in error
(-.f64 (/.f64 (Rewrite=> *-inverses_binary64 1) x) (/.f64 (*.f64 x -1) (*.f64 x (neg.f64 (pow.f64 x 3))))): 0 points increase in error, 86 points decrease in error
(-.f64 (/.f64 1 x) (/.f64 (*.f64 x -1) (Rewrite=> distribute-rgt-neg-out_binary64 (neg.f64 (*.f64 x (pow.f64 x 3)))))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (/.f64 (*.f64 x -1) (Rewrite<= distribute-lft-neg-out_binary64 (*.f64 (neg.f64 x) (pow.f64 x 3))))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (/.f64 (Rewrite=> *-commutative_binary64 (*.f64 -1 x)) (*.f64 (neg.f64 x) (pow.f64 x 3)))): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (Rewrite=> associate-/l*_binary64 (/.f64 -1 (/.f64 (*.f64 (neg.f64 x) (pow.f64 x 3)) x)))): 4 points increase in error, 3 points decrease in error
(-.f64 (/.f64 1 x) (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 -1 (*.f64 (neg.f64 x) (pow.f64 x 3))) x))): 8 points increase in error, 6 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (Rewrite<= metadata-eval (/.f64 1 -1)) (*.f64 (neg.f64 x) (pow.f64 x 3))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (Rewrite<= associate-/r*_binary64 (/.f64 1 (*.f64 -1 (*.f64 (neg.f64 x) (pow.f64 x 3))))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 1 (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 (neg.f64 x) (pow.f64 x 3))))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 1 (neg.f64 (Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 x (pow.f64 x 3)))))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 1 (Rewrite=> remove-double-neg_binary64 (*.f64 x (pow.f64 x 3)))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 1 x) (pow.f64 x 3))) x)): 3 points increase in error, 5 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 1 x))) (pow.f64 x 3)) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (Rewrite=> unpow3_binary64 (*.f64 (*.f64 x x) x))) x)): 5 points increase in error, 2 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (*.f64 (*.f64 (Rewrite<= /-rgt-identity_binary64 (/.f64 x 1)) x) x)) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (*.f64 (Rewrite<= associate-/r/_binary64 (/.f64 x (/.f64 1 x))) x)) x)): 0 points increase in error, 1 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (Rewrite<= associate-/r/_binary64 (/.f64 x (/.f64 (/.f64 1 x) x)))) x)): 3 points increase in error, 4 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (/.f64 x (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 1 x))) x))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (/.f64 x (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 x) (/.f64 1 x))))) x)): 1 points increase in error, 4 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (/.f64 x (*.f64 (Rewrite<= unpow-1_binary64 (pow.f64 x -1)) (/.f64 1 x)))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (/.f64 x (*.f64 (pow.f64 x -1) (Rewrite<= unpow-1_binary64 (pow.f64 x -1))))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (/.f64 x (Rewrite=> pow-sqr_binary64 (pow.f64 x (*.f64 2 -1))))) x)): 4 points increase in error, 5 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (/.f64 (*.f64 1 (/.f64 1 x)) (/.f64 x (pow.f64 x (Rewrite=> metadata-eval -2)))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (/.f64 x (pow.f64 x -2))) (/.f64 1 x))) x)): 3 points increase in error, 2 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (*.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 1 x) (pow.f64 x -2))) (/.f64 1 x)) x)): 4 points increase in error, 1 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (*.f64 (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 x -2) (/.f64 1 x))) (/.f64 1 x)) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (Rewrite<= associate-*r*_binary64 (*.f64 (pow.f64 x -2) (*.f64 (/.f64 1 x) (/.f64 1 x)))) x)): 4 points increase in error, 3 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (*.f64 (pow.f64 x -2) (*.f64 (Rewrite<= unpow-1_binary64 (pow.f64 x -1)) (/.f64 1 x))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (*.f64 (pow.f64 x -2) (*.f64 (pow.f64 x -1) (Rewrite<= unpow-1_binary64 (pow.f64 x -1)))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (*.f64 (pow.f64 x -2) (Rewrite=> pow-sqr_binary64 (pow.f64 x (*.f64 2 -1)))) x)): 5 points increase in error, 6 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (*.f64 (pow.f64 x -2) (pow.f64 x (Rewrite=> metadata-eval -2))) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (Rewrite=> pow-sqr_binary64 (pow.f64 x (*.f64 2 -2))) x)): 7 points increase in error, 4 points decrease in error
(-.f64 (/.f64 1 x) (*.f64 (pow.f64 x (Rewrite=> metadata-eval -4)) x)): 0 points increase in error, 0 points decrease in error
(-.f64 (/.f64 1 x) (Rewrite=> pow-plus_binary64 (pow.f64 x (+.f64 -4 1)))): 7 points increase in error, 16 points decrease in error
(-.f64 (/.f64 1 x) (pow.f64 x (Rewrite=> metadata-eval -3))): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 1 x) (neg.f64 (pow.f64 x -3)))): 0 points increase in error, 0 points decrease in error