Initial program 0.1
\[\frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}
\]
Simplified0.1
\[\leadsto \color{blue}{\frac{\frac{\alpha + 1}{\left(\alpha + \left(\beta + 2\right)\right) \cdot \frac{\alpha + \left(\beta + 2\right)}{\beta + 1}}}{\alpha + \left(\beta + 3\right)}}
\]
Proof
(/.f64 (/.f64 (+.f64 alpha 1) (*.f64 (+.f64 alpha (+.f64 beta 2)) (/.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 alpha)) (*.f64 (+.f64 alpha (+.f64 beta 2)) (/.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (+.f64 1 alpha) (*.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) 2)) (/.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (+.f64 1 alpha) (*.f64 (+.f64 (+.f64 alpha beta) (Rewrite<= metadata-eval (*.f64 2 1))) (/.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 13 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (+.f64 1 alpha) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 13 points decrease in error
(/.f64 (/.f64 (+.f64 1 alpha) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (/.f64 (+.f64 (+.f64 alpha beta) (Rewrite<= metadata-eval (*.f64 2 1))) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (+.f64 1 alpha) (/.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 beta 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1)))) (+.f64 alpha (+.f64 beta 3))): 13 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 1 alpha) (+.f64 beta 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1)))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 13 points decrease in error
(/.f64 (/.f64 (/.f64 (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 alpha 1)) (+.f64 beta 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 alpha (+.f64 beta 1)) (+.f64 beta 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 13 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 beta 1) alpha)) (+.f64 beta 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 13 points decrease in error
(/.f64 (/.f64 (/.f64 (+.f64 (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 beta alpha) alpha)) (+.f64 beta 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 beta alpha) (+.f64 alpha (+.f64 beta 1)))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (+.f64 (*.f64 beta alpha) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 beta alpha) (+.f64 alpha beta)) 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) (*.f64 beta alpha))) 1) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.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 alpha (+.f64 beta (Rewrite<= metadata-eval (+.f64 2 1))))): 20 points increase in error, 0 points decrease in error
(/.f64 (/.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))) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (+.f64 2 1)))): 0 points increase in error, 20 points decrease in error
(/.f64 (/.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))) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 alpha beta) 2) 1))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.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) (Rewrite<= metadata-eval (*.f64 2 1))) 1)): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.1
\[\leadsto \frac{\frac{\alpha + 1}{\color{blue}{\frac{2 + \left(\alpha + \beta\right)}{\frac{-1 - \beta}{-2 - \left(\alpha + \beta\right)}}}}}{\alpha + \left(\beta + 3\right)}
\]
Applied egg-rr0.1
\[\leadsto \color{blue}{\frac{\alpha + 1}{\alpha + \left(2 + \beta\right)} \cdot \left(\frac{-1 - \beta}{-2 - \left(\alpha + \beta\right)} \cdot \frac{1}{\alpha + \left(\beta + 3\right)}\right)}
\]
Simplified0.1
\[\leadsto \color{blue}{\frac{1 + \alpha}{\left(2 + \alpha\right) + \beta} \cdot \frac{-1 - \beta}{\left(\left(\beta + 3\right) + \alpha\right) \cdot \left(-2 - \left(\beta + \alpha\right)\right)}}
\]
Proof
(*.f64 (/.f64 (+.f64 1 alpha) (+.f64 (+.f64 2 alpha) beta)) (/.f64 (-.f64 -1 beta) (*.f64 (+.f64 (+.f64 beta 3) alpha) (-.f64 -2 (+.f64 beta alpha))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 alpha 1)) (+.f64 (+.f64 2 alpha) beta)) (/.f64 (-.f64 -1 beta) (*.f64 (+.f64 (+.f64 beta 3) alpha) (-.f64 -2 (+.f64 beta alpha))))): 0 points increase in error, 3 points decrease in error
(*.f64 (/.f64 (+.f64 alpha 1) (+.f64 (Rewrite=> +-commutative_binary64 (+.f64 alpha 2)) beta)) (/.f64 (-.f64 -1 beta) (*.f64 (+.f64 (+.f64 beta 3) alpha) (-.f64 -2 (+.f64 beta alpha))))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 alpha 1) (Rewrite<= associate-+r+_binary64 (+.f64 alpha (+.f64 2 beta)))) (/.f64 (-.f64 -1 beta) (*.f64 (+.f64 (+.f64 beta 3) alpha) (-.f64 -2 (+.f64 beta alpha))))): 6 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 alpha 1) (+.f64 alpha (+.f64 2 beta))) (/.f64 (-.f64 -1 beta) (*.f64 (Rewrite<= +-commutative_binary64 (+.f64 alpha (+.f64 beta 3))) (-.f64 -2 (+.f64 beta alpha))))): 0 points increase in error, 6 points decrease in error
(*.f64 (/.f64 (+.f64 alpha 1) (+.f64 alpha (+.f64 2 beta))) (/.f64 (-.f64 -1 beta) (*.f64 (+.f64 alpha (+.f64 beta 3)) (-.f64 -2 (Rewrite<= +-commutative_binary64 (+.f64 alpha beta)))))): 9 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 alpha 1) (+.f64 alpha (+.f64 2 beta))) (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (-.f64 -1 beta) (-.f64 -2 (+.f64 alpha beta))) (+.f64 alpha (+.f64 beta 3))))): 0 points increase in error, 9 points decrease in error
(*.f64 (/.f64 (+.f64 alpha 1) (+.f64 alpha (+.f64 2 beta))) (/.f64 (Rewrite<= *-rgt-identity_binary64 (*.f64 (/.f64 (-.f64 -1 beta) (-.f64 -2 (+.f64 alpha beta))) 1)) (+.f64 alpha (+.f64 beta 3)))): 0 points increase in error, 0 points decrease in error
(*.f64 (/.f64 (+.f64 alpha 1) (+.f64 alpha (+.f64 2 beta))) (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 (-.f64 -1 beta) (-.f64 -2 (+.f64 alpha beta))) (/.f64 1 (+.f64 alpha (+.f64 beta 3)))))): 0 points increase in error, 0 points decrease in error
Initial program 6.6
\[\frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1}
\]
Simplified0.1
\[\leadsto \color{blue}{\frac{\frac{\alpha + 1}{\left(\alpha + \left(\beta + 2\right)\right) \cdot \frac{\alpha + \left(\beta + 2\right)}{\beta + 1}}}{\alpha + \left(\beta + 3\right)}}
\]
Proof
(/.f64 (/.f64 (+.f64 alpha 1) (*.f64 (+.f64 alpha (+.f64 beta 2)) (/.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 alpha)) (*.f64 (+.f64 alpha (+.f64 beta 2)) (/.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (+.f64 1 alpha) (*.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) 2)) (/.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (+.f64 1 alpha) (*.f64 (+.f64 (+.f64 alpha beta) (Rewrite<= metadata-eval (*.f64 2 1))) (/.f64 (+.f64 alpha (+.f64 beta 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 13 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (+.f64 1 alpha) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) 2)) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 13 points decrease in error
(/.f64 (/.f64 (+.f64 1 alpha) (*.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (/.f64 (+.f64 (+.f64 alpha beta) (Rewrite<= metadata-eval (*.f64 2 1))) (+.f64 beta 1)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-/l/_binary64 (/.f64 (/.f64 (+.f64 1 alpha) (/.f64 (+.f64 (+.f64 alpha beta) (*.f64 2 1)) (+.f64 beta 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1)))) (+.f64 alpha (+.f64 beta 3))): 13 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 (+.f64 1 alpha) (+.f64 beta 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1)))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 13 points decrease in error
(/.f64 (/.f64 (/.f64 (*.f64 (Rewrite=> +-commutative_binary64 (+.f64 alpha 1)) (+.f64 beta 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 alpha (+.f64 beta 1)) (+.f64 beta 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 13 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (+.f64 (Rewrite<= *-commutative_binary64 (*.f64 (+.f64 beta 1) alpha)) (+.f64 beta 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 13 points decrease in error
(/.f64 (/.f64 (/.f64 (+.f64 (Rewrite<= distribute-lft1-in_binary64 (+.f64 (*.f64 beta alpha) alpha)) (+.f64 beta 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (Rewrite<= associate-+r+_binary64 (+.f64 (*.f64 beta alpha) (+.f64 alpha (+.f64 beta 1)))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (+.f64 (*.f64 beta alpha) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (*.f64 beta alpha) (+.f64 alpha beta)) 1)) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.f64 (/.f64 (+.f64 (Rewrite<= +-commutative_binary64 (+.f64 (+.f64 alpha beta) (*.f64 beta alpha))) 1) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 (+.f64 alpha beta) (*.f64 2 1))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.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 alpha (+.f64 beta (Rewrite<= metadata-eval (+.f64 2 1))))): 20 points increase in error, 0 points decrease in error
(/.f64 (/.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))) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 alpha beta) (+.f64 2 1)))): 0 points increase in error, 20 points decrease in error
(/.f64 (/.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))) (Rewrite<= associate-+l+_binary64 (+.f64 (+.f64 (+.f64 alpha beta) 2) 1))): 0 points increase in error, 0 points decrease in error
(/.f64 (/.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) (Rewrite<= metadata-eval (*.f64 2 1))) 1)): 0 points increase in error, 0 points decrease in error
Applied egg-rr0.2
\[\leadsto \frac{\frac{\alpha + 1}{\left(\alpha + \left(\beta + 2\right)\right) \cdot \color{blue}{\left(\frac{-1}{-1 - \beta} \cdot \left(2 + \left(\alpha + \beta\right)\right)\right)}}}{\alpha + \left(\beta + 3\right)}
\]
Applied egg-rr0.2
\[\leadsto \frac{\color{blue}{\frac{1}{\beta + \left(2 + \alpha\right)} \cdot \frac{\alpha + 1}{\frac{\beta + \left(2 + \alpha\right)}{-\left(-1 - \beta\right)}}}}{\alpha + \left(\beta + 3\right)}
\]
Simplified0.2
\[\leadsto \frac{\color{blue}{\frac{\alpha + 1}{2 + \left(\alpha + \beta\right)} \cdot \left(\left(\beta + 1\right) \cdot \frac{1}{2 + \left(\alpha + \beta\right)}\right)}}{\alpha + \left(\beta + 3\right)}
\]
Proof
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 2 (+.f64 alpha beta))) (*.f64 (+.f64 beta 1) (/.f64 1 (+.f64 2 (+.f64 alpha beta))))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 2 alpha) beta))) (*.f64 (+.f64 beta 1) (/.f64 1 (+.f64 2 (+.f64 alpha beta))))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (Rewrite<= +-commutative_binary64 (+.f64 beta (+.f64 2 alpha)))) (*.f64 (+.f64 beta 1) (/.f64 1 (+.f64 2 (+.f64 alpha beta))))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 beta (+.f64 2 alpha))) (*.f64 (+.f64 beta 1) (/.f64 1 (Rewrite=> associate-+r+_binary64 (+.f64 (+.f64 2 alpha) beta))))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 beta (+.f64 2 alpha))) (*.f64 (+.f64 beta 1) (/.f64 1 (Rewrite<= +-commutative_binary64 (+.f64 beta (+.f64 2 alpha)))))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= associate-*l*_binary64 (*.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 beta (+.f64 2 alpha))) (+.f64 beta 1)) (/.f64 1 (+.f64 beta (+.f64 2 alpha))))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 1 alpha)) (+.f64 beta (+.f64 2 alpha))) (+.f64 beta 1)) (/.f64 1 (+.f64 beta (+.f64 2 alpha)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 beta (+.f64 2 alpha))) (Rewrite=> +-commutative_binary64 (+.f64 1 beta))) (/.f64 1 (+.f64 beta (+.f64 2 alpha)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 beta (+.f64 2 alpha))) (+.f64 (Rewrite<= metadata-eval (-.f64 0 -1)) beta)) (/.f64 1 (+.f64 beta (+.f64 2 alpha)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 beta (+.f64 2 alpha))) (Rewrite<= associate--r-_binary64 (-.f64 0 (-.f64 -1 beta)))) (/.f64 1 (+.f64 beta (+.f64 2 alpha)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (*.f64 (/.f64 (+.f64 1 alpha) (+.f64 beta (+.f64 2 alpha))) (Rewrite<= neg-sub0_binary64 (neg.f64 (-.f64 -1 beta)))) (/.f64 1 (+.f64 beta (+.f64 2 alpha)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (+.f64 1 alpha) (/.f64 (+.f64 beta (+.f64 2 alpha)) (neg.f64 (-.f64 -1 beta))))) (/.f64 1 (+.f64 beta (+.f64 2 alpha)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (Rewrite=> +-commutative_binary64 (+.f64 alpha 1)) (/.f64 (+.f64 beta (+.f64 2 alpha)) (neg.f64 (-.f64 -1 beta)))) (/.f64 1 (+.f64 beta (+.f64 2 alpha)))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 1 (+.f64 beta (+.f64 2 alpha))) (/.f64 (+.f64 alpha 1) (/.f64 (+.f64 beta (+.f64 2 alpha)) (neg.f64 (-.f64 -1 beta)))))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
Taylor expanded in beta around inf 0.3
\[\leadsto \frac{\frac{\alpha + 1}{2 + \left(\alpha + \beta\right)} \cdot \color{blue}{\left(1 + -1 \cdot \frac{1 + \alpha}{\beta}\right)}}{\alpha + \left(\beta + 3\right)}
\]
Simplified0.3
\[\leadsto \frac{\frac{\alpha + 1}{2 + \left(\alpha + \beta\right)} \cdot \color{blue}{\left(1 + \frac{-1 - \alpha}{\beta}\right)}}{\alpha + \left(\beta + 3\right)}
\]
Proof
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 2 (+.f64 alpha beta))) (+.f64 1 (/.f64 (-.f64 -1 alpha) beta))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 2 (+.f64 alpha beta))) (+.f64 1 (/.f64 (-.f64 (Rewrite<= metadata-eval (-.f64 0 1)) alpha) beta))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 2 (+.f64 alpha beta))) (+.f64 1 (/.f64 (Rewrite<= associate--r+_binary64 (-.f64 0 (+.f64 1 alpha))) beta))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 2 (+.f64 alpha beta))) (+.f64 1 (/.f64 (Rewrite<= neg-sub0_binary64 (neg.f64 (+.f64 1 alpha))) beta))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 2 (+.f64 alpha beta))) (+.f64 1 (/.f64 (Rewrite<= mul-1-neg_binary64 (*.f64 -1 (+.f64 1 alpha))) beta))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error
(/.f64 (*.f64 (/.f64 (+.f64 alpha 1) (+.f64 2 (+.f64 alpha beta))) (+.f64 1 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (+.f64 1 alpha) beta))))) (+.f64 alpha (+.f64 beta 3))): 0 points increase in error, 0 points decrease in error