Well-Quasi-Orders (Q7361640)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Well_Quasi_Orders
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Well-Quasi-Orders |
AFP entry Well_Quasi_Orders |
Statements
13 April 2012
0 references
Christian Sternagel
0 references
Well-Quasi-Orders (English)
0 references
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.
0 references
