I would like to know how a JML expression of the form `\old(Expression[Id])` is evaluated, i.e. if I have the `\old(vector[value-1])` expression, does the `\old` also refer to "value" or just the to the value of the `vector[value-1]`. Thanks in advance!