Ch3, Ex14

a) It works because of the dataflow behavior. If you delete one element from an empty queue. Returned queue is q(~1 _ _|_) and returned element is unbound. As soon as we do one insert, these entities are bound.

b)For empty queues it returns the right results. But for non empty queues it blocks as its trying to compare something like 1|2|E == E where E is unbound. The entailment blocks because the answer depends upon the binding of E. If E is bound to anything except 1|2|E then the answer is false. But it can not decide before that binding happens.