Let \( I \) be an index set, and \( S \) a set then we say that a function \( t : I \to S \) is a tuple,

Suppose \( t: I \to S \) is a tuple such that \( I = \emptyset \) then \( t \) is said to be the empty tuple and is notated by \( \left( \right) \).

Suppose that \( t \) is a tuple and \( i \in \operatorname{ dom } \left( t \right) \) , then we define that the tuple's value at index \( i \) as \( t \left( i \right) \)

Suppose that \( t \) is a tuple, then we define \( t _ i \) to be \( t \) at index \( i \)

Suppose that the index set has some natural ordering, then the notation \( \left( t _ { i _ 1 } , t _ { i _ 2 } , \ldots \right) \)

A finite tuple is a tuple with a finite index set

A integer indexed tuple is a tuple whose index set equals \( \left\{ a, \ldots , b \right\} \) for some \( a, b \in \mathbb{ Z } \) or is some \( I \subseteq \mathbb{ Z } \)

We define two \( n \) tuples \( (x_1, x_2, ..., x_n) \) and \( (y_1, y_1, ..., y_n) \) to be equal when \[ \forall i \in [1 \ldots n], x_i = y_i \]

Suppose that \( a = \left( a _ 1, a _ 2, \ldots , a _ n \right) \) then \( \operatorname{ len } \left( a \right) = n \)

A zero indexed tuple is a tuple of the form \( a = \left( a _ 0, a _ 1, \ldots a _ m \right) \)

Suppose that \(a = \left( a _ 1, a _ 2, \ldots , a _ n \right) \), is an \( n \) tuple, then we define \[ \operatorname{rev} \left( a \right) := \left( a _ n, \ldots , a _ 1 \right) \]

Suppose that \( a = \left( a _ 1, \ldots , a _ n \right) \) and \( b = \left( b _ 1, \ldots , b _ m \right) \) are finite tuples, then \[ \operatorname{ concat } \left( a, b \right) = \left( a _ 1, \ldots a _ n, b _ 1, \ldots , b _ m \right) \]

Suppose that \(a = \left( a _ 1, a _ 2, \ldots , a _ n \right) \in \mathbb{ R } ^ n \), then we say that \( a \) is sorted in ascending order when for any \( i \in [ 1 \ldots n - 1 ] \) \( a _ i \le a _ { i + 1 } \)

Suppose that \(a = \left( a _ 1, a _ 2, \ldots , a _ n \right) \in \mathbb{ R } ^ n \), then we say that \( a \) is sorted in strictly ascending order when \[ \operatorname{ bop\_holds } \left( \lt , a \right) \]

Suppose that \( \star \) is a binary operation, then we say that it holds consecutively on a tuple \( a = \left( a _ 1, \ldots, a _ n \right) \) whenever we have \[ a _ i \star a _ { i + 1 } \] for each \( i \in \left[ 1, \ldots , n - 1 \right] \), we also define the predicate \( \operatorname{ bop\_holds } \) as follows: \[ \operatorname{ bop\_holds } \left( \star, a \right) = T \] iff the above property holds true.

Suppose that \( a \in \mathbb{ R } ^ n \) then define the \( \operatorname{ sorted\_asc } : \mathbb{ R } ^ n \to \left\{ T, F \right\} \) such that \[ \operatorname{ sorted\_asc } \left( a \right) = \operatorname{ bop\_holds } \left( \le , a \right) \]

Suppose that \( a \in \mathbb{ R } ^ n \) then we define \[ \operatorname{ strict\_asc\_sorted } \left( a \right) = \operatorname{ bop\_holds } \left( \lt , a \right) \]

Suppose that \( a = \left( a _ 1, \ldots , a _ n \right) \) is a tuple, then we define the function \[ \operatorname{ set } \left( a \right) = \left\{ a _ i: i \in \left[ 1, \ldots , n \right] \right\} \]

Suppose that \( a \in \mathbb{ R } ^ n \) then we define the function \( \operatorname{ strict\_asc\_sort } : \mathbb{ R } ^ n \to \mathbb{ R } ^ n \) such that if \( s = \operatorname{ strict\_asc\_sort } \left( a \right) \) then we have \[ \operatorname{ strict\_asc\_sorted } \left( s \right) = T \] such that \( \left\lvert a \right\rvert = \left\lvert s \right\rvert \) and \( \operatorname{ set } \left( a \right) = \operatorname{ set } \left( s \right) \)

Suppose that \( a, b \in \mathbb{ R } ^ n \) then \[ a \cap b \] is defined as the tuple \( s \) such that \[ s = \operatorname{ strict\_asc\_sort } \left( \operatorname{ concat } \left( a, b \right) \right) \] using the sorting function and concatenation

Suppose that \(a = \left( a _ 1, a _ 2, \ldots , a _ n \right) \in \mathbb{ R } ^ n \), then we say that \( a \) is sorted in descending order when for any \( i \in [ 1 \ldots n - 1 ] \) \( a _ i \ge a _ { i + 1 } \)

Suppose that \( \left( a _ 1, a _ 2, \ldots , a _ n \right) \in \mathbb{ R } ^ n \), then an inversion is a tuple \( i , j \in [ 1 \ldots n ] \times [ 1 \ldots n ] \) such that \( i \lt j \) but \( a _ i \gt a _ j \)