Initial program 0.2
\[\frac{6 \cdot \left(x - 1\right)}{\left(x + 1\right) + 4 \cdot \sqrt{x}}
\]
Simplified0.0
\[\leadsto \color{blue}{\frac{6}{\frac{x + \left(1 + 4 \cdot \sqrt{x}\right)}{x + -1}}}
\]
Proof
(/.f64 6 (/.f64 (+.f64 x (+.f64 1 (*.f64 4 (sqrt.f64 x)))) (+.f64 x -1))): 0 points increase in error, 0 points decrease in error
(/.f64 6 (/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 x 1) (*.f64 4 (sqrt.f64 x)))) (+.f64 x -1))): 0 points increase in error, 0 points decrease in error
(/.f64 6 (/.f64 (+.f64 (+.f64 x 1) (*.f64 4 (sqrt.f64 x))) (+.f64 x (Rewrite<= metadata-eval (neg.f64 1))))): 0 points increase in error, 0 points decrease in error
(/.f64 6 (/.f64 (+.f64 (+.f64 x 1) (*.f64 4 (sqrt.f64 x))) (Rewrite<= sub-neg_binary64 (-.f64 x 1)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 6 (-.f64 x 1)) (+.f64 (+.f64 x 1) (*.f64 4 (sqrt.f64 x))))): 25 points increase in error, 5 points decrease in error
Applied egg-rr0.2
\[\leadsto \frac{6}{\frac{\color{blue}{\mathsf{fma}\left(1 - x \cdot 16, \frac{1}{1 - 4 \cdot \sqrt{x}}, x\right)}}{x + -1}}
\]
Simplified0.2
\[\leadsto \frac{6}{\frac{\color{blue}{x + \frac{1 + x \cdot -16}{1 + \sqrt{x} \cdot -4}}}{x + -1}}
\]
Proof
(+.f64 x (/.f64 (+.f64 1 (*.f64 x -16)) (+.f64 1 (*.f64 (sqrt.f64 x) -4)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 (+.f64 1 (*.f64 x (Rewrite<= metadata-eval (neg.f64 16)))) (+.f64 1 (*.f64 (sqrt.f64 x) -4)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 (+.f64 1 (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 x 16)))) (+.f64 1 (*.f64 (sqrt.f64 x) -4)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 (Rewrite<= sub-neg_binary64 (-.f64 1 (*.f64 x 16))) (+.f64 1 (*.f64 (sqrt.f64 x) -4)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (-.f64 1 (*.f64 x 16)) 1)) (+.f64 1 (*.f64 (sqrt.f64 x) -4)))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 (*.f64 (-.f64 1 (*.f64 x 16)) 1) (+.f64 1 (Rewrite<= *-commutative_binary64 (*.f64 -4 (sqrt.f64 x)))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 (*.f64 (-.f64 1 (*.f64 x 16)) 1) (+.f64 1 (*.f64 (Rewrite<= metadata-eval (neg.f64 4)) (sqrt.f64 x))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (/.f64 (*.f64 (-.f64 1 (*.f64 x 16)) 1) (Rewrite<= cancel-sign-sub-inv_binary64 (-.f64 1 (*.f64 4 (sqrt.f64 x)))))): 0 points increase in error, 0 points decrease in error
(+.f64 x (Rewrite<= associate-*r/_binary64 (*.f64 (-.f64 1 (*.f64 x 16)) (/.f64 1 (-.f64 1 (*.f64 4 (sqrt.f64 x))))))): 2 points increase in error, 1 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (*.f64 (-.f64 1 (*.f64 x 16)) (/.f64 1 (-.f64 1 (*.f64 4 (sqrt.f64 x))))) x)): 0 points increase in error, 0 points decrease in error
(Rewrite<= fma-udef_binary64 (fma.f64 (-.f64 1 (*.f64 x 16)) (/.f64 1 (-.f64 1 (*.f64 4 (sqrt.f64 x)))) x)): 1 points increase in error, 0 points decrease in error
Final simplification0.2
\[\leadsto \frac{6}{\frac{x + \frac{1 + x \cdot -16}{1 + \sqrt{x} \cdot -4}}{x + -1}}
\]