{"entities":{"Q40319":{"pageid":40375,"ns":120,"title":"Item:Q40319","lastrevid":105427172,"modified":"2026-10-09T10:07:01Z","type":"item","id":"Q40319","labels":{"en":{"language":"en","value":"Well Quasi Orders"}},"descriptions":{"en":{"language":"en","value":"AFP entry Well_Quasi_Orders"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"0bd15088367b2612c3560582f11a5684f255a452","datavalue":{"value":"28605","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40319$B24271D3-7473-4CBD-918E-AC7684365DA9","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":"Q40319$D3CB4BAB-93B5-48D4-96C8-5EE0ECA65EA2","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"eb77717aae636251b69667559129db5462258f75","datavalue":{"value":"https://www.isa-afp.org/entries/Well_Quasi_Orders.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40319$A247BF06-E5C0-4AB0-9E78-889EE8AE4403","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40319$96DAC463-85C1-4F00-938C-9895595AAEDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40319$F5D22FCA-A453-4DCD-9DE7-8069B2923A1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40319$7E9C2DF7-6386-45CD-BD6A-5A457127387E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40319$BCB76DDA-7ED6-4EAA-8B91-64343012AEDF","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$BD093311-812F-4E5E-B96B-193EFBE4DFC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"61d0c0612cc30c9c51b93ddaf1f78ee1ae75f9fe","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$D0423642-E4EA-47F8-B297-23CC6A28C166","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$93CE2168-6B02-4CC1-BAC4-CE73ED855C89","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"d3a62eaf34da81f5e92b727b678d5beeaeb06686","datavalue":{"value":{"entity-type":"item","numeric-id":41247,"id":"Q41247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$202A9AA4-0D4D-4A8D-B23A-5BCFF7520FA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$A024716E-3AB0-4613-B032-1988A9428605","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ef8d4fcb901e471e97f6d315665a098aedf96b01","datavalue":{"value":{"entity-type":"item","numeric-id":53718,"id":"Q53718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$1F29A1F1-2682-4144-B0B4-D249F20FD865","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2778ef58df5d105bc5fcd1f1e6190b4cffc33d19","datavalue":{"value":{"entity-type":"item","numeric-id":40261,"id":"Q40261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$3B7393E2-BB29-4A4D-8A13-D5C08DC1CC4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"88ce92c4af709094185feda008c0e79821510197","datavalue":{"value":{"entity-type":"item","numeric-id":21947,"id":"Q21947"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$B590D92D-064C-45BE-8B5C-C9AABF34E830","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"169d14de70bf8d1baad42217a3a30ab4f80fc86e","datavalue":{"value":{"entity-type":"item","numeric-id":21746,"id":"Q21746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$91BA51FE-B4F5-4392-9CA9-99A7FD9AA947","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"139c69b2a23f419923a7989e28183ef8179b6836","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$5AC87E7E-A1D9-470A-B306-DEF9983AB229","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"56b7764d0d615099750cf4afce659a311d7bcae4","datavalue":{"value":{"entity-type":"item","numeric-id":31286,"id":"Q31286"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$F12B8FBF-1842-452D-998D-0628D92E77AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9aa564a0f52a6edc96b42c28a3944f2d40b4b32c","datavalue":{"value":{"entity-type":"item","numeric-id":21993,"id":"Q21993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40319$D92A5C83-B3D2-43B4-8FEE-7635841E95E9","rank":"normal"}],"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":"Q40319$AB2BE70E-85E6-4181-9F8F-0FECDE9B5E20","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7335db8cbac804a8435e80e80636b4dde04d73bd","datavalue":{"value":"Christian Sternagel","type":"string"},"datatype":"string"},"type":"statement","id":"Q40319$4DE115E8-655E-4E04-B6F3-2B46D44D6F11","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":"Q40319$2A006131-38F1-40E1-998B-4C1D4519AE2C","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":"Q40319$0C0885C4-AB88-42ED-9686-B08969AE86EA","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":"Q40319$49D222BA-0481-4984-89BD-72829C649A7F","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":"Q40319$CEFC2373-7AC8-4140-8378-3FA69A87C9BD","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":"Q40319$7C94A19E-0F2F-4D16-BE4D-0D2D011D1B43","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":"Q40319$BEB728B2-62FC-472E-8350-8D52F980F0AF","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":"Q40319$EA4CC42D-9087-4EB8-A931-423B6AB5ABB6","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":"Q40319$5A4278E4-63C2-473A-AAEF-30A6C42C97D5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Well Quasi Orders","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Well_Quasi_Orders"}}}}}