##
Finite Sequence Additon

This operation adds up an ordered sequence of numbers (<+> x) where x is a
tuple of length N. Each tuple has a length
and each number in the sequence can be extracted using the index
operation. It is defined here. The reason to
introduce this notation is that since we can use any tuple, this allows us to reason
abstractly about a sum of an arbitrary finite sequence of numbers.

Tuple Overview