Simplified10.8
\[\leadsto \left(\left(\left(x - 0.5\right) \cdot \log x - x\right) + 0.91893853320467\right) + \color{blue}{\left(\mathsf{fma}\left(-0.0027777777777778, \frac{z}{x}, \frac{0.083333333333333}{x}\right) + \frac{z \cdot z}{x} \cdot \left(0.0007936500793651 + y\right)\right)}
\]
Proof
(+.f64 (fma.f64 -13888888888889/5000000000000000 (/.f64 z x) (/.f64 83333333333333/1000000000000000 x)) (*.f64 (/.f64 (*.f64 z z) x) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 -13888888888889/5000000000000000 (/.f64 z x) (/.f64 (Rewrite<= metadata-eval (*.f64 83333333333333/1000000000000000 1)) x)) (*.f64 (/.f64 (*.f64 z z) x) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (fma.f64 -13888888888889/5000000000000000 (/.f64 z x) (Rewrite<= associate-*r/_binary64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)))) (*.f64 (/.f64 (*.f64 z z) x) (+.f64 7936500793651/10000000000000000 y))): 22 points increase in error, 27 points decrease in error
(+.f64 (Rewrite<= fma-def_binary64 (+.f64 (*.f64 -13888888888889/5000000000000000 (/.f64 z x)) (*.f64 83333333333333/1000000000000000 (/.f64 1 x)))) (*.f64 (/.f64 (*.f64 z z) x) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x)))) (*.f64 (/.f64 (*.f64 z z) x) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (/.f64 (*.f64 z z) (Rewrite<= *-rgt-identity_binary64 (*.f64 x 1))) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 z x) (/.f64 z 1))) (+.f64 7936500793651/10000000000000000 y))): 6 points increase in error, 22 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (*.f64 (/.f64 (Rewrite<= remove-double-div_binary64 (/.f64 1 (/.f64 1 z))) x) (/.f64 z 1)) (+.f64 7936500793651/10000000000000000 y))): 5 points increase in error, 3 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (*.f64 (/.f64 (Rewrite<= unpow-1_binary64 (pow.f64 (/.f64 1 z) -1)) x) (/.f64 z 1)) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (*.f64 (/.f64 (pow.f64 (/.f64 1 z) (Rewrite<= metadata-eval (/.f64 -2 2))) x) (/.f64 z 1)) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (*.f64 (/.f64 (pow.f64 (/.f64 1 z) (/.f64 -2 2)) x) (/.f64 (Rewrite<= remove-double-div_binary64 (/.f64 1 (/.f64 1 z))) 1)) (+.f64 7936500793651/10000000000000000 y))): 12 points increase in error, 3 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (*.f64 (/.f64 (pow.f64 (/.f64 1 z) (/.f64 -2 2)) x) (/.f64 (Rewrite<= unpow-1_binary64 (pow.f64 (/.f64 1 z) -1)) 1)) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (*.f64 (/.f64 (pow.f64 (/.f64 1 z) (/.f64 -2 2)) x) (/.f64 (pow.f64 (/.f64 1 z) (Rewrite<= metadata-eval (/.f64 -2 2))) 1)) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (pow.f64 (/.f64 1 z) (/.f64 -2 2)) (pow.f64 (/.f64 1 z) (/.f64 -2 2))) (*.f64 x 1))) (+.f64 7936500793651/10000000000000000 y))): 24 points increase in error, 8 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (/.f64 (Rewrite<= sqr-pow_binary64 (pow.f64 (/.f64 1 z) -2)) (*.f64 x 1)) (+.f64 7936500793651/10000000000000000 y))): 4 points increase in error, 11 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (*.f64 (/.f64 (pow.f64 (/.f64 1 z) -2) (Rewrite=> *-rgt-identity_binary64 x)) (+.f64 7936500793651/10000000000000000 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (Rewrite<= associate-/r/_binary64 (/.f64 (pow.f64 (/.f64 1 z) -2) (/.f64 x (+.f64 7936500793651/10000000000000000 y))))): 37 points increase in error, 18 points decrease in error
(+.f64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (*.f64 -13888888888889/5000000000000000 (/.f64 z x))) (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (pow.f64 (/.f64 1 z) -2) (+.f64 7936500793651/10000000000000000 y)) x))): 25 points increase in error, 36 points decrease in error
(Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 83333333333333/1000000000000000 (/.f64 1 x)) (+.f64 (*.f64 -13888888888889/5000000000000000 (/.f64 z x)) (/.f64 (*.f64 (pow.f64 (/.f64 1 z) -2) (+.f64 7936500793651/10000000000000000 y)) x)))): 1 points increase in error, 1 points decrease in error
Simplified0.8
\[\leadsto \left(\left(\color{blue}{x \cdot \log x} - x\right) + 0.91893853320467\right) + \left(\mathsf{fma}\left(-0.0027777777777778, \frac{z}{x}, \frac{0.083333333333333}{x}\right) + \left(z \cdot \left(z \cdot \frac{1}{x}\right)\right) \cdot \left(0.0007936500793651 + y\right)\right)
\]
Proof
(*.f64 x (log.f64 x)): 0 points increase in error, 0 points decrease in error
(Rewrite<= *-commutative_binary64 (*.f64 (log.f64 x) x)): 0 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (log.f64 x)))) x): 0 points increase in error, 0 points decrease in error
(*.f64 (neg.f64 (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 x)))) x): 0 points increase in error, 1 points decrease in error
(Rewrite=> distribute-lft-neg-out_binary64 (neg.f64 (*.f64 (log.f64 (/.f64 1 x)) x))): 0 points increase in error, 0 points decrease in error
(Rewrite<= mul-1-neg_binary64 (*.f64 -1 (*.f64 (log.f64 (/.f64 1 x)) x))): 0 points increase in error, 0 points decrease in error