equal
deleted
inserted
replaced
571 in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last |
571 in the support of @{text x} (that is @{term "supp x \<sharp>* p"}). The last |
572 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders |
572 fact and Property~\ref{supppermeq} allow us to ``rename'' just the binders |
573 in @{text x}, because @{term "p \<bullet> x = x"}. |
573 in @{text x}, because @{term "p \<bullet> x = x"}. |
574 |
574 |
575 All properties given in this section are formalised in Isabelle/HOL and also |
575 All properties given in this section are formalised in Isabelle/HOL and also |
576 most of them are described with proofs in \cite{HuffmanUrban10}. In the next section |
576 most of them are described with proofs in \cite{HuffmanUrban10}. In the next |
577 we make extensively use of the properties of @{text "supp"} and permutations |
577 sections we will make extensively use of these properties for characterising |
578 for characterising alpha-equivalence in the presence of multiple binders. |
578 alpha-equivalence in the presence of multiple binders. |
579 |
|
580 *} |
579 *} |
581 |
580 |
582 |
581 |
583 section {* General Binders\label{sec:binders} *} |
582 section {* General Binders\label{sec:binders} *} |
584 |
583 |