Correctness and exact termination conditions for all-size planning search

Suppose $S\mathrm{\ne }\mathrm{\varnothing }$. By [F3] let $n_{\ast }=\min S$. In ascending mode [F2] calls the evaluator at $1,\dots ,n_{\ast }$: each call terminates, every earlier answer is false by leastness, and the answer at $n_{\ast }$ is true. The finite sequence of calls therefore terminates at $n_{\ast }$, with exactly $n_{\ast }$ evaluations and the output required by [F1].

In bounded mode at most $B$ calls occur and every call terminates, so the mode terminates, including when $B=0$. If an index is returned, every smaller positive integer has already answered false, and exactness makes the returned integer the least of $S$, not merely least in a selected list.

If ascending mode terminates, [F2] says it returns only at a true answer, so its returned integer is in $S$ and $S$ is nonempty. Conversely, if $S$ is empty, every terminating call answers false and [F2] increments to the next positive integer. No return instruction is reached, so the execution continues forever. Together with step 1.1 this proves the equivalence and the empty-case behavior.

If bounded mode returns none, every index at most $B$ is infeasible. Were $S$ nonempty, the completeness certificate would place some element of $S$ at most $B$, contradicting those answers. Thus $S$ is empty and none is the answer of [F1]. Conversely, empty $S$ makes every bounded answer false, so none is returned.

In the infeasibility mode the supplied proof states that $S$ is empty, so immediate return of none is correct by [F1]. A true answer at a positive $B$ proves that $B\in S$ and therefore is itself a finite completeness witness, whether or not feasibility is monotone. The constant-false evaluator is nondecreasing but has empty $S$, so step 2.1 shows that monotonicity alone does not give termination of ascending search. These observations establish all remaining assertions.