equal
deleted
inserted
replaced
113 variables {\em(except the induction variable itself!)}.} |
113 variables {\em(except the induction variable itself!)}.} |
114 \end{quote} |
114 \end{quote} |
115 This prevents trivial failures like the one above and does not affect the |
115 This prevents trivial failures like the one above and does not affect the |
116 validity of the goal. However, this heuristic should not be applied blindly. |
116 validity of the goal. However, this heuristic should not be applied blindly. |
117 It is not always required, and the additional quantifiers can complicate |
117 It is not always required, and the additional quantifiers can complicate |
118 matters in some cases, The variables that should be quantified are typically |
118 matters in some cases. The variables that should be quantified are typically |
119 those that change in recursive calls. |
119 those that change in recursive calls. |
120 |
120 |
121 A final point worth mentioning is the orientation of the equation we just |
121 A final point worth mentioning is the orientation of the equation we just |
122 proved: the more complex notion (@{term itrev}) is on the left-hand |
122 proved: the more complex notion (@{term itrev}) is on the left-hand |
123 side, the simpler one (@{term rev}) on the right-hand side. This constitutes |
123 side, the simpler one (@{term rev}) on the right-hand side. This constitutes |