How to constrain a dynamic array with the incremental pattern for each elements

In reply to zhangjintmru:

The sort() method is defined in section 7.12.2 Array ordering methods of the LRM. You can get a copy here.

Although your implementation works, it has unnecessary constraints. If you have ts[0] < ts[1] AND ts[1] < ts[2], then it follows that ts[0] < ts[2]