\begin{definition}[Definition:Exchange Operation]
The '''exchange operation''' on two variables $a$ and $b$ is denoted:
:$a \leftrightarrow b$
and is interpreted as:
:the value of variable $a$ is to be replaced by the current value of variable $b$
and at the same time:
:the value of variable $b$ is to be replaced by the current value of variable $a$.
\end{definition}