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

Login to edit