Solution

ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/computer-aided-formal-verification/3/d/solution

Let be any fixed point of . Then
so and every successor of every member of belongs to . Take and an arbitrary infinite path in a transition system from . By mathematical induction, every belongs to : the base case is the choice of , and implies .
Since , the whole path in a transition system stays in . The path in a transition system was arbitrary, so . Thus , and since was arbitrary in ,
Part (b) proves that itself is a fixed point. Therefore
the greatest fixed point with respect to set inclusion. In fact the same induction works for every , showing why a successor-closed set of good states certifies this universal property.

New to topics? Read the docs here!