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:
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
Note that an explicit
To change the limit, see set-induction-depth-limit.