MathCheck Array Claim Problem 13 / 15

The array `P` is indexed from `0` and has `N+1` elements. Write a predicate saying that `P` is in increasing order up to location `k` (which must exist), and from then on in decreasing order. array_claim P[0...N] f_nodes 40 0 <= k <= N /\ (AA i; 0 <= i < k: P[i] <= P[i+1]) /\ AA i; k <= i < N: P[i] >= P[i+1] <=>

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

or