Suppose we have the predicate$\qquad A.p.q  (i \mid pij<q : X.iX.j)$which says that $X[p..q)$ is ascending.Apparently, the predicate holds for empty segments, is prefix closed and is postfix closed.I would like to prove that the predicate above is indeed prefix closed, but I am not able to; that is, I am unable to prove that$\qquad A.p.q \implies (s \mid psq : A.p.s)$and I wondered if somebody could help?
How to prove that a predicate is prefix closed
logic;proof techniques;first order logic
Your predicate states that $X_p \leq X_{p+1} \leq \cdots \leq X_{q-1}$. If you take any subinterval of $[p,q)$, say $[p',q')$, you will still have $X_{p'} \leq X_{p'+1} \leq \cdots \leq X_{q'}$. In other words, a subinterval of a non-decreasing sequence is also non-decreasing.Now that you know why what you want to prove is true, it remains to prove it formally. Always remember: the first step is to understand why something is true, and only then should you try to prove it. In fact, most of the time in mathematics and computer science we skip the second step, that of proving things formally, since it obscures the situation.