(** {1 VerifyThis@fm2012 competition, Challenge 1: Longest Repeated Substring} {h The following is the original description of the verification task, reproduced verbatim. A reference implementation in Java (based on code by Robert Sedgewick and Kevin Wayne) was also given. The Why3 implementation below follows the Java implementation as faithfully as possible.
```Longest Common Prefix (LCP) - 45 minutes

-----------------

Longest Common Prefix (LCP) is an algorithm used for text querying. In
the following, we model text as an integer array. You may use other
representations (e.g., Java Strings), if your system supports them.

LCP can be implemented with the pseudocode given below. Formalize and
verify the following informal specification for LCP.

Input:  an integer array a, and two indices x and y into this array
Output: length of the longest common prefix of the subarrays of a
starting at x and y respectively.

Pseudocode:

int lcp(int[] a, int x, int y) {
int l = 0;
while (x+l<a.length && y+l<a.length && a[x+l]==a[y+l]) {
l++;
}
return l;
}

========

BACKGROUND
----------

Together with a suffix array, LCP can be used to solve interesting text
problems, such as finding the longest repeated substring (LRS) in a text.

A suffix array (for a given text) is an array of all suffixes of the
text. For the text [7,8,8,6], the suffix array is
[[7,8,8,6],
[8,8,6],
[8,6],
[6]]

Typically, the suffixes are not stored explicitly as above but
represented as pointers into the original text. The suffixes in a suffix
array  are sorted in lexicographical order. This way, occurrences of
repeated substrings in the original text are neighbors in the suffix
array.

For the above, example (assuming pointers are 0-based integers), the
sorted suffix array is:

[3,0,2,1]