ΘρϵηΠατπ

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 ti to be t at index i
Ordered Tuple Notation
Suppose that the index set has some natural ordering, then the notation (ti1,ti2,…)
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∈ℤ or is some I⊆ℤ

Note that a integer indexed tuple is represented using ordered tuple notation using (a1,a2,…). When it's finite we get (a−2,a−1,a0,a1,a2,a3,a4)

When an Integer Indexed Tuple is Empty
Suppose that i>j∈ℤ then (ai,…,aj)=()
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 (x1,x2,...,xn) and (y1,y1,...,yn) to be equal when ∀i∈[1…n],xi=yi

Note that finite tuples tuples are indexed starting from 1

Length
Suppose that a=(a1,a2,…,an) then len⁡(a)=n
Zero Indexed Tuple
A zero indexed tuple is a tuple of the form a=(a0,a1,…am)
Length of a Zero Indexed Tuple
Suppose that a=(a0,a1,…am) 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],ri=zi−1
Reverse of a Finite Tuple
Suppose that a=(a1,a2,…,an), is an n tuple, then we define rev⁡(a):=(an,…,a1)
Reverse Cancels
For any n tuple a rev⁡(rev⁡(a))=a
Concatenation
Suppose that a=(a1,…,an) and b=(b1,…,bm) are finite tuples, then concat⁡(a,b)=(a1,…an,b1,…,bm)
Sorted in Ascending Order
Suppose that a=(a1,a2,…,an)∈ℝn, then we say that a is sorted in ascending order when for any i∈[1…n−1] ai≤ai+1
Sorted in Strictly Ascending Order
Suppose that a=(a1,a2,…,an)∈ℝn, then we say that a is sorted in strictly ascending order when bop_holds⁡(<,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=(a1,…,an) whenever we have ai⋆ai+1 for each i∈[1,…,n−1], we also define the predicate bop_holds⁡ as follows: bop_holds⁡(⋆,a)=T iff the above property holds true.
Sorted Tuple Predicate
Suppose that a∈ℝn then define the sorted_asc⁡:ℝn→{T,F} such that sorted_asc⁡(a)=bop_holds⁡(≤,a)
sorted_asc Holds iff It is Sorted in Ascending Order
sorted_asc⁡(a)=T iff a is sorted in ascending order
Sorted in Strictly Ascending order Predicate
Suppose that a∈ℝn then we define strict_asc_sorted⁡(a)=bop_holds⁡(<,a)
Set of a Tuple
Suppose that a=(a1,…,an) is a tuple, then we define the function set⁡(a)={ai:i∈[1,…,n]}
Strictly Ascending Sorting Function
Suppose that a∈ℝn then we define the function strict_asc_sort⁡:ℝn→ℝn such that if s=strict_asc_sort⁡(a) then we have strict_asc_sorted⁡(s)=T such that |a|=|s| and set⁡(a)=set⁡(s)
Intersection of Two Sorted Tuples
Suppose that a,b∈ℝn then a∩b is defined as the tuple s such that s=strict_asc_sort⁡(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=(a1,a2,…,an)∈ℝn, then we say that a is sorted in descending order when for any i∈[1…n−1] ai≥ai+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 (a1,a2,…,an)∈ℝn, then an inversion is a tuple i,j∈[1…n]×[1…n] such that i<j but ai>aj

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