use(queues).
use(queue_induction2,[p=del_min_complete,q='del_min_complete!']).
use(queue_induction2,[p=del_min_correct,q='del_min_correct!']).








% definition of defined queue terms

defined(empty).
defined(Q) == defined(insert(Q,E)).
%defined(Q) -> Q=empty, exists(Q1,exists(E,Q=insert(Q1,E) and defined(Q1))).



/*

 del_min is totally defined on defined, that is,
 non-empty insert/empty queue terms.

 The significance of this lemma is that queue induction
 can be restricted to defined terms.

*/

del_min_complete(Q) ==
   ( ~(Q=empty) and defined(Q) => defined(queue(del_min(Q)))).




/*

 Main correctness property of del_min

*/


del_min_correct(Q) == forall(E,forall(E1,
      (~(Q=empty) and elem(del_min(Q))=E and contains(Q,E1) => E=<E1))).