Strong planning winning-set iteration ($W_{t+1}=W_t\cup {\mathrm{Pre}}_{\forall }(W_t)$)

For a finite nondeterministic planning problem with goal set $G$, initialize $W_0=G$ and putA state in $W_t$ has a strong plan reaching $G$ within $t$ steps. The proof is mathematical induction: an action witnessing admission to $W_{t+1}$ has only successors with plans of depth at most $t$. Conversely, the first action of any guaranteed plan of depth $t+1$ has every successor in $W_t$, again by mathematical induction. Since $W_t$ only grows inside a finite state space, the iteration stabilizes after at most the number of states many strict expansions. Recording a witnessing action at first admission gives a policy whose rank decreases at every nonterminal step.