Telephone numbers

Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Eléonore Mangel.

Created on 2022-03-24.
Last modified on 2024-10-16.

module elementary-number-theory.telephone-numbers where
Imports 
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))

Recent changes