Christian Sternagel 📧

April 13, 2012

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


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.


Session Well_Quasi_Orders