Simplified2.0
\[\leadsto \color{blue}{\frac{\frac{\alpha + 1}{\left(\alpha + \beta\right) + 3} \cdot \left(\beta + 1\right)}{\left(\alpha + \left(\beta + 2\right)\right) \cdot \left(\alpha + \left(\beta + 2\right)\right)}}
\]
Proof
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 (+.f64 alpha beta) 3)) (+.f64 beta 1)) (*.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 alpha (+.f64 beta 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 alpha)) (+.f64 (+.f64 alpha beta) 3)) (+.f64 beta 1)) (*.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 alpha (+.f64 beta 2)))): 0 points increase in error, 24 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 (+.f64 alpha beta) (Rewrite<= metadata-eval (+.f64 2 1)))) (+.f64 beta 1)) (*.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 alpha (+.f64 beta 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 1 alpha) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 alpha beta) 2) 1))) (+.f64 beta 1)) (*.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 alpha (+.f64 beta 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 (+.f64 (+.f64 alpha beta) (Rewrite<= metadata-eval (*.f64 2 1))) 1)) (+.f64 beta 1)) (*.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 alpha (+.f64 beta 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 1 alpha) (Rewrite<= /-rgt-identity_binary64 (/.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) 1))) (+.f64 beta 1)) (*.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 alpha (+.f64 beta 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> associate-*l/_binary64 (/.f64 (*.f64 (+.f64 1 alpha) (+.f64 beta 1)) (/.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) 1))) (*.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 alpha (+.f64 beta 2)))): 22 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (*.f64 (+.f64 1 alpha) (+.f64 beta 1)) (Rewrite=> /-rgt-identity_binary64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1))) (*.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 alpha (+.f64 beta 2)))): 0 points increase in error, 21 points decrease in error
(/.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1)) (+.f64 beta 1))) (*.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 alpha (+.f64 beta 2)))): 10 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1)) (+.f64 beta 1)) (*.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) 2)) (+.f64 alpha (+.f64 beta 2)))): 0 points increase in error, 11 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1)) (+.f64 beta 1)) (*.f64 (+.f64 (+.f64 alpha beta) (Rewrite<= metadata-eval (*.f64 2 1))) (+.f64 alpha (+.f64 beta 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1)) (+.f64 beta 1)) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) 2)))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1)) (+.f64 beta 1)) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (Rewrite<= metadata-eval (*.f64 2 1))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1)) (/.f64 (+.f64 beta 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1)))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= times-frac_binary64 (/.f64 (*.f64 (+.f64 1 alpha) (+.f64 beta 1)) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1)))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 beta 1) (+.f64 1 alpha))) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= distribute-rgt1-in_binary64 (+.f64 (+.f64 1 alpha) (*.f64 beta (+.f64 1 alpha)))) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (+.f64 1 alpha) (Rewrite=> distribute-lft-in_binary64 (+.f64 (*.f64 beta 1) (*.f64 beta alpha)))) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 (+.f64 1 alpha) (+.f64 (Rewrite=> *-rgt-identity_binary64 beta) (*.f64 beta alpha))) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-+r+_binary64 (+.f64 1 (+.f64 alpha (+.f64 beta (*.f64 beta alpha))))) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))))): 0 points increase in error, 0 points decrease in error
(/.f64 (+.f64 1 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (*.f64 beta alpha)))) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 beta alpha)) 1)) (*.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))))): 0 points increase in error, 0 points decrease in error
(Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 beta alpha)) 1) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1)))) (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 beta alpha)) 1) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1)))) (+.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) 1)): 0 points increase in error, 0 points decrease in error
Simplified0.1
\[\leadsto \color{blue}{\frac{\frac{1 + \alpha}{\frac{\beta + \left(2 + \alpha\right)}{\beta + 1} \cdot \left(\left(\beta + 3\right) + \alpha\right)}}{\beta + \left(2 + \alpha\right)}}
\]
Proof
(/.f64 (/.f64 (+.f64 1 alpha) (*.f64 (/.f64 (+.f64 beta (+.f64 2 alpha)) (+.f64 beta 1)) (+.f64 (+.f64 beta 3) alpha))) (+.f64 beta (+.f64 2 alpha))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 alpha 1)) (*.f64 (/.f64 (+.f64 beta (+.f64 2 alpha)) (+.f64 beta 1)) (+.f64 (+.f64 beta 3) alpha))) (+.f64 beta (+.f64 2 alpha))): 0 points increase in error, 9 points decrease in error
(/.f64 (/.f64 (+.f64 alpha 1) (*.f64 (/.f64 (+.f64 beta (Rewrite=> +-commutative_binary64 (+.f64 alpha 2))) (+.f64 beta 1)) (+.f64 (+.f64 beta 3) alpha))) (+.f64 beta (+.f64 2 alpha))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (+.f64 alpha 1) (*.f64 (/.f64 (+.f64 beta (+.f64 alpha 2)) (Rewrite=> +-commutative_binary64 (+.f64 1 beta))) (+.f64 (+.f64 beta 3) alpha))) (+.f64 beta (+.f64 2 alpha))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (+.f64 alpha 1) (*.f64 (/.f64 (+.f64 beta (+.f64 alpha 2)) (+.f64 1 beta)) (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta 3))))) (+.f64 beta (+.f64 2 alpha))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (+.f64 alpha 1) (+.f64 alpha (+.f64 beta 3))) (/.f64 (+.f64 beta (+.f64 alpha 2)) (+.f64 1 beta)))) (+.f64 beta (+.f64 2 alpha))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite=> associate-/r/_binary64 (*.f64 (/.f64 (/.f64 (+.f64 alpha 1) (+.f64 alpha (+.f64 beta 3))) (+.f64 beta (+.f64 alpha 2))) (+.f64 1 beta))) (+.f64 beta (+.f64 2 alpha))): 1 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (/.f64 (+.f64 alpha 1) (+.f64 alpha (+.f64 beta 3))) (+.f64 beta (+.f64 alpha 2))) (+.f64 1 beta)) (+.f64 beta (Rewrite=> +-commutative_binary64 (+.f64 alpha 2)))): 0 points increase in error, 1 points decrease in error
(Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (/.f64 (+.f64 alpha 1) (+.f64 alpha (+.f64 beta 3))) (+.f64 beta (+.f64 alpha 2))) (/.f64 (+.f64 1 beta) (+.f64 beta (+.f64 alpha 2))))): 9 points increase in error, 0 points decrease in error