I'm using the event-B prover to proove some proof obligations.
I have a relation representing a $table: table \in 1‥n \to \mathbb{N}$. I know that in a sorted table the following property is true:
$\forall i· i \in 1‥m−1 \implies table(i)\le table(i+1)$
I would like to prove that from this property we can conclude:
$\forall i,j· i \in 1‥m \land j \in 1‥m \land i\le j \implies table(i)\le table(j) $ But I don't know how to conclude this in sequent calculus. From my perspective this is something so evident. Some help would be very much appreciated.
As always induction is your friend.
First, $i < j$ means $\exists m > 0 \mid $i+m = j $.
Therefore, we want to show that $\forall j, a(j)\le a(j+1) \implies \forall m>0, a(j) \le a(j+m) $.
Base case: this is true for $m=1$.
Induction: Suppose this is true for $m$. Then we have $1 \le k \le m \implies a(j) \le a(j+k) $. But we also have $a(j+m) \le a(j+m+1) $. Since $a(j) \le a(j+m)$, this implies that $a(j) \le a(j+m+1)$. Therefore $a(j) \le a(j+k)$ is true for $k = m+1$, so that $1 \le k \le m+1 \implies a(j) \le a(j+k) $, which is what we wanted to prove.