Past exam of the computer science course of the University of Oxford / 2015 / Computer aided formal verification / 3 / f / Solution

Yes: the procedure always terminates after finitely many steps. If an iteration does not return, then $X_{i+1}⊊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 mostwhen 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.