Email Gateway (Aug 18 2022 at 19:35): Email Gateway (Aug 18 2022 at 19:35):From: Tobias Nipkow <nipkow@in.tum.de>
Well-Quasi-Orders
Christian Sternagel
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 two main results are instantiations for
the product type and the list type, which (almost) directly follow from our
proofs of (1) Dickson's Lemma and (2) Higman's Lemma. 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 its finite subsets is wqo.
The research was funded by the Austrian Science Fund (FWF): J3202.
http://afp.sourceforge.net/devel-entries/Well_Quasi_Orders.shtml
Note that this entry is only available in the development version (until the
release).
Last updated: Apr 20 2024 at 04:19 UTC