Initial program 29.0
\[\log \left(N + 1\right) - \log N
\]
Simplified29.0
\[\leadsto \color{blue}{\mathsf{log1p}\left(N\right) - \log N}
\]
Proof
(-.f64 (log1p.f64 N) (log.f64 N)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= log1p-def_binary64 (log.f64 (+.f64 1 N))) (log.f64 N)): 3 points increase in error, 0 points decrease in error
(-.f64 (log.f64 (Rewrite<= +-commutative_binary64 (+.f64 N 1))) (log.f64 N)): 0 points increase in error, 3 points decrease in error
Applied egg-rr28.9
\[\leadsto \color{blue}{\log \left(\frac{N + 1}{N}\right)}
\]
Applied egg-rr28.9
\[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{N + 1}{N} - 1\right)}
\]
Simplified0.0
\[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{N} + 0\right)}
\]
Proof
(log1p.f64 (+.f64 (/.f64 1 N) 0)): 0 points increase in error, 0 points decrease in error
(log1p.f64 (+.f64 (/.f64 1 N) (Rewrite<= metadata-eval (-.f64 1 1)))): 5 points increase in error, 3 points decrease in error
(log1p.f64 (Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (/.f64 1 N) 1) 1))): 0 points increase in error, 8 points decrease in error
(log1p.f64 (-.f64 (+.f64 (Rewrite<= *-lft-identity_binary64 (*.f64 1 (/.f64 1 N))) 1) 1)): 0 points increase in error, 8 points decrease in error
(log1p.f64 (-.f64 (+.f64 (*.f64 1 (/.f64 1 N)) (Rewrite<= rgt-mult-inverse_binary64 (*.f64 N (/.f64 1 N)))) 1)): 0 points increase in error, 0 points decrease in error
(log1p.f64 (-.f64 (Rewrite<= distribute-rgt-in_binary64 (*.f64 (/.f64 1 N) (+.f64 1 N))) 1)): 0 points increase in error, 0 points decrease in error
(log1p.f64 (-.f64 (*.f64 (/.f64 1 N) (Rewrite<= +-commutative_binary64 (+.f64 N 1))) 1)): 0 points increase in error, 0 points decrease in error
(log1p.f64 (-.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 1 (+.f64 N 1)) N)) 1)): 8 points increase in error, 0 points decrease in error
(log1p.f64 (-.f64 (Rewrite<= associate-*r/_binary64 (*.f64 1 (/.f64 (+.f64 N 1) N))) 1)): 0 points increase in error, 8 points decrease in error
(log1p.f64 (-.f64 (Rewrite=> *-lft-identity_binary64 (/.f64 (+.f64 N 1) N)) 1)): 8 points increase in error, 0 points decrease in error
Applied egg-rr28.9
\[\leadsto \color{blue}{\left(1 + \mathsf{log1p}\left(\frac{1}{N}\right)\right) - 1}
\]
Simplified0.0
\[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{N}\right)}
\]
Proof
(log1p.f64 (/.f64 1 N)): 0 points increase in error, 0 points decrease in error
(Rewrite<= +-rgt-identity_binary64 (+.f64 (log1p.f64 (/.f64 1 N)) 0)): 2 points increase in error, 0 points decrease in error
(+.f64 (log1p.f64 (/.f64 1 N)) (Rewrite<= metadata-eval (-.f64 1 1))): 0 points increase in error, 2 points decrease in error
(Rewrite<= associate--l+_binary64 (-.f64 (+.f64 (log1p.f64 (/.f64 1 N)) 1) 1)): 0 points increase in error, 2 points decrease in error
(-.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 (log1p.f64 (/.f64 1 N)))) 1): 0 points increase in error, 0 points decrease in error
Final simplification0.0
\[\leadsto \mathsf{log1p}\left(\frac{1}{N}\right)
\]