- Split input into 2 regimes
if (/ (/ (/ (+ (+ (+ alpha beta) (* beta alpha)) 1.0) (+ (+ alpha beta) (* 2 1))) (+ (+ alpha beta) (* 2 1))) (+ (+ (+ alpha beta) (* 2 1)) 1.0)) < 0.08379260992851913
Initial program 0.1
\[\frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}\]
- Using strategy
rm Applied div-inv0.1
\[\leadsto \frac{\color{blue}{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1} \cdot \frac{1}{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}\]
if 0.08379260992851913 < (/ (/ (/ (+ (+ (+ alpha beta) (* beta alpha)) 1.0) (+ (+ alpha beta) (* 2 1))) (+ (+ alpha beta) (* 2 1))) (+ (+ (+ alpha beta) (* 2 1)) 1.0))
Initial program 61.4
\[\frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}\]
- Using strategy
rm Applied *-un-lft-identity61.4
\[\leadsto \frac{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\color{blue}{1 \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0\right)}}\]
Applied add-sqr-sqrt61.4
\[\leadsto \frac{\color{blue}{\sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}} \cdot \sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}}}{1 \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0\right)}\]
Applied times-frac61.4
\[\leadsto \color{blue}{\frac{\sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}}{1} \cdot \frac{\sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}}\]
Simplified61.4
\[\leadsto \color{blue}{\sqrt{\frac{\frac{(\beta \cdot \alpha + \beta)_* + \left(1.0 + \alpha\right)}{\beta + \left(\alpha + 2\right)}}{\beta + \left(\alpha + 2\right)}}} \cdot \frac{\sqrt{\frac{\frac{\left(\left(\alpha + \beta\right) + \beta \cdot \alpha\right) + 1.0}{\left(\alpha + \beta\right) + 2 \cdot 1}}{\left(\alpha + \beta\right) + 2 \cdot 1}}}{\left(\left(\alpha + \beta\right) + 2 \cdot 1\right) + 1.0}\]
Simplified61.4
\[\leadsto \sqrt{\frac{\frac{(\beta \cdot \alpha + \beta)_* + \left(1.0 + \alpha\right)}{\beta + \left(\alpha + 2\right)}}{\beta + \left(\alpha + 2\right)}} \cdot \color{blue}{\frac{\sqrt{\frac{\frac{\left(\beta + 1.0\right) + (\beta \cdot \alpha + \alpha)_*}{\left(2 + \beta\right) + \alpha}}{\left(2 + \beta\right) + \alpha}}}{\left(1.0 + \alpha\right) + \left(2 + \beta\right)}}\]
Taylor expanded around inf 19.0
\[\leadsto \color{blue}{0}\]
- Recombined 2 regimes into one program.
Final simplification1.2
\[\leadsto \begin{array}{l}
\mathbf{if}\;\frac{\frac{\frac{1.0 + \left(\alpha \cdot \beta + \left(\beta + \alpha\right)\right)}{2 + \left(\beta + \alpha\right)}}{2 + \left(\beta + \alpha\right)}}{\left(2 + \left(\beta + \alpha\right)\right) + 1.0} \le 0.08379260992851913:\\
\;\;\;\;\frac{\frac{1.0 + \left(\alpha \cdot \beta + \left(\beta + \alpha\right)\right)}{2 + \left(\beta + \alpha\right)} \cdot \frac{1}{2 + \left(\beta + \alpha\right)}}{\left(2 + \left(\beta + \alpha\right)\right) + 1.0}\\
\mathbf{else}:\\
\;\;\;\;0\\
\end{array}\]