### PARALLEL-PUSHING-OF-SUBGOALS-FOR-INDUCTION

consequences of how parallelized proofs of subgoals are pushed for induction
Major Section: PARALLEL-PROOF

This documentation topic relates to the experimental extension of ACL2
supporting parallel execution and proof; see parallelism.

The following discussion, concerning the naming of subgoals pushed for proof
by induction and the timeliness of aborting when two or more goals are pushed
for proof by induction, only applies when waterfall parallelism is enabled
(see set-waterfall-parallelism).

When two sibling subgoals (e.g. 4.5 and 4.6) both push goals to be proved by
induction (e.g., 4.6 pushes *1 and 4.5 pushes *2), a name is assigned to the
second pushed subgoal (e.g., *2) as if the first push hasn't happened (e.g.,
*2 is mistakenly called *1). In such a case, we say what the name _could_
be. The following non-theorem illustrates how this works.

(set-waterfall-parallelism :full)
(thm (equal (append (car (cons x x)) y z) (append x x y)))

There is another consequence of the way the parallelized waterfall pushes
subgoals for proof by induction. Without waterfall parallelism enabled, ACL2
sometimes decides to abort instead of pushing a goal for later proof by
induction, preferring instead to induct on the original conjecture. But with
waterfall parallelism enabled, the prover no longer necessarily immediately
aborts to prove the original conjecture. Suppose for example that sibling
subgoals, Subgoal 4.6 and Subgoal 4.5, each push a subgoal for induction. If
the waterfall is performing the proof of each of these subgoals in parallel,
the proof will no longer abort immediately after the second push occurs, that
is at Subgoal 4.5. As a result, the prover will continue through Subgoal
4.4, Subgoal 4.3, and beyond. It is not until the results of combining the
proof results of Subgoal 4.6 with the results from the remaining sibling
subgoals (4.5, 4.4, and so on), that the proof attempt will abort and revert
to prove the original conjecture by induction. This example illustrates
behavior that is rather like the case that `:`

`otf-flg`

is `t`

, in
the sense that the abort does not happen immediately, but also rather like
the case that `:`

`otf-flg`

is `nil`

, in the sense that the abort does
occur before getting to Subgoal 3.