Every value in array segment
b[1..n]
that is not inb[i..j]
is inb[i..j]
.
Let predicate p(v)
be "v
is in b[i..j]
."
(A k: 0<k<=N: ~p(b[k]) -> p(b[k]))
=
(A k: 0<k<=N: ~~p(b[k]) | p(b[k]))
=
(A k: 0<k<=N: p(b[k]) | p(b[k]))
=
(A k: 0<k<=N: p(b[k]))
Every value in array segment b[1..n]
that is in b[i..j]
.