Initial program 28.5
\[\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1}\]
- Using strategy
rm Applied difference-of-sqr-1_binary64_175328.5
\[\leadsto \frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\color{blue}{\left(\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 1\right) \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1\right)}}\]
Applied times-frac_binary64_178912.4
\[\leadsto \frac{\color{blue}{\frac{i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i} \cdot \frac{\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}}{\left(\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 1\right) \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1\right)}\]
Applied times-frac_binary64_17897.6
\[\leadsto \color{blue}{\frac{\frac{i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 1} \cdot \frac{\frac{\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1}}\]
Simplified7.6
\[\leadsto \color{blue}{\frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1}} \cdot \frac{\frac{\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1}\]
Simplified7.6
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \color{blue}{\frac{\frac{\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1}}\]
- Using strategy
rm Applied *-un-lft-identity_binary64_17837.6
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\color{blue}{1 \cdot \left(\left(\alpha + \beta\right) + i \cdot 2\right)}}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \frac{\frac{\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1}\]
Applied times-frac_binary64_17897.5
\[\leadsto \frac{\color{blue}{\frac{i}{1} \cdot \frac{i + \left(\alpha + \beta\right)}{\left(\alpha + \beta\right) + i \cdot 2}}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \frac{\frac{\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1}\]
Simplified7.5
\[\leadsto \frac{\color{blue}{i} \cdot \frac{i + \left(\alpha + \beta\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \frac{\frac{\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1}\]
Initial program 64.0
\[\frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1}\]
- Using strategy
rm Applied difference-of-sqr-1_binary64_175364.0
\[\leadsto \frac{\frac{\left(i \cdot \left(\left(\alpha + \beta\right) + i\right)\right) \cdot \left(\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)\right)}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) \cdot \left(\left(\alpha + \beta\right) + 2 \cdot i\right)}}{\color{blue}{\left(\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 1\right) \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1\right)}}\]
Applied times-frac_binary64_178921.3
\[\leadsto \frac{\color{blue}{\frac{i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i} \cdot \frac{\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}}{\left(\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 1\right) \cdot \left(\left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1\right)}\]
Applied times-frac_binary64_178921.3
\[\leadsto \color{blue}{\frac{\frac{i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) + 1} \cdot \frac{\frac{\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1}}\]
Simplified21.3
\[\leadsto \color{blue}{\frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1}} \cdot \frac{\frac{\beta \cdot \alpha + i \cdot \left(\left(\alpha + \beta\right) + i\right)}{\left(\alpha + \beta\right) + 2 \cdot i}}{\left(\left(\alpha + \beta\right) + 2 \cdot i\right) - 1}\]
Simplified21.3
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \color{blue}{\frac{\frac{\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1}}\]
- Using strategy
rm Applied add-exp-log_binary64_182125.5
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \frac{\frac{\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\color{blue}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}}}\]
Applied add-exp-log_binary64_182126.2
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \frac{\frac{\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\color{blue}{e^{\log \left(\left(\alpha + \beta\right) + i \cdot 2\right)}}}}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}}\]
Applied add-exp-log_binary64_182124.7
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \frac{\frac{\color{blue}{e^{\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right)}}}{e^{\log \left(\left(\alpha + \beta\right) + i \cdot 2\right)}}}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}}\]
Applied div-exp_binary64_183424.7
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \frac{\color{blue}{e^{\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)}}}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}}\]
Applied div-exp_binary64_183424.8
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \color{blue}{e^{\left(\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}}\]
Applied add-exp-log_binary64_182125.3
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\color{blue}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1\right)}}} \cdot e^{\left(\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}\]
Applied add-exp-log_binary64_182126.1
\[\leadsto \frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\color{blue}{e^{\log \left(\left(\alpha + \beta\right) + i \cdot 2\right)}}}}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1\right)}} \cdot e^{\left(\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}\]
Applied add-exp-log_binary64_182125.1
\[\leadsto \frac{\frac{i \cdot \color{blue}{e^{\log \left(i + \left(\alpha + \beta\right)\right)}}}{e^{\log \left(\left(\alpha + \beta\right) + i \cdot 2\right)}}}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1\right)}} \cdot e^{\left(\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}\]
Applied add-exp-log_binary64_182125.4
\[\leadsto \frac{\frac{\color{blue}{e^{\log i}} \cdot e^{\log \left(i + \left(\alpha + \beta\right)\right)}}{e^{\log \left(\left(\alpha + \beta\right) + i \cdot 2\right)}}}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1\right)}} \cdot e^{\left(\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}\]
Applied prod-exp_binary64_183225.4
\[\leadsto \frac{\frac{\color{blue}{e^{\log i + \log \left(i + \left(\alpha + \beta\right)\right)}}}{e^{\log \left(\left(\alpha + \beta\right) + i \cdot 2\right)}}}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1\right)}} \cdot e^{\left(\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}\]
Applied div-exp_binary64_183425.4
\[\leadsto \frac{\color{blue}{e^{\left(\log i + \log \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)}}}{e^{\log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1\right)}} \cdot e^{\left(\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}\]
Applied div-exp_binary64_183425.4
\[\leadsto \color{blue}{e^{\left(\left(\log i + \log \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1\right)}} \cdot e^{\left(\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)}\]
Applied prod-exp_binary64_183225.4
\[\leadsto \color{blue}{e^{\left(\left(\left(\log i + \log \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1\right)\right) + \left(\left(\log \left(\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)\right) - \log \left(\left(\alpha + \beta\right) + i \cdot 2\right)\right) - \log \left(\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1\right)\right)}}\]
Simplified21.3
\[\leadsto e^{\color{blue}{\log \left(\frac{\frac{i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) + 1} \cdot \frac{\frac{\alpha \cdot \beta + i \cdot \left(i + \left(\alpha + \beta\right)\right)}{\left(\alpha + \beta\right) + i \cdot 2}}{\left(\left(\alpha + \beta\right) + i \cdot 2\right) - 1}\right)}}\]