/*

specification of priority ques

*/

use(to).

% projections

queue(pair(Q,E))=Q.
elem(pair(Q,E))=E.

% delete

delete(empty,E)=empty.
delete(insert(Q,E),E)=Q.
delete(insert(Q,E1),E2)=insert(delete(Q,E2),E1), E1=E2.

% delete minimal element

del_min(insert(empty,E))=pair(empty,E).
E=<elem(del_min(Q)) -> 
 del_min(insert(Q,E))=pair(Q,E),Q=empty.
elem(del_min(Q))<E  -> 
 del_min(insert(Q,E))=pair(insert(queue(del_min(Q)),E),elem(del_min(Q))),Q=empty.

% membership in queues

contains(empty,E) -> [].
contains(insert(Q,E),E).
contains(insert(Q,E1),E2)==contains(Q,E2), E1=E2.

precedence([del_min,delete,contains,elem,queue,pair,empty,insert,inf,undef,=<,<]).