Initial program 14.2
\[\left(\frac{\pi}{2} \cdot \frac{1}{b \cdot b - a \cdot a}\right) \cdot \left(\frac{1}{a} - \frac{1}{b}\right)
\]
Simplified14.2
\[\leadsto \color{blue}{\frac{\pi}{2} \cdot \left(\frac{1}{b \cdot b - a \cdot a} \cdot \left(\frac{1}{a} - \frac{1}{b}\right)\right)}
\]
Proof
(*.f64 (/.f64 (PI.f64) 2) (*.f64 (/.f64 1 (-.f64 (*.f64 b b) (*.f64 a a))) (-.f64 (/.f64 1 a) (/.f64 1 b)))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 (PI.f64) 2) (/.f64 1 (-.f64 (*.f64 b b) (*.f64 a a)))) (-.f64 (/.f64 1 a) (/.f64 1 b)))): 20 points increase in error, 18 points decrease in error
Applied egg-rr18.7
\[\leadsto \frac{\pi}{2} \cdot \color{blue}{\frac{b - a}{\left(b \cdot b - a \cdot a\right) \cdot \left(b \cdot a\right)}}
\]
Simplified0.3
\[\leadsto \frac{\pi}{2} \cdot \color{blue}{\frac{\frac{1}{a + b}}{a \cdot b}}
\]
Proof
(/.f64 (/.f64 1 (+.f64 a b)) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= *-inverses_binary64 (/.f64 (neg.f64 (-.f64 b a)) (neg.f64 (-.f64 b a)))) (+.f64 a b)) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (neg.f64 (-.f64 b a)) (neg.f64 (-.f64 b a))) (Rewrite<= +-commutative_binary64 (+.f64 b a))) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-/r*_binary64 (/.f64 (neg.f64 (-.f64 b a)) (*.f64 (neg.f64 (-.f64 b a)) (+.f64 b a)))) (*.f64 a b)): 48 points increase in error, 10 points decrease in error
(/.f64 (/.f64 (neg.f64 (-.f64 b a)) (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 b a) (neg.f64 (-.f64 b a))))) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 b a))) (*.f64 (+.f64 b a) (neg.f64 (-.f64 b a)))) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (-.f64 b a) -1)) (*.f64 (+.f64 b a) (neg.f64 (-.f64 b a)))) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> times-frac_binary64 (*.f64 (/.f64 (-.f64 b a) (+.f64 b a)) (/.f64 -1 (neg.f64 (-.f64 b a))))) (*.f64 a b)): 10 points increase in error, 48 points decrease in error
(/.f64 (*.f64 (/.f64 (-.f64 b a) (+.f64 b a)) (/.f64 -1 (Rewrite=> neg-mul-1_binary64 (*.f64 -1 (-.f64 b a))))) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (-.f64 b a) (+.f64 b a)) (Rewrite=> associate-/r*_binary64 (/.f64 (/.f64 -1 -1) (-.f64 b a)))) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (-.f64 b a) (+.f64 b a)) (/.f64 (Rewrite=> metadata-eval 1) (-.f64 b a))) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= times-frac_binary64 (/.f64 (*.f64 (-.f64 b a) 1) (*.f64 (+.f64 b a) (-.f64 b a)))) (*.f64 a b)): 48 points increase in error, 10 points decrease in error
(/.f64 (/.f64 (Rewrite=> *-rgt-identity_binary64 (-.f64 b a)) (*.f64 (+.f64 b a) (-.f64 b a))) (*.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (-.f64 b a) (Rewrite<= difference-of-squares_binary64 (-.f64 (*.f64 b b) (*.f64 a a)))) (*.f64 a b)): 22 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (-.f64 b a) (-.f64 (*.f64 b b) (*.f64 a a))) (Rewrite<= *-commutative_binary64 (*.f64 b a))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (-.f64 b a) (*.f64 (-.f64 (*.f64 b b) (*.f64 a a)) (*.f64 b a)))): 42 points increase in error, 17 points decrease in error
Applied egg-rr5.1
\[\leadsto \color{blue}{0 + \frac{\pi \cdot 0.5}{a \cdot \left(b \cdot \left(a + b\right)\right)}}
\]
Simplified0.3
\[\leadsto \color{blue}{\frac{\frac{\frac{\pi}{\frac{a}{0.5}}}{b}}{a + b}}
\]
Proof
(/.f64 (/.f64 (/.f64 (PI.f64) (/.f64 a 1/2)) b) (+.f64 a b)): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (PI.f64) 1/2) a)) b) (+.f64 a b)): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (/.f64 (*.f64 (PI.f64) 1/2) a) (*.f64 b (+.f64 a b)))): 39 points increase in error, 21 points decrease in error
(Rewrite<= associate-/r*_binary64 (/.f64 (*.f64 (PI.f64) 1/2) (*.f64 a (*.f64 b (+.f64 a b))))): 20 points increase in error, 17 points decrease in error
(Rewrite<= +-lft-identity_binary64 (+.f64 0 (/.f64 (*.f64 (PI.f64) 1/2) (*.f64 a (*.f64 b (+.f64 a b)))))): 0 points increase in error, 0 points decrease in error
Final simplification0.3
\[\leadsto \frac{\frac{\frac{\pi}{\frac{a}{0.5}}}{b}}{a + b}
\]