In MathCheck, comparisons can be chained. For instance, `1 ≤ i < j ≤ n` means the same as `1 ≤ i ^^ i < j ^^ j ≤ n`. (In some situations, MathCheck does not allow misleading chains such as `0 ≤ x ≠ y ≤ 1`, which might seem to promise that `x ≤ 1` although it does not. On this course, MathCheck allows you to write such chains.)
Please write predicates that express the given claims on the array `K[0`…`M]`. In these questions, “(exists and)” reminds you to include in the answers the requirement that the array is sufficiently big. From then on, it is your responsibility to remember to add such a requirement (unless the question makes it clear that it is not needed).