In formal methods its common to have a special notation 0 -> N which is 0 .. N-1. That way, a sequence of length M+N consists of a sequence with indices 0 -> M

In formal methods its common to have a special notation 0 -> N which is 0 .. N-1. That way, a sequence of length M+N consists of a sequence with indices 0 -> M and a sequence with indices M -> M+N.