Initial program 32.2
\[0.5 \cdot \sqrt{2 \cdot \left(\sqrt{re \cdot re + im \cdot im} - re\right)}\]
- Using strategy
rm Applied flip--35.6
\[\leadsto 0.5 \cdot \sqrt{2 \cdot \color{blue}{\frac{\sqrt{re \cdot re + im \cdot im} \cdot \sqrt{re \cdot re + im \cdot im} - re \cdot re}{\sqrt{re \cdot re + im \cdot im} + re}}}\]
Applied associate-*r/35.6
\[\leadsto 0.5 \cdot \sqrt{\color{blue}{\frac{2 \cdot \left(\sqrt{re \cdot re + im \cdot im} \cdot \sqrt{re \cdot re + im \cdot im} - re \cdot re\right)}{\sqrt{re \cdot re + im \cdot im} + re}}}\]
Applied sqrt-div35.9
\[\leadsto 0.5 \cdot \color{blue}{\frac{\sqrt{2 \cdot \left(\sqrt{re \cdot re + im \cdot im} \cdot \sqrt{re \cdot re + im \cdot im} - re \cdot re\right)}}{\sqrt{\sqrt{re \cdot re + im \cdot im} + re}}}\]
Simplified31.3
\[\leadsto 0.5 \cdot \frac{\color{blue}{\sqrt{\left(im \cdot im\right) \cdot 2}}}{\sqrt{\sqrt{re \cdot re + im \cdot im} + re}}\]
Simplified31.3
\[\leadsto 0.5 \cdot \frac{\sqrt{\left(im \cdot im\right) \cdot 2}}{\color{blue}{\sqrt{re + \sqrt{re \cdot re + im \cdot im}}}}\]
- Using strategy
rm Applied *-un-lft-identity31.3
\[\leadsto 0.5 \cdot \frac{\sqrt{\left(im \cdot im\right) \cdot 2}}{\sqrt{\color{blue}{1 \cdot \left(re + \sqrt{re \cdot re + im \cdot im}\right)}}}\]
Applied sqrt-prod31.3
\[\leadsto 0.5 \cdot \frac{\sqrt{\left(im \cdot im\right) \cdot 2}}{\color{blue}{\sqrt{1} \cdot \sqrt{re + \sqrt{re \cdot re + im \cdot im}}}}\]
Applied sqrt-prod31.3
\[\leadsto 0.5 \cdot \frac{\color{blue}{\sqrt{im \cdot im} \cdot \sqrt{2}}}{\sqrt{1} \cdot \sqrt{re + \sqrt{re \cdot re + im \cdot im}}}\]
Applied times-frac31.3
\[\leadsto 0.5 \cdot \color{blue}{\left(\frac{\sqrt{im \cdot im}}{\sqrt{1}} \cdot \frac{\sqrt{2}}{\sqrt{re + \sqrt{re \cdot re + im \cdot im}}}\right)}\]
Simplified25.7
\[\leadsto 0.5 \cdot \left(\color{blue}{\left|im\right|} \cdot \frac{\sqrt{2}}{\sqrt{re + \sqrt{re \cdot re + im \cdot im}}}\right)\]
- Using strategy
rm Applied sqrt-undiv25.6
\[\leadsto 0.5 \cdot \left(\left|im\right| \cdot \color{blue}{\sqrt{\frac{2}{re + \sqrt{re \cdot re + im \cdot im}}}}\right)\]
- Using strategy
rm Applied *-un-lft-identity25.6
\[\leadsto 0.5 \cdot \left(\left|im\right| \cdot \sqrt{\frac{2}{\color{blue}{1 \cdot \left(re + \sqrt{re \cdot re + im \cdot im}\right)}}}\right)\]
Applied add-sqr-sqrt25.8
\[\leadsto 0.5 \cdot \left(\left|im\right| \cdot \sqrt{\frac{\color{blue}{\sqrt{2} \cdot \sqrt{2}}}{1 \cdot \left(re + \sqrt{re \cdot re + im \cdot im}\right)}}\right)\]
Applied times-frac25.7
\[\leadsto 0.5 \cdot \left(\left|im\right| \cdot \sqrt{\color{blue}{\frac{\sqrt{2}}{1} \cdot \frac{\sqrt{2}}{re + \sqrt{re \cdot re + im \cdot im}}}}\right)\]
Applied sqrt-prod25.6
\[\leadsto 0.5 \cdot \left(\left|im\right| \cdot \color{blue}{\left(\sqrt{\frac{\sqrt{2}}{1}} \cdot \sqrt{\frac{\sqrt{2}}{re + \sqrt{re \cdot re + im \cdot im}}}\right)}\right)\]
Applied associate-*r*25.6
\[\leadsto 0.5 \cdot \color{blue}{\left(\left(\left|im\right| \cdot \sqrt{\frac{\sqrt{2}}{1}}\right) \cdot \sqrt{\frac{\sqrt{2}}{re + \sqrt{re \cdot re + im \cdot im}}}\right)}\]
Simplified25.6
\[\leadsto 0.5 \cdot \left(\color{blue}{\left(\left|im\right| \cdot \sqrt{\sqrt{2}}\right)} \cdot \sqrt{\frac{\sqrt{2}}{re + \sqrt{re \cdot re + im \cdot im}}}\right)\]
Initial program 60.3
\[0.5 \cdot \sqrt{2 \cdot \left(\sqrt{re \cdot re + im \cdot im} - re\right)}\]
- Using strategy
rm Applied flip--60.3
\[\leadsto 0.5 \cdot \sqrt{2 \cdot \color{blue}{\frac{\sqrt{re \cdot re + im \cdot im} \cdot \sqrt{re \cdot re + im \cdot im} - re \cdot re}{\sqrt{re \cdot re + im \cdot im} + re}}}\]
Applied associate-*r/60.3
\[\leadsto 0.5 \cdot \sqrt{\color{blue}{\frac{2 \cdot \left(\sqrt{re \cdot re + im \cdot im} \cdot \sqrt{re \cdot re + im \cdot im} - re \cdot re\right)}{\sqrt{re \cdot re + im \cdot im} + re}}}\]
Applied sqrt-div60.3
\[\leadsto 0.5 \cdot \color{blue}{\frac{\sqrt{2 \cdot \left(\sqrt{re \cdot re + im \cdot im} \cdot \sqrt{re \cdot re + im \cdot im} - re \cdot re\right)}}{\sqrt{\sqrt{re \cdot re + im \cdot im} + re}}}\]
Simplified43.2
\[\leadsto 0.5 \cdot \frac{\color{blue}{\sqrt{\left(im \cdot im\right) \cdot 2}}}{\sqrt{\sqrt{re \cdot re + im \cdot im} + re}}\]
Simplified43.2
\[\leadsto 0.5 \cdot \frac{\sqrt{\left(im \cdot im\right) \cdot 2}}{\color{blue}{\sqrt{re + \sqrt{re \cdot re + im \cdot im}}}}\]
- Using strategy
rm Applied *-un-lft-identity43.2
\[\leadsto 0.5 \cdot \frac{\sqrt{\left(im \cdot im\right) \cdot 2}}{\sqrt{\color{blue}{1 \cdot \left(re + \sqrt{re \cdot re + im \cdot im}\right)}}}\]
Applied sqrt-prod43.2
\[\leadsto 0.5 \cdot \frac{\sqrt{\left(im \cdot im\right) \cdot 2}}{\color{blue}{\sqrt{1} \cdot \sqrt{re + \sqrt{re \cdot re + im \cdot im}}}}\]
Applied sqrt-prod43.2
\[\leadsto 0.5 \cdot \frac{\color{blue}{\sqrt{im \cdot im} \cdot \sqrt{2}}}{\sqrt{1} \cdot \sqrt{re + \sqrt{re \cdot re + im \cdot im}}}\]
Applied times-frac43.2
\[\leadsto 0.5 \cdot \color{blue}{\left(\frac{\sqrt{im \cdot im}}{\sqrt{1}} \cdot \frac{\sqrt{2}}{\sqrt{re + \sqrt{re \cdot re + im \cdot im}}}\right)}\]
Simplified40.1
\[\leadsto 0.5 \cdot \left(\color{blue}{\left|im\right|} \cdot \frac{\sqrt{2}}{\sqrt{re + \sqrt{re \cdot re + im \cdot im}}}\right)\]
- Using strategy
rm Applied sqrt-undiv40.0
\[\leadsto 0.5 \cdot \left(\left|im\right| \cdot \color{blue}{\sqrt{\frac{2}{re + \sqrt{re \cdot re + im \cdot im}}}}\right)\]
Taylor expanded around inf 10.4
\[\leadsto 0.5 \cdot \left(\left|im\right| \cdot \sqrt{\frac{2}{re + \color{blue}{re}}}\right)\]