762 permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"} |
762 permutation. However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"} |
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 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}. |
769 |
769 |
770 In the rest of this section we are going to show that the alpha-equivalences |
770 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 |
771 really lead to abstractions where some atoms are bound (or more precisely |
772 removed from the support). For this we will consider three abstraction |
772 removed from the support). For this we will consider three abstraction |