Ackermannian and Primitive-Recursive Bounds with Dickson’s Lemma

Dickson’s Lemma is a simple yet powerful tool widely used in
decidability proofs, especially when dealing with counters or related
data structures in algorithmics, verification and model-checking,
constraint solving, logic, etc. While Dickson’s Lemma is well-known,
most computer scientists are not aware of the complexity upper bounds
that are entailed by its use. This is mainly because, on this issue,
the existing literature is not very accessible. We propose a new
analysis of the length of bad sequences over (N^k , ≤), improving on
earlier results and providing upper bounds that are essentially tight.