763 $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no |
763 $\not\approx_{\,\textit{set}}$ @{text "({x, y}, x)"} since there is no |
764 permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal |
764 permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal |
765 (similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be |
765 (similarly for $\approx_{\,\textit{list}}$). It can also relatively easily be |
766 shown that all three notions of alpha-equivalence coincide, if we only |
766 shown that all three notions of alpha-equivalence coincide, if we only |
767 abstract a single atom. In this case they also agree with the alpha-equivalence |
767 abstract a single atom. In this case they also agree with the alpha-equivalence |
768 used in older versions of Nominal Isabelle \cite{Urban08}. |
768 used in older versions of Nominal Isabelle \cite{Urban08}.\footnote{We omit a |
|
769 proof of this fact since the details are hairy and not really important for the |
|
770 purpose of this paper.} |
769 |
771 |
770 In the rest of this section we are going to show that the alpha-equivalences |
772 In the rest of this section we are going to show that the alpha-equivalences |
771 really lead to abstractions where some atoms are bound (or more precisely |
773 really lead to abstractions where some atoms are bound (or more precisely |
772 removed from the support). For this we will consider three abstraction |
774 removed from the support). For this we will consider three abstraction |
773 types that are quotients of the relations |
775 types that are quotients of the relations |