Converse of renaming substitutions

Question

In the paper Theory Unification in Abstract Clause Graphs, Hans Jorgen Ohlbach states that, given the renaming substitution $\sigma$, the converse substitution $\sigma^{c}$ is defined as $x=\sigma(y) \leftrightarrow y=\sigma^{c}(x)$, for all variables $x$ in the set of variables $V$. Example: if $\sigma = \{x \mapsto x', y\mapsto y'\}$, then the converse $\sigma_{c} = \{x' \mapsto x, y'\mapsto y\}$. The author concludes that, if $\sigma$ is a renaming substitution, then $\sigma\sigma^{c} = \sigma$ and $\sigma^{c}\sigma = \sigma^{c}$. This conclusion is not clear to me, since, as far as I can tell, $\sigma\sigma^{c} = \sigma^{c}$ and $\sigma^{c}\sigma = \sigma$. For instance, using the same example above, considering $\sigma = \{x \mapsto x', y\mapsto y'\}$, then

$\sigma\sigma^{c} = $

$\{x \mapsto x', y\mapsto y'\}\{x' \mapsto x, y'\mapsto y\} = $

$\{x \mapsto x, y \mapsto y, x' \mapsto x, y'\mapsto y\} =$

$\{x' \mapsto x, y'\mapsto y\} =$

$\sigma^{c}$.

Could someone help me understand how the author concludes that $\sigma\sigma^{c} = \sigma$ and $\sigma^{c}\sigma = \sigma^{c}$?

Answer 1

Assume that we are speaking of "repeated substitution".

Then, with term $t(x,y)$ and the above substitutions we have:

$\sigma(t(x,y))=t(x',y')$ and thus: $\sigma^c[\sigma(t(x,y))]=\sigma^c[t(x',y')]=t(x,y)$.

But $\sigma^c(t(x,y))=t(x,y)$, because there are no $x',y'$ in $t$, and thus: $\sigma^c\sigma=\sigma^c$.

In the same way:

$\sigma^c(t(x,y))=t(x,y)$ and thus: $\sigma[\sigma^c(t(x,y))]=\sigma[t(x,y)]=t(x',y')$ which is $\sigma(t)$.

Thus: $\sigma\sigma^c=\sigma$