Initial program 0.0
\[x + \frac{y}{500}\]
- Using strategy
rm Applied flip-+_binary64_1198731.4
\[\leadsto \color{blue}{\frac{x \cdot x - \frac{y}{500} \cdot \frac{y}{500}}{x - \frac{y}{500}}}\]
Simplified31.5
\[\leadsto \frac{\color{blue}{x \cdot x - y \cdot \frac{y}{250000}}}{x - \frac{y}{500}}\]
- Using strategy
rm Applied add-sqr-sqrt_binary64_1203547.9
\[\leadsto \frac{x \cdot x - y \cdot \frac{y}{250000}}{x - \color{blue}{\sqrt{\frac{y}{500}} \cdot \sqrt{\frac{y}{500}}}}\]
Applied add-sqr-sqrt_binary64_1203556.1
\[\leadsto \frac{x \cdot x - y \cdot \frac{y}{250000}}{\color{blue}{\sqrt{x} \cdot \sqrt{x}} - \sqrt{\frac{y}{500}} \cdot \sqrt{\frac{y}{500}}}\]
Applied difference-of-squares_binary64_1198256.1
\[\leadsto \frac{x \cdot x - y \cdot \frac{y}{250000}}{\color{blue}{\left(\sqrt{x} + \sqrt{\frac{y}{500}}\right) \cdot \left(\sqrt{x} - \sqrt{\frac{y}{500}}\right)}}\]
Applied *-un-lft-identity_binary64_1201356.1
\[\leadsto \frac{\color{blue}{1 \cdot \left(x \cdot x - y \cdot \frac{y}{250000}\right)}}{\left(\sqrt{x} + \sqrt{\frac{y}{500}}\right) \cdot \left(\sqrt{x} - \sqrt{\frac{y}{500}}\right)}\]
Applied times-frac_binary64_1201956.1
\[\leadsto \color{blue}{\frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - y \cdot \frac{y}{250000}}{\sqrt{x} - \sqrt{\frac{y}{500}}}}\]
- Using strategy
rm Applied add-sqr-sqrt_binary64_1203556.1
\[\leadsto \frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - y \cdot \frac{y}{\color{blue}{\sqrt{250000} \cdot \sqrt{250000}}}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied add-sqr-sqrt_binary64_1203556.1
\[\leadsto \frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - y \cdot \frac{\color{blue}{\sqrt{y} \cdot \sqrt{y}}}{\sqrt{250000} \cdot \sqrt{250000}}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied times-frac_binary64_1201956.1
\[\leadsto \frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - y \cdot \color{blue}{\left(\frac{\sqrt{y}}{\sqrt{250000}} \cdot \frac{\sqrt{y}}{\sqrt{250000}}\right)}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied add-sqr-sqrt_binary64_1203556.1
\[\leadsto \frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - \color{blue}{\left(\sqrt{y} \cdot \sqrt{y}\right)} \cdot \left(\frac{\sqrt{y}}{\sqrt{250000}} \cdot \frac{\sqrt{y}}{\sqrt{250000}}\right)}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied unswap-sqr_binary64_1198156.1
\[\leadsto \frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - \color{blue}{\left(\sqrt{y} \cdot \frac{\sqrt{y}}{\sqrt{250000}}\right) \cdot \left(\sqrt{y} \cdot \frac{\sqrt{y}}{\sqrt{250000}}\right)}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Simplified56.1
\[\leadsto \frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - \color{blue}{\frac{y}{500}} \cdot \left(\sqrt{y} \cdot \frac{\sqrt{y}}{\sqrt{250000}}\right)}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Simplified56.0
\[\leadsto \frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - \frac{y}{500} \cdot \color{blue}{\frac{y}{500}}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
- Using strategy
rm Applied *-un-lft-identity_binary64_1201356.0
\[\leadsto \frac{1}{\sqrt{x} + \sqrt{\color{blue}{1 \cdot \frac{y}{500}}}} \cdot \frac{x \cdot x - \frac{y}{500} \cdot \frac{y}{500}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied sqrt-prod_binary64_1202956.0
\[\leadsto \frac{1}{\sqrt{x} + \color{blue}{\sqrt{1} \cdot \sqrt{\frac{y}{500}}}} \cdot \frac{x \cdot x - \frac{y}{500} \cdot \frac{y}{500}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied *-un-lft-identity_binary64_1201356.0
\[\leadsto \frac{1}{\sqrt{\color{blue}{1 \cdot x}} + \sqrt{1} \cdot \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - \frac{y}{500} \cdot \frac{y}{500}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied sqrt-prod_binary64_1202956.0
\[\leadsto \frac{1}{\color{blue}{\sqrt{1} \cdot \sqrt{x}} + \sqrt{1} \cdot \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - \frac{y}{500} \cdot \frac{y}{500}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied distribute-lft-out_binary64_1196456.0
\[\leadsto \frac{1}{\color{blue}{\sqrt{1} \cdot \left(\sqrt{x} + \sqrt{\frac{y}{500}}\right)}} \cdot \frac{x \cdot x - \frac{y}{500} \cdot \frac{y}{500}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied *-un-lft-identity_binary64_1201356.0
\[\leadsto \frac{\color{blue}{1 \cdot 1}}{\sqrt{1} \cdot \left(\sqrt{x} + \sqrt{\frac{y}{500}}\right)} \cdot \frac{x \cdot x - \frac{y}{500} \cdot \frac{y}{500}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied times-frac_binary64_1201956.0
\[\leadsto \color{blue}{\left(\frac{1}{\sqrt{1}} \cdot \frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}}\right)} \cdot \frac{x \cdot x - \frac{y}{500} \cdot \frac{y}{500}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\]
Applied associate-*l*_binary64_1195456.0
\[\leadsto \color{blue}{\frac{1}{\sqrt{1}} \cdot \left(\frac{1}{\sqrt{x} + \sqrt{\frac{y}{500}}} \cdot \frac{x \cdot x - \frac{y}{500} \cdot \frac{y}{500}}{\sqrt{x} - \sqrt{\frac{y}{500}}}\right)}\]
Simplified0.0
\[\leadsto \frac{1}{\sqrt{1}} \cdot \color{blue}{\left(x + \frac{y}{500}\right)}\]
Simplified0.0
\[\leadsto \color{blue}{x + \frac{y}{500}}\]
Final simplification0.0
\[\leadsto x + \frac{y}{500}\]