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

Let $X$ be any fixed point of $H$. Thenso $X\subseteq A$ and every successor of every member of $X$ belongs to $X$. Take $s_0\in X$ and an arbitrary infinite path in a transition system $s_0{s}_1{s}_2\cdots$ from $s_0$. By mathematical induction, every $s_i$ belongs to $X$: the base case is the choice of $s_0$, and $s_i\in X$ implies $s_{i+1}\in \mathrm{Post}(s_i)\subseteq X$.

Since $X\subseteq A$, the whole path in a transition system stays in $A$. The path in a transition system was arbitrary, so $s_0\models \forall \square \Phi$. Thus $s_0\in G_{\Phi }$, and since $s_0$ was arbitrary in $X$,Part (b) proves that $G_{\Phi }$ itself is a fixed point. Thereforethe greatest fixed point with respect to set inclusion. In fact the same induction works for every $X\subseteq H(X)$, showing why a successor-closed set of good states certifies this universal property.