Enhancement Isabelle_Sort_Capability(definition LEQV(x,y: Entry): B)
            for Queue_Template;
      requires(for all x,y,z: Entry, if LEQV(x,y) and LEQV(y,z)then
          LEQV(x,z)) and (for all x,y:Entry, LEQV(x,y) or LEQV(y,x));

    Definition IsNondecerasing(a: Str(Entry)): B=(for all b,c: Str(Entry),
      for all x,y: Entry,
            if a = b o <x> o <y> o c then LEQV(x,y));

    Definition IsASmallest(Q:Str(Entry), min:Entry): B=(for all x:Entry, 
			if (there exists y,z:Str(Entry), Q = y o <x> o z) then LEQV(min, x));

    Operation Sort_Q(updates Q: Queue);
        ensures IsNondecerasing(Q) and IsPermutation(#Q,Q);
end Isabelle_Sort_Capability;