elements, that is . The tail of the queue is then almost and inserting an element x to is almost . It is said almost, because in both of those results, . An auxiliary function must then be called for the invariant to be satisfied. Two cases must be considered, depending on whether is the empty list, in which case , or not. The formal definition is and where is f followed by r reversed. Let us call the function which returns f followed by r reversed. Let us furthermore assume that , since it is the case when this function is called. More precisely, we define a lazy function which takes as input three list such that , and return the concatenation of f, of r reversed and of a. Then . The inductive definition of rotate is and . Its running time is , but, since lazy evaluation is used, the computation is delayed until the results is forced by the computation. The list s in the data structure has two purposes. This list serves as a counter for , indeed, if and only if s is the empty list. This counter allows us to ensure that the rear is never longer than the front list. Furthermore, using s, which is a tail of f, forces the computation of a part of the (lazy) list f during each tail and insert operation. Therefore, when , the list f is totally forced. If it was not the case, the internal representation of f could be some append of append of... of append, and forcing would not be a constant time operation anymore. See also Circular buffer Double-ended queue (deque) Priority queue Queuing theory Stack (abstract data type) – the "opposite" of a queue: LIFO (Last In First Out) References General references Further reading Donald Knuth. The Art of Computer Programming, Volume 1: Fundamental Algorithms, Third Edition. Addison-Wesley, 1997. . Section 2.2.1: Stacks, Queues, and Dequeues, pp. 238–243. Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction to Algorithms, Second Edition. MIT Press and McGraw-Hill, 2001. . Section 10.1: Stacks and queues, pp. 200–204. William Ford, William Topp. Data Structures with C++ and STL, Second Edition. Prentice Hall, 2002. . Chapter 8: Queues and Priority Queues, pp. 386–390. Adam Drozdek. Data Structures and Algorithms in C++, Third Edition. Thomson Course Technology, 2005. . Chapter 4: Stacks