# 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