use(queues).


% 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 restrictedprove to defined terms.

*/

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


del_min_complete_induction ==
    (  del_min_complete(empty)
              and
       forall(Q,del_min_complete(Q) => forall(E,del_min_complete(insert(Q,E))))).



/* queue induction
  
   qi(P) == P(empty) and forall(Q,P(Q) => forall(E,P(insert(Q,E)))

   we have to instantiate this manually for each P

   In a higher-order logic we would prove that queue induction
   is correct, that is,

            qi(P) => forall(Q,P(Q)),

   using del_min_complete.
/*

 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))).


del_min_correct_induction == 
    (  del_min_correct(empty)
              and 
       forall(Q,del_min_correct(Q) => forall(E,del_min_correct(insert(Q,E))))).