The tuple index operation extracts a specific number from a tuple. which is an ordered sequence of numbers. For example, if A is a tuple and (= A (<,> (<,> (2) (5)) (7))), then (= (_ A (1)) (2)), (= (_ A (2)) (5)), and (= (_ A (3)) (7)). The index operation is defined here. If the index goes above the length of the tuple, it will still return a number, but this is not a meaningful value and theorems should be constructed in such a way that the index never goes above the tuple length.