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 orderwhen
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