Prisoners

This module checks that the invariant CountInvariant of module Prisoners is actually an inductive invariant of specification Spec. More precisely, its conjunction with TypeOK is an inductive invariant of the next-state action Next, meaning that it satisfies

(TypeOK /\ CountInvariant) /\ Next => (TypeOK /\ CountInvariant)'

Because Init implies TypeOK, it's easy to see that this implies that TypeOK /\ CountInvariant is also an invariant of Spec.