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 Cited by 5 Authors 2 Sternagel, Christian 1 Felgenhauer, Bertram 1 Nagele, Julian 1 Thiemann, RenĂ© 1 Zankl, Harald Cited in 1 Serial 1 Logical Methods in Computer Science Cited in 2 Fields 3 Computer science (68-XX) 2 Mathematical logic and foundations (03-XX) Citations by Year