Simplified51.8
\[\leadsto \color{blue}{1 - \mathsf{log1p}\left(\frac{x - y}{y + -1}\right)}
\]
Proof
(-.f64 1 (log1p.f64 (/.f64 (-.f64 x y) (+.f64 y -1)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (/.f64 (-.f64 x y) (Rewrite=> +-commutative_binary64 (+.f64 -1 y))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (/.f64 (-.f64 x y) (+.f64 (Rewrite<= metadata-eval (-.f64 0 1)) y)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (/.f64 (-.f64 x y) (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 1 y)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (/.f64 (-.f64 x y) (Rewrite=> sub0-neg_binary64 (neg.f64 (-.f64 1 y)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (/.f64 (-.f64 x y) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 1 y)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (/.f64 (-.f64 x y) (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 1 y) -1))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 (-.f64 x y) (-.f64 1 y)) -1)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (/.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 (-.f64 x y) (-.f64 1 y)))) -1))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite=> associate-/l*_binary64 (/.f64 1 (/.f64 -1 (/.f64 (-.f64 x y) (-.f64 1 y))))))): 7 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 1 -1) (/.f64 (-.f64 x y) (-.f64 1 y)))))): 0 points increase in error, 7 points decrease in error
(-.f64 1 (log1p.f64 (*.f64 (Rewrite=> metadata-eval -1) (/.f64 (-.f64 x y) (-.f64 1 y))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (/.f64 (-.f64 x y) (-.f64 1 y)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite<= log1p-def_binary64 (log.f64 (+.f64 1 (neg.f64 (/.f64 (-.f64 x y) (-.f64 1 y))))))): 2 points increase in error, 0 points decrease in error
(-.f64 1 (log.f64 (Rewrite<= sub-neg_binary64 (-.f64 1 (/.f64 (-.f64 x y) (-.f64 1 y)))))): 0 points increase in error, 0 points decrease in error