Sulanke arrays

DefinitionSulanke array B#✓fully proved

The Sulanke array \(B\) assigns a natural number \(B(k, i)\) to every pair of natural numbers \(k\) and \(i\). It is defined by recursion on \(k\): \(B(0, 0) = 1\), \(B(0, i) = 0\) for \(i \ge 1\), \(B(k+1, 0) = B(k, 0)\), and for all \(k\) and \(i\)

\[B(k+1, i+1) = \bigl(B(k, i+1) + 2B(k, i)\bigr) + \bigl(B(k, i) + 2B(k, i-1)\bigr),\]

where \(B(k, -1)\) is read as \(0\).

This is the recurrence obtained by eliminating the Sulanke array \(A\), given by \(A(k+1, i) = B(k, i) + 2B(k, i-1)\), from \(B(k+1, i) = A(k+1, i) + A(k+1, i-1)\), with values at negative indices read as \(0\).

def sulankeB : ℕ → ℕ → ℕ
  | 0, 0 => 1
  | 0, _ + 1 => 0
  | k + 1, 0 => sulankeB k 0
  | k + 1, n + 1 =>
    (sulankeB k (n + 1) + 2 * sulankeB k n) +
      (sulankeB k n + 2 * match n with | 0 => (0 : ℕ) | m + 1 => sulankeB k m)

Used by 1

Used bySulanke array A

DefinitionSulanke array A#✓fully proved

The Sulanke array \(A\) assigns a natural number \(A(k, i)\) to every pair of natural numbers \(k\) and \(i\). It is defined from the Sulanke array \(B\) by \(A(0, i) = 0\) for every \(i\), \(A(k+1, 0) = B(k, 0)\) for every \(k\), and \(A(k+1, i+1) = B(k, i+1) + 2B(k, i)\) for all \(k\) and \(i\).

def sulankeA : ℕ → ℕ → ℕ
  | 0, _ => 0
  | k + 1, 0 => sulankeB k 0
  | k + 1, n + 1 => sulankeB k (n + 1) + 2 * sulankeB k n

Uses 1

Statement usesSulanke array B

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.