## Ordered Pair

(<,> x y) represents an ordered pair of numbers. Each ordered pair maps to a single number. The first number in the pair can be obtained from using the head operation. The second number can be extracted using the tail operation.

### Definition

The ordered pair (<,> x y) is defined using triangular numbers:

(= (<,> A B) (+ (tri (+ A B)) A)) /edit/peano/peano_thms.gh/df-op

This formula basically counts every space on a 2D grid, by traveling along the diagonals in the following sequence where each column is a new value of x and each row is a new value of y starting with 0. The triangular numbers form the first column.

• 0 2 5 9 14
• 1 4 8 13
• 3 7 12
• 6 11
• 10

Continuing to count in this fashion along the diagonals gives as a one-to-one correspondence between the ordered pairs and individual numbers.

Every individual number maps to a pair of numbers and that mapping is unique for both the first number and the second number.

### Theorems

• Equivalence: (<-> (= (<,> A B) (<,> A' B')) (/\ (= A A') (= B B'))) /edit/peano/peano_thms.gh/opth
• Expand into head and tail: (= A (<,> (head A) (tail A))) /edit/peano/peano_thms.gh/opexpand