CONSTANT N = 4

SPECIFICATION Spec

INVARIANT TypeOK
PROPERTY EventuallyTerminal