The specification for ticket lock is proven using the atomic
specification for the increment operation.