Christian Sternagel 📧

April 13, 2012


Based on Isabelle/HOL's type class for preorders, we introduce a type class for well-quasi-orders (wqo) which is characterized by the absence of "bad" sequences (our proofs are along the lines of the proof of Nash-Williams, from which we also borrow terminology). Our main results are instantiations for the product type, the list type, and a type of finite trees, which (almost) directly follow from our proofs of (1) Dickson's Lemma, (2) Higman's Lemma, and (3) Kruskal's Tree Theorem. More concretely:
  • If the sets A and B are wqo then their Cartesian product is wqo.
  • If the set A is wqo then the set of finite lists over A is wqo.
  • If the set A is wqo then the set of finite trees over A is wqo.
The research was funded by the Austrian Science Fund (FWF): J3202.
BSD License

Change history

June 8, 2017

Proved (classical) equivalence to inductive definition of almost-full relations according to the ITP 2012 paper "Stop When You Are Almost-Full" by Vytiniotis, Coquand, and Wahlstedt.

January 3, 2016

An alternative proof of Higman's lemma by open induction.

July 9, 2014

Simplified proofs of Higman's lemma and Kruskal's tree theorem, based on homogeneous sequences.

May 16, 2013

Simplified construction of minimal bad sequences.

December 19, 2012

New variant of Kruskal's tree theorem for terms (as opposed to variadic terms, i.e., trees), plus finite version of the tree theorem as corollary.

June 11, 2012

Added Kruskal's Tree Theorem.


Theories of Well_Quasi_Orders