Tuple
Let I be an index set, and S a set then we say that a function t : I → S is a tuple,
Empty Tuple
Suppose t : I → S is a tuple such that I = ∅ then t is said to be the empty tuple and is notated by ( ) .
Tuple at an Index
Suppose that t is a tuple and i ∈ dom ⁡ ( t ) , then we define that the tuple's value at index i as t ( i )
Tuple Subscript Notation
Suppose that t is a tuple, then we define t i to be t at index i
Ordered Tuple Notation
Suppose that the index set has some natural ordering, then the notation ( t i 1 , t i 2 , … )
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 { a , … , b } for some a , b ∈ Z or is some I ⊆ Z

Note that a integer indexed tuple is represented using ordered tuple notation using ( a 1 , a 2 , … ) . When it's finite we get ( a − 2 , a − 1 , a 0 , a 1 , a 2 , a 3 , a 4 )

When an Integer Indexed Tuple is Empty
Suppose that i > j ∈ Z then ( a i , … , a j ) = ( )
By definition we can see that it's index set is { i , … , j } which is equal to ∅ and therefore it is the empty tuple.
Finite Tuple Equality
We define two n tuples ( x 1 , x 2 , . . . , x n ) and ( y 1 , y 1 , . . . , y n ) to be equal when ∀ i ∈ [ 1 … n ] , x i = y i

Note that finite tuples tuples are indexed starting from 1

Length
Suppose that a = ( a 1 , a 2 , … , a n ) then len ⁡ ( a ) = n
Zero Indexed Tuple
A zero indexed tuple is a tuple of the form a = ( a 0 , a 1 , … a m )
Length of a Zero Indexed Tuple
Suppose that a = ( a 0 , a 1 , … a m ) is a zero indexed tuple, then len ⁡ ( a ) = m + 1
Converting from Regular to Zero Indexing
Let a be a finite tuple and suppose len ⁡ ( a ) = n , let r be a but indexed regularly, and let z be a but using zero indexing, then for all i ∈ [ 1 . . . n ] , r i = z i − 1
Reverse of a Finite Tuple
Suppose that a = ( a 1 , a 2 , … , a n ) , is an n tuple, then we define rev ⁡ ( a ) := ( a n , … , a 1 )
Reverse Cancels
For any n tuple a rev ⁡ ( rev ⁡ ( a ) ) = a
Concatenation
Suppose that a = ( a 1 , … , a n ) and b = ( b 1 , … , b m ) are finite tuples, then concat ⁡ ( a , b ) = ( a 1 , … a n , b 1 , … , b m )
Sorted in Ascending Order
Suppose that a = ( a 1 , a 2 , … , a n ) ∈ R n , then we say that a is sorted in ascending order when for any i ∈ [ 1 … n − 1 ] a i ≤ a i + 1
Sorted in Strictly Ascending Order
Suppose that a = ( a 1 , a 2 , … , a n ) ∈ R n , then we say that a is sorted in strictly ascending order when b o p _ h o l d s ⁡ ( < , a )
A Binary Relation Holds Consecutively on a Tuple
Suppose that ⋆ is a binary operation, then we say that it holds consecutively on a tuple a = ( a 1 , … , a n ) whenever we have a i ⋆ a i + 1 for each i ∈ [ 1 , … , n − 1 ] , we also define the predicate b o p _ h o l d s as follows: b o p _ h o l d s ⁡ ( ⋆ , a ) = T iff the above property holds true.
Sorted Tuple Predicate
Suppose that a ∈ R n then define the s o r t e d _ a s c : R n → { T , F } such that s o r t e d _ a s c ⁡ ( a ) = b o p _ h o l d s ⁡ ( ≤ , a )
sorted_asc Holds iff It is Sorted in Ascending Order
s o r t e d _ a s c ⁡ ( a ) = T iff a is sorted in ascending order
Sorted in Strictly Ascending order Predicate
Suppose that a ∈ R n then we define s t r i c t _ a s c _ s o r t e d ⁡ ( a ) = b o p _ h o l d s ⁡ ( < , a )
Set of a Tuple
Suppose that a = ( a 1 , … , a n ) is a tuple, then we define the function set ⁡ ( a ) = { a i : i ∈ [ 1 , … , n ] }
Strictly Ascending Sorting Function
Suppose that a ∈ R n then we define the function s t r i c t _ a s c _ s o r t : R n → R n such that if s = s t r i c t _ a s c _ s o r t ⁡ ( a ) then we have s t r i c t _ a s c _ s o r t e d ⁡ ( s ) = T such that | a | = | s | and set ⁡ ( a ) = set ⁡ ( s )
Intersection of Two Sorted Tuples
Suppose that a , b ∈ R n then a ∩ b is defined as the tuple s such that s = s t r i c t _ a s c _ s o r t ⁡ ( concat ⁡ ( a , b ) ) using the sorting function and concatenation
Ascending Tuple
Show that ( 1 , 2 , 3 , 4 , 100 ) is an ascending n tuple
Sorted in Descending Order
Suppose that a = ( a 1 , a 2 , … , a n ) ∈ R n , then we say that a is sorted in descending order when for any i ∈ [ 1 … n − 1 ] a i ≥ a i + 1
Descending Tuple
Show that ( 8 , 5 , 3 , 1 , 0 ) is a descending n tuple
The reverse of Ascending is Descending
Suppose that a is a finite tuple sorted in ascending order, then rev ⁡ ( a ) is sorted in descending order.
Inversion
Suppose that ( a 1 , a 2 , … , a n ) ∈ R n , then an inversion is a tuple i , j ∈ [ 1 … n ] × [ 1 … n ] such that i < j but a i > a j

Given the tuple a := ( 8 , 9 , 10 , 11 , 3 ) then we can see that ( 1 , 5 ) is an inversion because 1 < 5 but 8 > 3