For this question assume that Max_Length = 6;

Operation Mystery4(updates Q: Queue);
      requires:  |Q| > 0;
      ensures:   there exists E: Entry, α: Str(Entry) such             that #Q = <E> o α and Q = α o <E>;

test set 1:
      inputs:        Q = <2, 3, 4, 5, 6 >;
      outputs:      Q = <3, 4, 5, 6, 2 >;

test set 2:
      inputs:         Q = <17, 21, 11, 17 >;
      outputs:       Q = <21, 11, 17, 17 >;

test set 3:
      inputs:         Q = <17, 21, 11, 17 >;
      outputs:       Q = <17, 17, 21, 11>;

test set 4:
      inputs:         Q = Λ;
      outputs:       Q = Λ;