Formal target: Corpus.OEIS52709.conjecture

Conjecture: for $n > 0$, $a(n)$ is also the number of sequences of length $n - 1$ covering an initial interval of positive integers and avoiding three terms $(\dots, x, \dots, y, \dots, z, \dots)$ such that $x \le y \le z$.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 0 n →
    ∀ [inst : Fintype.{0} (Set.Elem.{0} (Corpus.OEIS52709.sequencesCountedByA052709 n))],
      Eq.{1} (Corpus.OEIS52709.a n) (Fintype.card.{0} (Set.Elem.{0} (Corpus.OEIS52709.sequencesCountedByA052709 n)))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record