		Search-engine friendly clone of the ACL2 documentation.

Induction

Induction-depth-limit

The maximum number permitted of nested inductions

ACL2 may limit the number of levels of induction. Consider for example a subgoal with this goal-spec:

Subgoal *1.2.3.1.2.3.1.2.3/7'11'

This represents nine levels of induction. By default, that is the maximum permitted, since proofs rarely succeed with more than a few levels of induction. (Indeed, one is well served by relying on only one level of induction, avoiding nested inductions in favor of proving suitable rewrite rules. See the-method.) Thus, if ACL2 would otherwise attempt to push the subgoal indicated above for later proof by induction, the overall proof would fail because that would cause the maximum nesting depth of 9 to be exceeded.

To see the current limit:

(induction-depth-limit (w state))

This limit is always a natural number, with one exception: it can be nil, which means that there is no limit on the nesting depth of inductions.

Note that an explicit :induct hint (see hints) will cause an induction to occur, regardless of the induction-depth-limit. Of course, if we have already reached the induction-depth-limit at the point the :induct hint is applied, then any attempt to push a subgoal for induction will fail (unless it too has an associated :induct hint).

To change the limit, see set-induction-depth-limit.

Subtopics

Set-induction-depth-limit: Set the induction-depth-limit