Tuple
Let be an index set, and a set then we say that a function is a tuple,
Empty Tuple
Suppose is a tuple such that then is said to be the empty tuple and is notated by .
Tuple at an Index
Suppose that is a tuple and , then we define that the tuple's value at index as
Tuple Subscript Notation
Suppose that is a tuple, then we define to be at index
Ordered Tuple Notation
Suppose that the index set has some natural ordering, then the notation
Finite Tuple
A finite tuple is a tuple with a finite index set
Integer Indexed Tuple
A integer indexed tuple is a tuple whose index set equals for some or is some
Note that a integer indexed tuple is represented using ordered tuple notation using . When it's finite we get
When an Integer Indexed Tuple is Empty
Suppose that then
By definition we can see that it's index set is which is equal to and therefore it is the empty tuple.
Finite Tuple Equality
We define two tuples and to be equal when
Note that finite tuples tuples are indexed starting from 1
Length
Suppose that then
Zero Indexed Tuple
A zero indexed tuple is a tuple of the form
Length of a Zero Indexed Tuple
Suppose that is a zero indexed tuple, then
Converting from Regular to Zero Indexing
Let be a finite tuple and suppose , let be but indexed regularly, and let be but using zero indexing, then for all
Reverse of a Finite Tuple
Suppose that , is an tuple, then we define
Reverse Cancels
For any tuple
Concatenation
Suppose that and are finite tuples, then
Sorted in Ascending Order
Suppose that , then we say that is sorted in ascending order when for any
Sorted in Strictly Ascending Order
Suppose that , then we say that is sorted in strictly ascending order when
A Binary Relation Holds Consecutively on a Tuple
Suppose that is a binary operation, then we say that it holds consecutively on a tuple whenever we have for each , we also define the predicate as follows: iff the above property holds true.
Sorted Tuple Predicate
Suppose that then define the such that
sorted_asc Holds iff It is Sorted in Ascending Order
iff is sorted in ascending order
Sorted in Strictly Ascending order Predicate
Suppose that then we define
Set of a Tuple
Suppose that is a tuple, then we define the function
Strictly Ascending Sorting Function
Suppose that then we define the function such that if then we have such that and
Intersection of Two Sorted Tuples
Suppose that then is defined as the tuple such that using the sorting function and concatenation
Ascending Tuple
Show that is an ascending tuple
Sorted in Descending Order
Suppose that , then we say that is sorted in descending order when for any
Descending Tuple
Show that is a descending tuple
The reverse of Ascending is Descending
Suppose that is a finite tuple sorted in ascending order, then is sorted in descending order.
Inversion
Suppose that , then an inversion is a tuple such that but
Given the tuple then we can see that is an inversion because but