🏗️ ΘρϵηΠατπ🚧 (under construction)

Tuple
Let I be an index set, and S a set then we say that a function t:IS is a tuple,
Empty Tuple
Suppose t:IS 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 idom(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,bZ or is some IZ

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

When an Integer Indexed Tuple is Empty
Suppose that i>jZ then (ai,,aj)=()
Finite Tuple Equality
We define two n tuples (x1,x2,...,xn) and (y1,y1,...,yn) to be equal when i[1n],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=zi1
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)Rn, then we say that a is sorted in ascending order when for any i[1n1] aiai+1
Sorted in Strictly Ascending Order
Suppose that a=(a1,a2,,an)Rn, 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 aiai+1 for each i[1,,n1], we also define the predicate bop_holds as follows: bop_holds(,a)=T iff the above property holds true.
Sorted Tuple Predicate
Suppose that aRn then define the sorted_asc:Rn{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 aRn 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 aRn then we define the function strict_asc_sort:RnRn 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,bRn then ab 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)Rn, then we say that a is sorted in descending order when for any i[1n1] aiai+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)Rn, then an inversion is a tuple i,j[1n]×[1n] 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