Initial program 52.8
\[1 - \log \left(1 - \frac{x - y}{1 - y}\right)
\]
Simplified52.8
\[\leadsto \color{blue}{1 - \mathsf{log1p}\left(\frac{y - x}{1 - y}\right)}
\]
Proof
(-.f64 1 (log1p.f64 (/.f64 (-.f64 y x) (-.f64 1 y)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 y (-.f64 1 y)) (/.f64 x (-.f64 1 y)))))): 0 points increase in error, 1 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 y (-.f64 1 y)) (neg.f64 (/.f64 x (-.f64 1 y))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 x (-.f64 1 y))) (/.f64 y (-.f64 1 y)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (/.f64 x (-.f64 1 y)))) (/.f64 y (-.f64 1 y))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (/.f64 x (-.f64 1 y)) (/.f64 y (-.f64 1 y))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (-.f64 0 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 x y) (-.f64 1 y)))))): 1 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= neg-sub0_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))))))): 5 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
Taylor expanded in y around -inf 0.4
\[\leadsto \color{blue}{1 - \left(\log \left(-1 \cdot \left(x - 1\right)\right) + \log \left(\frac{-1}{y}\right)\right)}
\]
Simplified0.4
\[\leadsto \color{blue}{\left(1 - \mathsf{log1p}\left(-x\right)\right) - \log \left(\frac{-1}{y}\right)}
\]
Proof
(-.f64 (-.f64 1 (log1p.f64 (neg.f64 x))) (log.f64 (/.f64 -1 y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 1 (log1p.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 x)))) (log.f64 (/.f64 -1 y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 1 (Rewrite<= log1p-def_binary64 (log.f64 (+.f64 1 (*.f64 -1 x))))) (log.f64 (/.f64 -1 y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 1 (log.f64 (Rewrite=> +-commutative_binary64 (+.f64 (*.f64 -1 x) 1)))) (log.f64 (/.f64 -1 y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 1 (log.f64 (+.f64 (*.f64 -1 x) (Rewrite<= metadata-eval (*.f64 -1 -1))))) (log.f64 (/.f64 -1 y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 1 (log.f64 (Rewrite<= distribute-lft-in_binary64 (*.f64 -1 (+.f64 x -1))))) (log.f64 (/.f64 -1 y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 1 (log.f64 (*.f64 -1 (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))))) (log.f64 (/.f64 -1 y))): 0 points increase in error, 0 points decrease in error
(-.f64 (-.f64 1 (log.f64 (*.f64 -1 (Rewrite<= sub-neg_binary64 (-.f64 x 1))))) (log.f64 (/.f64 -1 y))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--r+_binary64 (-.f64 1 (+.f64 (log.f64 (*.f64 -1 (-.f64 x 1))) (log.f64 (/.f64 -1 y))))): 0 points increase in error, 0 points decrease in error
Taylor expanded in y around 0 64.0
\[\leadsto \color{blue}{1 - \left(\log -1 + \left(\log \left(1 - x\right) + -1 \cdot \log y\right)\right)}
\]
Simplified0.4
\[\leadsto \color{blue}{\left(1 - \mathsf{log1p}\left(-x\right)\right) + \log \left(-y\right)}
\]
Proof
(+.f64 (-.f64 1 (log1p.f64 (neg.f64 x))) (log.f64 (neg.f64 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 1 (Rewrite<= log1p-def_binary64 (log.f64 (+.f64 1 (neg.f64 x))))) (log.f64 (neg.f64 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 1 (log.f64 (Rewrite<= sub-neg_binary64 (-.f64 1 x)))) (log.f64 (neg.f64 y))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 1 (log.f64 (-.f64 1 x))) (Rewrite<= remove-double-neg_binary64 (neg.f64 (neg.f64 (log.f64 (neg.f64 y)))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 1 (log.f64 (-.f64 1 x))) (neg.f64 (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 (neg.f64 y)))))): 1 points increase in error, 0 points decrease in error
(+.f64 (-.f64 1 (log.f64 (-.f64 1 x))) (neg.f64 (log.f64 (/.f64 (Rewrite<= metadata-eval (/.f64 -1 -1)) (neg.f64 y))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 1 (log.f64 (-.f64 1 x))) (neg.f64 (log.f64 (Rewrite<= associate-/r*_binary64 (/.f64 -1 (*.f64 -1 (neg.f64 y))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 1 (log.f64 (-.f64 1 x))) (neg.f64 (log.f64 (/.f64 -1 (Rewrite<= neg-mul-1_binary64 (neg.f64 (neg.f64 y))))))): 0 points increase in error, 0 points decrease in error
(+.f64 (-.f64 1 (log.f64 (-.f64 1 x))) (neg.f64 (log.f64 (/.f64 -1 (Rewrite=> remove-double-neg_binary64 y))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= sub-neg_binary64 (-.f64 (-.f64 1 (log.f64 (-.f64 1 x))) (log.f64 (/.f64 -1 y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate--r+_binary64 (-.f64 1 (+.f64 (log.f64 (-.f64 1 x)) (log.f64 (/.f64 -1 y))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite<= +-commutative_binary64 (+.f64 (log.f64 (/.f64 -1 y)) (log.f64 (-.f64 1 x))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (+.f64 (Rewrite=> log-div_binary64 (-.f64 (log.f64 -1) (log.f64 y))) (log.f64 (-.f64 1 x)))): 158 points increase in error, 0 points decrease in error
(-.f64 1 (+.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (log.f64 -1) (neg.f64 (log.f64 y)))) (log.f64 (-.f64 1 x)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (Rewrite<= associate-+r+_binary64 (+.f64 (log.f64 -1) (+.f64 (neg.f64 (log.f64 y)) (log.f64 (-.f64 1 x)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (+.f64 (log.f64 -1) (Rewrite=> +-commutative_binary64 (+.f64 (log.f64 (-.f64 1 x)) (neg.f64 (log.f64 y)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (+.f64 (log.f64 -1) (+.f64 (log.f64 (-.f64 1 x)) (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (log.f64 y)))))): 0 points increase in error, 0 points decrease in error
Initial program 0.1
\[1 - \log \left(1 - \frac{x - y}{1 - y}\right)
\]
Simplified0.1
\[\leadsto \color{blue}{1 - \mathsf{log1p}\left(\frac{y - x}{1 - y}\right)}
\]
Proof
(-.f64 1 (log1p.f64 (/.f64 (-.f64 y x) (-.f64 1 y)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 y (-.f64 1 y)) (/.f64 x (-.f64 1 y)))))): 0 points increase in error, 1 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 y (-.f64 1 y)) (neg.f64 (/.f64 x (-.f64 1 y))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 x (-.f64 1 y))) (/.f64 y (-.f64 1 y)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (/.f64 x (-.f64 1 y)))) (/.f64 y (-.f64 1 y))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (/.f64 x (-.f64 1 y)) (/.f64 y (-.f64 1 y))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (-.f64 0 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 x y) (-.f64 1 y)))))): 1 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= neg-sub0_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))))))): 5 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
Initial program 32.5
\[1 - \log \left(1 - \frac{x - y}{1 - y}\right)
\]
Simplified32.5
\[\leadsto \color{blue}{1 - \mathsf{log1p}\left(\frac{y - x}{1 - y}\right)}
\]
Proof
(-.f64 1 (log1p.f64 (/.f64 (-.f64 y x) (-.f64 1 y)))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite=> div-sub_binary64 (-.f64 (/.f64 y (-.f64 1 y)) (/.f64 x (-.f64 1 y)))))): 0 points increase in error, 1 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= unsub-neg_binary64 (+.f64 (/.f64 y (-.f64 1 y)) (neg.f64 (/.f64 x (-.f64 1 y))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= +-commutative_binary64 (+.f64 (neg.f64 (/.f64 x (-.f64 1 y))) (/.f64 y (-.f64 1 y)))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (+.f64 (Rewrite=> neg-sub0_binary64 (-.f64 0 (/.f64 x (-.f64 1 y)))) (/.f64 y (-.f64 1 y))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 (/.f64 x (-.f64 1 y)) (/.f64 y (-.f64 1 y))))))): 0 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (-.f64 0 (Rewrite<= div-sub_binary64 (/.f64 (-.f64 x y) (-.f64 1 y)))))): 1 points increase in error, 0 points decrease in error
(-.f64 1 (log1p.f64 (Rewrite<= neg-sub0_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))))))): 5 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
Taylor expanded in y around inf 0.9
\[\leadsto 1 - \color{blue}{\left(\log \left(\frac{1}{y}\right) + \log \left(x - 1\right)\right)}
\]
Simplified0.9
\[\leadsto 1 - \color{blue}{\left(\log \left(-1 + x\right) - \log y\right)}
\]
Proof
(-.f64 (log.f64 (+.f64 -1 x)) (log.f64 y)): 0 points increase in error, 0 points decrease in error
(-.f64 (log.f64 (Rewrite<= +-commutative_binary64 (+.f64 x -1))) (log.f64 y)): 0 points increase in error, 0 points decrease in error
(-.f64 (log.f64 (+.f64 x (Rewrite<= metadata-eval (neg.f64 1)))) (log.f64 y)): 0 points increase in error, 0 points decrease in error
(-.f64 (log.f64 (Rewrite<= sub-neg_binary64 (-.f64 x 1))) (log.f64 y)): 0 points increase in error, 0 points decrease in error
(Rewrite<= unsub-neg_binary64 (+.f64 (log.f64 (-.f64 x 1)) (neg.f64 (log.f64 y)))): 0 points increase in error, 0 points decrease in error
(+.f64 (log.f64 (-.f64 x 1)) (Rewrite<= log-rec_binary64 (log.f64 (/.f64 1 y)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-commutative_binary64 (+.f64 (log.f64 (/.f64 1 y)) (log.f64 (-.f64 x 1)))): 0 points increase in error, 0 points decrease in error