The program reads the list of words into arrays, the entries one after the other with the start and the length of every word. It then selects the distinct words in increasing order: in round $t$ it scans all words and keeps the smallest one above the word selected in round $t - 1$, comparing words lexicographically entry by entry. The indices of the selected words are recorded, and finally their number and their frames are written. With $m$ words of total length $N$, this takes $O(m² · N)$ steps, so cubic time in the length of the input. Every value the program produces is at most the length of the input plus its largest entry, so word-length exponent $1$ suffices.

The proof is carried out for the notion $Lax185574.Computing.Computes$, and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$.