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