spec Queue =
  sorts Elem; Queue
  ops first: Queue ->? Elem;
      deq: Queue ->? Queue;
      enq: Elem * Queue -> Queue;
      new: Queue
  pred empty: Queue
  vars x: Elem; q: Queue
  . empty(new)                       %(new_empty)%
  . not empty(enq(x,q))              %(enq_nempty)%
  . def first(q) => not empty(q)     %(empty_first_undef)%
  . def deq(q) => not empty(q)       %(empty_deq_undef)%
  . not empty(q) => deq(enq(x,q)) =e= enq(x,deq(q)) %(deq_enq_nempty)%
  . not empty(q) => first(enq(x,q)) =e= first(q) %(first_enq_nempty)%
  . empty(q) => deq(enq(x,q)) = q    %(deq_enq_empty)%
  . empty(q) => first(enq(x,q)) = x  %(first_enq_empty)%
then %implies
     vars x,y: Elem; q:Queue         
  . not empty(q) => def first(q)    %(first_empty_def)%
  . not empty(q) => def deq(q)      %(deq_empty_def)%
  . def deq(enq(x,q))               %(deq_enq_def)%
  . def first(enq(x,q))             %(first_enq_def)%
  . not def deq(new)                %(deq_new_undef)%
  . not def first(new)              %(first_new_undef)%
  . deq(deq(enq(x,enq(y,new))))=new %(short_queue_deq)%
  . first(deq(enq(x,enq(y,new))))=x %(short_queue_first)%