equal
deleted
inserted
replaced
1713 third \emph{only} holds because of our restriction |
1713 third \emph{only} holds because of our restriction |
1714 imposed on the form of the binding functions---namely \emph{not} returning |
1714 imposed on the form of the binding functions---namely \emph{not} returning |
1715 any bound atoms. In Ott, in contrast, the user may |
1715 any bound atoms. In Ott, in contrast, the user may |
1716 define @{text "bn"}$_{1..m}$ so that they return bound |
1716 define @{text "bn"}$_{1..m}$ so that they return bound |
1717 atoms and in this case the third implication is \emph{not} true. A |
1717 atoms and in this case the third implication is \emph{not} true. A |
1718 result is that the lifing of the corresponding binding functions in Ott to $\alpha$-equated |
1718 result is that the lifting of the corresponding binding functions in Ott to $\alpha$-equated |
1719 terms is impossible. |
1719 terms is impossible. |
1720 |
1720 |
1721 Having established respectfulness for the raw term-constructors, the |
1721 Having established respectfulness for the raw term-constructors, the |
1722 quotient package is able to automatically deduce \eqref{distinctalpha} from |
1722 quotient package is able to automatically deduce \eqref{distinctalpha} from |
1723 \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can |
1723 \eqref{distinctraw}. Having the facts \eqref{fnresp} at our disposal, we can |