The alpha conversion of expr - that is, any ambiguous conflicts of bound variables between distinct quantified expressions are removed.

The output has exactly the same structure as input. In particular, the output will only be prenex if the input was, as this command does not attempt prenex conversion.

$\mathrm{with}\left(\mathrm{QuantifierElimination}\right)\:$$\mathrm{with}\left(\mathrm{QuantifierTools}\right)\:$

$\mathrm{AlphaConvert}\left(\mathrm{And}\left(\mathrm{exists}\left(\left[x\,y\right]\,xy=0\right)\,\mathrm{exists}\left(\left[x\,z\right]\,xz=0\right)\right)\right)$

$\exists \left(\left[x\,y\right]\,xy=0\right)\wedge \exists \left(\left[\mathrm{x\_\_1}\,z\right]\,\mathrm{x\_\_1}z=0\right)$

The QuantifierElimination:-QuantifierTools:-AlphaConvert command was introduced in Maple 2023.

For more information on Maple 2023 changes, see Updates in Maple 2023.