ADT Queue [ X ] INITIALS emptyQueue : -> Queue CONSTRUCTORS insQueue : X * Queue -> Queue SELECTORS remQueue : Queue(i) -> Queue infoQueue : Queue(i) -> X isEmptyQueue : Queue(i) -> BOOL copyQueue : Queue(i) -> Queue EQ_Queue (c): Queue(i) * Queue(i) -> BOOL AXIOMS remQueue(emptyQueue) = ERROR remQueue(insQueue(X1,Q2)) = if isEmptyQueue(Q2) then emptyQueue else insQueue(X1,remQueue(Q2)) fi infoQueue(emptyQueue) = ERROR infoQueue(insQueue(X1,Q2)) = if isEmptyQueue(Q2) then X1 else infoQueue(Q2) fi isEmptyQueue(emptyQueue) = TRUE isEmptyQueue(insQueue(X1,Q2)) = FALSE copyQueue(emptyQueue) = emptyQueue copyQueue(insQueue(X1,Q2)) = insQueue(X1,Q2) EQ_Queue(emptyQueue,emptyQueue) = TRUE EQ_Queue(emptyQueue,insQueue(X1,Q2)) = FALSE EQ_Queue(insQueue(X1,Q2),emptyQueue) = FALSE EQ_Queue(insQueue(X1,Q2),insQueue(X3,Q4)) = AND(EQUAL(X1,X3),EQ_Queue(Q2,Q4))