MathCheck Array Claim Problem 14 / 15

The array `H` is indexed from `-1` to `l`. Write a predicate saying that `H` is otherwise in increasing order, but the entries in locations `i` and `j` (where `i < j`) are in wrong order. array_claim H[-1...l] f_nodes 40 -1 <= i < j <= l /\ H[i] > H[j] /\ AA k: AA h; -1 <= k < h <= l: i = k /\ j = h \/ H[k] <= H[h] <=>

end_of_answer next_URL https://math.tut.fi/mathcheck/array_claim15.html

or