Formal target: Corpus.OEIS105210.conjecture_disjoint_starting_values

Cormier and Selfridge found 5 starting values for which the sequences appear to not merge.

Exact formal statement

∀ (j k : Nat),
  Membership.mem.{0, 0}
      (Insert.insert.{0, 0} 1
        (Insert.insert.{0, 0} 393
          (Insert.insert.{0, 0} 412 (Insert.insert.{0, 0} 668 (Singleton.singleton.{0, 0} 932)))))
      j →
    Membership.mem.{0, 0}
        (Insert.insert.{0, 0} 1
          (Insert.insert.{0, 0} 393
            (Insert.insert.{0, 0} 412 (Insert.insert.{0, 0} 668 (Singleton.singleton.{0, 0} 932)))))
        k →
      Ne.{1} j k →
        Eq.{1} (Inter.inter.{0} (Corpus.OEIS105210.sequenceSet j) (Corpus.OEIS105210.sequenceSet k))
          EmptyCollection.emptyCollection.{0}

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record