### Abstract

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.

### License

BSD License

### 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.

### Topics

- Mathematics/Combinatorics

### Session Well_Quasi_Orders

- Infinite_Sequences
- Minimal_Elements
- Least_Enum
- Almost_Full
- Minimal_Bad_Sequences
- Higman_OI
- Almost_Full_Relations
- Well_Quasi_Orders
- Kruskal
- Kruskal_Examples
- Wqo_Instances
- Multiset_Extension
- Wqo_Multiset

### Depends on

- Abstract Rewriting
- Open Induction

### Used by

- Substitutions for Lambda-Free Higher-Order Terms
- Extensions to the Comprehensive Framework for Saturation Theorem Proving
- A Comprehensive Framework for Saturation Theorem Proving
- Decreasing Diagrams II
- The Myhill-Nerode Theorem Based on Regular Expressions
- Executable Multivariate Polynomials

## Cite

×

Well_Quasi_Orders-AFP

    @article{Well_Quasi_Orders-AFP,
      author  = {Christian Sternagel},
      title   = {Well-Quasi-Orders},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Well_Quasi_Orders.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012