Added a theory of intervals and a test case: a specification for a lock-free deque