AlphaConvert - Maple Help

QuantifierElimination[QuantifierTools]

 AlphaConvert
 alpha conversion of a Tarski formula, removing conflicts between bound variables

 Calling Sequence AlphaConvert( expr )

Parameters

 expr - Tarski formula, usually quantified

Returns

 • 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.

Examples

 > $\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]{,}{x}{}{y}{=}{0}\right){\wedge }{\exists }{}\left(\left[\mathrm{x__1}{,}{z}\right]{,}\mathrm{x__1}{}{z}{=}{0}\right)$ (1)

Compatibility

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