equal
deleted
inserted
replaced
718 \noindent |
718 \noindent |
719 Homeier calls these proof obligations \emph{respectfulness |
719 Homeier calls these proof obligations \emph{respectfulness |
720 theorems}. However, unlike his quotient package, we might have several |
720 theorems}. However, unlike his quotient package, we might have several |
721 respectfulness theorems for one constant---he has at most one. |
721 respectfulness theorems for one constant---he has at most one. |
722 The reason is that because of our quotient compositions, the types |
722 The reason is that because of our quotient compositions, the types |
723 @{text \<sigma>} and @{text \<tau>} are not completely determined by the type of @{text "c\<^bsub>r\<^esub>"}. |
723 @{text \<sigma>} and @{text \<tau>} are not completely determined by @{text "c\<^bsub>r\<^esub>"}. |
724 And for every instantiation of the types, we might end up with a |
724 And for every instantiation of the types, a corresponding |
725 corresponding respectfulness theorem. |
725 respectfulness theorem is necessary. |
726 |
726 |
727 Before lifting a theorem, we require the user to discharge |
727 Before lifting a theorem, we require the user to discharge |
728 respectfulness proof obligations. In case of @{text bn} |
728 respectfulness proof obligations. In case of @{text bn} |
729 this obligation is as follows |
729 this obligation is as follows |
730 |
730 |