This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Telephone numbers

module elementary-number-theory.telephone-numbers where

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.multiplication-natural-numbers
open import elementary-number-theory.natural-numbers

Idea

The telephone numbers are a sequence of natural numbers that count the way n telephone lines can be connected to each other, where each line can be connected to at most one other line. They also occur in several other combinatorics problems.

Definitions

telephone-number : ℕ → ℕ
telephone-number zero-ℕ = succ-ℕ zero-ℕ
telephone-number (succ-ℕ zero-ℕ) = succ-ℕ zero-ℕ
telephone-number (succ-ℕ (succ-ℕ n)) =
  (telephone-number (succ-ℕ n)) +ℕ ((succ-ℕ n) *ℕ (telephone-number n))