Problem 11c is still part of problem 11 and refers still to the structure defined at the beginning of problem 11. Thus, the transition relation is a∧((b∧c)↔¬b′)∧(c′↔(¬b∧¬c)) and the initial states are b↔c.
The reachable states are those states that are either (1) initial states or (2) reachable with a transition from a reachable state. That can be expressed as a fixpoint which is mu y. (Init ⋁ <:>y) and hence, we perform a fixpoint iteration: Actually, we should start with y0 = \{\}, but that leads then to y1 := Init, so that we started in the solution of 11c directly with Phi_0 := Init. After this, we continue by computing y{i+1} := (Init ⋁ <:>y{i}) which simply means we are adding successor states until we find a fixpoint.
