equal
deleted
inserted
replaced
131 variables {\em(except the induction variable itself!)}.} |
131 variables {\em(except the induction variable itself!)}.} |
132 \end{quote} |
132 \end{quote} |
133 This prevents trivial failures like the one above and does not affect the |
133 This prevents trivial failures like the one above and does not affect the |
134 validity of the goal. However, this heuristic should not be applied blindly. |
134 validity of the goal. However, this heuristic should not be applied blindly. |
135 It is not always required, and the additional quantifiers can complicate |
135 It is not always required, and the additional quantifiers can complicate |
136 matters in some cases, The variables that should be quantified are typically |
136 matters in some cases. The variables that should be quantified are typically |
137 those that change in recursive calls. |
137 those that change in recursive calls. |
138 |
138 |
139 A final point worth mentioning is the orientation of the equation we just |
139 A final point worth mentioning is the orientation of the equation we just |
140 proved: the more complex notion (\isa{itrev}) is on the left-hand |
140 proved: the more complex notion (\isa{itrev}) is on the left-hand |
141 side, the simpler one (\isa{rev}) on the right-hand side. This constitutes |
141 side, the simpler one (\isa{rev}) on the right-hand side. This constitutes |