Initial program 14.0
\[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)
\]
Simplified14.0
\[\leadsto \color{blue}{\frac{\frac{\pi}{2}}{b \cdot b - a \cdot a} \cdot \left(\frac{1}{a} + \frac{-1}{b}\right)}
\]
Proof
(*.f64 (/.f64 (/.f64 (PI.f64) 2) (-.f64 (*.f64 b b) (*.f64 a a))) (+.f64 (/.f64 1 a) (/.f64 -1 b))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (/.f64 (PI.f64) 2) (-.f64 (*.f64 b b) (*.f64 a a))) (+.f64 (/.f64 1 a) (/.f64 (Rewrite<= metadata-eval (neg.f64 1)) b))): 6 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (/.f64 (PI.f64) 2) (-.f64 (*.f64 b b) (*.f64 a a))) (+.f64 (/.f64 1 a) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 1 b))))): 0 points increase in error, 6 points decrease in error
(*.f64 (/.f64 (/.f64 (PI.f64) 2) (-.f64 (*.f64 b b) (*.f64 a a))) (Rewrite<= sub-neg_binary64 (-.f64 (/.f64 1 a) (/.f64 1 b)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (/.f64 (PI.f64) 2) 1)) (-.f64 (*.f64 b b) (*.f64 a a))) (-.f64 (/.f64 1 a) (/.f64 1 b))): 6 points increase in error, 0 points decrease in error
(*.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (PI.f64) 2) (/.f64 1 (-.f64 (*.f64 b b) (*.f64 a a))))) (-.f64 (/.f64 1 a) (/.f64 1 b))): 0 points increase in error, 6 points decrease in error
Applied egg-rr29.2
\[\leadsto \color{blue}{e^{\mathsf{log1p}\left(\frac{\pi \cdot 0.5}{\left(b + a\right) \cdot \left(b \cdot a\right)}\right)} - 1}
\]
Simplified0.3
\[\leadsto \color{blue}{\frac{\pi}{a + b} \cdot \frac{0.5}{a \cdot b}}
\]
Proof
(*.f64 (/.f64 (PI.f64) (+.f64 a b)) (/.f64 1/2 (*.f64 a b))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (PI.f64) (Rewrite<= +-commutative_binary64 (+.f64 b a))) (/.f64 1/2 (*.f64 a b))): 5 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (PI.f64) (+.f64 b a)) (/.f64 1/2 (Rewrite<= *-commutative_binary64 (*.f64 b a)))): 0 points increase in error, 5 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 (PI.f64) 1/2) (*.f64 (+.f64 b a) (*.f64 b a)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= expm1-log1p_binary64 (expm1.f64 (log1p.f64 (/.f64 (*.f64 (PI.f64) 1/2) (*.f64 (+.f64 b a) (*.f64 b a)))))): 3 points increase in error, 0 points decrease in error
(Rewrite<= expm1-def_binary64 (-.f64 (exp.f64 (log1p.f64 (/.f64 (*.f64 (PI.f64) 1/2) (*.f64 (+.f64 b a) (*.f64 b a))))) 1)): 0 points increase in error, 3 points decrease in error
Final simplification0.3
\[\leadsto \frac{\pi}{a + b} \cdot \frac{0.5}{a \cdot b}
\]