Finite Sequence Product

This operation takes the product of 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 product of an arbitrary finite sequence of numbers.

Theorems

Tuple Overview

Login to edit