{"entities":{"Q7361640":{"pageid":31520459,"ns":120,"title":"Item:Q7361640","lastrevid":105367868,"modified":"2026-10-07T13:37:17Z","type":"item","id":"Q7361640","labels":{"en":{"language":"en","value":"Well-Quasi-Orders"}},"descriptions":{"en":{"language":"en","value":"AFP entry Well_Quasi_Orders"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2cc174eb58bf02bcaa6ca77f7de4ad3130b6de0a","datavalue":{"value":"https://isa-afp.org/entries/Well_Quasi_Orders.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361640$04807DC6-6FBA-4685-888E-AAF19F319F1F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"e3538f66ac447e631727bb2ad2d214ee0bd11997","datavalue":{"value":{"time":"+2012-04-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361640$C696799A-54DF-4AFA-9D0A-580FC3021B52","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7335db8cbac804a8435e80e80636b4dde04d73bd","datavalue":{"value":"Christian Sternagel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361640$89E0858F-281A-4F38-8B9C-D3080603C8E1","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"da39ac72b499099382fea6599b640e5617766c4a","datavalue":{"value":{"text":"Well-Quasi-Orders","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361640$4688400C-D3E8-4FC6-A816-0FC71E751447","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a7e17732f98a1c520168005b60d8c3ead1fb62d1","datavalue":{"value":"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.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361640$49B7193C-4E79-4984-B8CB-18018AC3501B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ed0853d5d25943754f0b88d3bc5a4e688b584cb","datavalue":{"value":{"entity-type":"item","numeric-id":5734436,"id":"Q5734436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361640$E12552CB-C62D-4430-A760-0E18D6FB3D5C","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361640$6D031FB0-A3CE-4B48-A530-CEE0BE0B7D64","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"bb0293970cb12cb0c0b06315232bb60667277b31","datavalue":{"value":{"entity-type":"item","numeric-id":7361362,"id":"Q7361362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361640$A71F0097-59BD-4850-BBD1-C7DED17BDBFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"890c0c4a61156b4e729dc9fcff8e39e1971a8f5e","datavalue":{"value":{"entity-type":"item","numeric-id":7361686,"id":"Q7361686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361640$0DE24736-6D85-493A-9697-488DEA8FE9E9","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"5634edfbfbc0239093a6d080d47ef70273afec4d","datavalue":{"value":{"entity-type":"item","numeric-id":7360824,"id":"Q7360824"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361640$0D400B59-8B43-49FD-9DF2-58F8CA3969BF","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361640$A0AE803F-9639-4E6B-ABCB-E1140852AC95","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Well-Quasi-Orders","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Well-Quasi-Orders"}}}}}