INVARIANT XHasNotWon SPECIFICATION Spec