= Solution
\b[Yes: the procedure always terminates after finitely many steps.] If an iteration does not return, then $X_{i+1}\subsetneq X_i$. Thus at least one <state> is permanently removed. A finite <set> of $|S|$ <states> can suffer at most $|S|$ such strict decreases, after which the next equality test must return. Therefore the procedure makes at most
$$
\boxed{|S|+1\text{ evaluations of }H}
$$
when started from $X_0=S$, counting the final evaluation that detects equality. The bound also covers $S=\varnothing$, where the first evaluation already returns. Each evaluation inspects finitely many <states> and successors, so every individual step terminates as well. Finiteness, rather than monotonicity alone, supplies this finite termination bound.
Back to article page
