Enhancement 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 IsNondecreasing(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 IsPreceding(alpha:Str(Entry), beta:Str(Entry)): B=(for all x,y: Entry,
            if <x> is_substring_of alpha and <y> is_substring_of beta then LEQV(x,y));

    Operation Sort_Q(updates Q: Queue);
        ensures IsNonDecreasing(Q) and IsPermutation(#Q,Q);
end Sort_Capability;