Well Quasi Orders

swMATH ID: 28605
Software Authors: Christian Sternagel
Description: Well-Quasi-Orders. 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.
Homepage: https://www.isa-afp.org/entries/Well_Quasi_Orders.html
Dependencies: Isabelle
Related Software: Archive Formal Proofs; CeTA; Isabelle/HOL; Decreasing Diagrams II; Isabelle; Open Induction; Myhill-Nerode; CiME; CSI; ACL2; KBCV; mkbTT
Cited in: 3 Documents

Citations by Year