lInput assertion:
la == a0
lOutput assertion:
la == a0, and
l(($i) a[i] == v) ¨ a[r] == v, and
l(("i) a[i] != v) ¨ r == -1
lwhere r represents the returned value
lFor simplicity, we assume that the quantifiers range over
the valid indices of the
array only.
l