Double ended queue data abstraction and axioms
Like you say items can be added to a double ended queue on both sides, yet you have only a single AddQ operator. More substantial is the change to the axioms. An item added at the end can (after several operations) be retrieved from the front.