{"entities":{"Q5094473":{"pageid":7124049,"ns":120,"title":"Item:Q5094473","lastrevid":94264718,"modified":"2026-06-05T06:22:42Z","type":"item","id":"Q5094473","labels":{"en":{"language":"en","value":"Formalizing ordinal partition relations using Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7566889"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$F47E2889-1FF0-4806-BF07-F6C2C8605DB9","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"a4e19198a9c93606109c94d2665a430ae6c9c3da","datavalue":{"value":{"text":"Formalizing Ordinal Partition Relations Using Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5094473$3C7231DE-5029-47BA-BAE3-9F25048B0C64","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b87a3102b4ff8b27da381b4dc090a892d91ab719","datavalue":{"value":"10.1080/10586458.2021.1980464","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5094473$F821D48D-DB85-4CA7-89A1-96ED5A826A58","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7de47c3ec68b0b7b2a80923314e788ab2246fa9a","datavalue":{"value":{"entity-type":"item","numeric-id":446250,"id":"Q446250"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$3B71C16A-813C-4B53-84E8-15F61A513105","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"43720d5641a605df4a870ccd696a31d0b30078dc","datavalue":{"value":{"entity-type":"item","numeric-id":472315,"id":"Q472315"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$2CEB72D1-FB74-44D7-B850-FE3DD1234B4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$5AC0A5D8-8511-4B4F-B784-9A95A59284A3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"8ce533b63d10b7f2de5da010e89f9963c037687d","datavalue":{"value":{"entity-type":"item","numeric-id":2706533,"id":"Q2706533"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$02140B37-0A72-4EEE-96D0-6B1201A41DF5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"fa016bb6723a582b7104f77969047fbd7302b4b2","datavalue":{"value":{"time":"+2022-08-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5094473$1C66590B-9E4A-4F21-821F-FEB5B224D283","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5a50a0a33c931da5379c0fecb93631d43faf35c7","datavalue":{"value":"https://arxiv.org/abs/2011.13218","type":"string"},"datatype":"url"},"type":"statement","id":"Q5094473$972B7FC8-FE2F-4A3F-B1F0-3EB2676A219C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"ef68bb45cd2d5821c75b5f0eeb710e1b0eda186e","datavalue":{"value":"03E02","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5094473$A423FDAF-1B50-49D1-9270-8E43F58C5A56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"da00c812255bd7f02dddc14c65a56e042cf0446e","datavalue":{"value":"03E05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5094473$9BA021B3-E37B-41B0-A4B1-96385F0EDC5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7ae77b7014ae74d050ddd08c7570cbea14e17b7f","datavalue":{"value":"03E10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5094473$9EADD4B4-7605-450A-81A2-6588491548A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5094473$ACA9E04C-4363-4DC6-B8D1-4A1A42AC03A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5094473$D5AE74ED-97F9-4CA3-A2F8-540CE12F7BC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fee8f2ca1323cad9e9232d7279e663a6ec082a12","datavalue":{"value":"68V35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5094473$37F22133-F22C-44BE-AEB1-36D4AA72D72E","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"da304eda77033a67f3463da9600301041fc243df","datavalue":{"value":"7566889","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5094473$C4E50501-93FD-4F56-883D-E43991E3E886","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3c5d06c9c7bfafcdc4852e0a384a12838570908d","datavalue":{"value":"ordinal partition relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q5094473$76A5BF7A-7B1C-40A5-8D40-4FE02D6645AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b36a4092864d39bf9c99c5936b3d1261e44b9950","datavalue":{"value":"set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5094473$6CB58353-069A-4EEF-AA65-1FAAE8E65C7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5094473$404744C5-EE30-4A6E-A8FC-21E7FA115DCE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q5094473$71A21513-A6A0-499E-8E9C-3F60AFE35542","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q5094473$8FA447F3-9942-4B9C-B821-63CFB68EDDFF","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e338912f65cbd77347bbd512933e55736ef58bd1","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$7D3F33B6-B5F5-4E83-A8F1-117E04882935","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$664669CC-F1E5-413F-A7CE-226A78100B71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"07f544da61a733e790b6290335bb2f4a402f91cc","datavalue":{"value":{"entity-type":"item","numeric-id":35395,"id":"Q35395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$0CC41F20-A983-49EB-A82A-AF5E55B60938","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a9301974fbdbf3896f705a4c8ed840f169a9b63f","datavalue":{"value":{"entity-type":"item","numeric-id":19182,"id":"Q19182"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$FEA15D20-69F0-442E-9305-5135F6BBD538","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6a5699a860dd7dc9c732976be3ba437fb61ff7dd","datavalue":{"value":{"entity-type":"item","numeric-id":19322,"id":"Q19322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$A0125311-3B1F-4DC1-9C7D-A0206EFFE6C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$FD24F1DF-9AFB-4B44-B0EB-B6666C9E2BDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"31d2ddeef485fccfd3a5fe32ea329d2b65b4f1b4","datavalue":{"value":{"entity-type":"item","numeric-id":35396,"id":"Q35396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$7CBD0526-C05C-476F-9114-FB088496DB9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$11F7F03B-FA65-47D2-81A0-5A96F86B1A9E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ecb36fec89ff827cd73a8ca1a85f36a2e419c34e","datavalue":{"value":{"entity-type":"item","numeric-id":13377,"id":"Q13377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$D1DDC339-F696-4EAF-AAC3-156ACD3879F6","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$7E89915E-971B-4B38-A0DA-78330386D32B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"fe87c6940c35c6de1e37b3c42e7d28db5e15412d","datavalue":{"value":"W3206346340","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5094473$DD06F942-77B4-4F09-839D-D0EF92115E93","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"30934abbc32128e5c1a91e04943aee41658d6f31","datavalue":{"value":{"entity-type":"item","numeric-id":1694568,"id":"Q1694568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$D49DB37C-3172-4C5D-A3C2-7143F706C096","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49023bd5aa461c9f63f0725228815aa2af2e478f","datavalue":{"value":{"entity-type":"item","numeric-id":5747646,"id":"Q5747646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$A7860B4D-348F-45A4-B3FC-AF7B27C9149E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d0e0d2f6f6067cafe5004d11baa83402037d817","datavalue":{"value":{"entity-type":"item","numeric-id":4916054,"id":"Q4916054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$EDA75798-52F2-49C8-88B8-576F18CC23A4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f354b8eec708ff059e8b857d312e027ab0efb65b","datavalue":{"value":{"entity-type":"item","numeric-id":2562081,"id":"Q2562081"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$23921B2C-7A84-4D66-B0DC-2D062C5DC17C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ca7e027091589776f78a6d7ad8457e805c17b28","datavalue":{"value":{"entity-type":"item","numeric-id":5777498,"id":"Q5777498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$0C6A45D8-39B1-43C5-B3BE-87E8971C01C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a9e9cd00bd888e0c2ec3144ef21f154ae7d49a0","datavalue":{"value":{"entity-type":"item","numeric-id":5573370,"id":"Q5573370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$260ABEE6-F009-4C9D-9463-D45DA7AD1C07","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbeda89ac2a3ea929d234b729dd0cd1bfa4b6aab","datavalue":{"value":{"entity-type":"item","numeric-id":3778761,"id":"Q3778761"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$35609CFB-0475-4188-BB68-B38419A94171","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5bef25bf28ebce0c8dc4719615dc3b84fe63927","datavalue":{"value":{"entity-type":"item","numeric-id":3233344,"id":"Q3233344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$1129B80B-B1E8-48DB-9F5F-2E4A670A5BC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e703bce69e980fe1560eee6510aff487fcb0309e","datavalue":{"value":{"entity-type":"item","numeric-id":1062673,"id":"Q1062673"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$F34B2DEE-111D-4F4F-B34C-5ED6C0EA8291","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9fb077dc2fa4aa97a42af62fda1019437d3f6ca","datavalue":{"value":{"entity-type":"item","numeric-id":3215221,"id":"Q3215221"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$8867F7C1-5491-429E-9E50-0E9E80641AB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc05e7fe24ec86ef16233bf0c5792273a4614ef0","datavalue":{"value":{"entity-type":"item","numeric-id":4053665,"id":"Q4053665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$33326B7B-3B65-4001-940B-BA1D35E83ED2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c970e8ce2457c29e8457681a06ca02889857b294","datavalue":{"value":{"entity-type":"item","numeric-id":4401454,"id":"Q4401454"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$C507E0DF-59F7-4309-B0EC-8E946529AA02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5aab69d140b5ba265eb63d058537f581b13c23f4","datavalue":{"value":{"entity-type":"item","numeric-id":2955752,"id":"Q2955752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$5CD3E979-092C-4754-AEB5-DDF7A47B7AF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cb4857d0d243b746647a153e1690cd4acc84f69e","datavalue":{"value":{"entity-type":"item","numeric-id":5280247,"id":"Q5280247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$EA0FF276-6898-4F4B-B1FC-B82BDDEB625F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67a0619f07c8313163d5395382f74c59a1da4d00","datavalue":{"value":{"entity-type":"item","numeric-id":5448058,"id":"Q5448058"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$93DD1EFC-6BDC-408A-80DC-B7F550CDB601","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34f831bdd0445bbb207a58535cee0f990813469d","datavalue":{"value":{"entity-type":"item","numeric-id":2655322,"id":"Q2655322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$73698702-BEDA-4D0F-B82A-FC8A5B4A7EDA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"34dd873a66486e9e38fc156a4b8aa6ba19960bb7","datavalue":{"value":{"entity-type":"item","numeric-id":3088003,"id":"Q3088003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$2013AA86-5782-4E54-B95F-7F1A87C56DA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"68c91066f858fa64a799af591825e0694228fffb","datavalue":{"value":{"entity-type":"item","numeric-id":4122841,"id":"Q4122841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$F2E0412B-4C13-49F8-955A-A25FB6F3CC96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"65c8c8ed706a86d97db05d5b778c49fb79be8a30","datavalue":{"value":{"entity-type":"item","numeric-id":1144013,"id":"Q1144013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$E714722E-8A8A-4E4B-8563-10C60B9C73E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"410758c42f999c02dc0101939bddf60a260ea3ea","datavalue":{"value":{"entity-type":"item","numeric-id":1191918,"id":"Q1191918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$CB74EA43-1A22-4263-929C-B3233A612A97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61621a25c1d2828341801c1766512d672764dedb","datavalue":{"value":{"entity-type":"item","numeric-id":5183500,"id":"Q5183500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$2EB82FD0-69A3-44FB-9A35-3FEEBD1F040B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dd75fa562171f1bc8488c55c38ad826341f610ad","datavalue":{"value":{"entity-type":"item","numeric-id":2543669,"id":"Q2543669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$9E1F0CEE-15E2-408B-8209-06D1D9B49DFA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e0dffc55f1a93c6cf3f7f56c1bd747358a0b606f","datavalue":{"value":{"entity-type":"item","numeric-id":3837736,"id":"Q3837736"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$92CFE137-233B-4DCB-B763-672319DAE124","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f1cf7e426127d502c57b4bb01a758b7cc7fadf5","datavalue":{"value":{"entity-type":"item","numeric-id":5337204,"id":"Q5337204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$EB1FBA1E-4E7F-4E9A-AAF3-B7CD68DEFEE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$F8665A6E-06DA-4151-B4CF-A8D55643F14D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f4d5de220317fd709a7e63acdecfb92f5c42b492","datavalue":{"value":{"entity-type":"item","numeric-id":2280211,"id":"Q2280211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$A97CD5A1-D61B-4842-A4A9-B1C516B51444","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8c3064cbe75bec6f186869899bd3d6fb1331ce8","datavalue":{"value":{"entity-type":"item","numeric-id":636357,"id":"Q636357"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$9C067724-4F3B-4B20-8EC2-ABDD2AAD5BC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ffe1da045a7bbdb406dcccc9155b5cffc83f9be7","datavalue":{"value":{"entity-type":"item","numeric-id":769270,"id":"Q769270"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$5E29B372-82C8-4C8E-9E6F-715EF9712AD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"add39993ad64fcea5e8edce49e746268fda7e488","datavalue":{"value":{"entity-type":"item","numeric-id":1111550,"id":"Q1111550"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$71F34B3E-B3B0-4D5B-907A-C2322E9AD7F4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"06c000009930df9c8318a8d9f5bca7755b9a8b21","datavalue":{"value":{"entity-type":"item","numeric-id":4040819,"id":"Q4040819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$41C842B7-87CE-4D1F-AB28-8E2A413847C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4fc287ec8a6e146c3e57a73c560da2d9b4de9d84","datavalue":{"value":{"entity-type":"item","numeric-id":3579526,"id":"Q3579526"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$0F75823F-C69E-4EF7-99F3-7C3380736CD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4ef8738eccd7b653460e41e83660d0f8b8c95df","datavalue":{"value":{"entity-type":"item","numeric-id":2881098,"id":"Q2881098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$13B8F39B-EDA4-4F53-869A-DD22C0F3BDB4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f6946cd334a576097a16d5346c4ccb4db32e8d67","datavalue":{"value":{"entity-type":"item","numeric-id":5961491,"id":"Q5961491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50c3c341979477a4939f812ef24744ee021b1ca2","datavalue":{"value":{"amount":"+0.7716537714004517","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5094473$3A3EC6CF-66EB-48A5-9B54-B9A19A818D64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b653490062e2722e03fa974cf4f542752f3cd1b","datavalue":{"value":{"entity-type":"item","numeric-id":2879247,"id":"Q2879247"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f640778398b5ee417ba18839ecc6993de08519d2","datavalue":{"value":{"amount":"+0.7621093392372131","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5094473$3B2FB7BE-83C9-4C9F-BFB7-5789D677BFD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"67817ded466701f9bbe95b0240a3a1e5b5ec9fbc","datavalue":{"value":{"entity-type":"item","numeric-id":5327341,"id":"Q5327341"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c69165d325af04653b72e805cc80810df41a93a0","datavalue":{"value":{"amount":"+0.7514740228652954","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5094473$FAFCE75E-F420-42D9-8801-F2397DDE1653","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"10712b80cd7952b3c9a1b6eb094b1a55922e0e6a","datavalue":{"value":{"entity-type":"item","numeric-id":5111307,"id":"Q5111307"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b22c7014040b9ff58d26775e58f0eda1e6a18ff5","datavalue":{"value":{"amount":"+0.7418400049209595","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5094473$1D2986B1-EF61-4B3B-B9D5-93B36DBF4BB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a0ea3a15d6367636d22543fb15a9c56e3bc93a57","datavalue":{"value":{"entity-type":"item","numeric-id":2333671,"id":"Q2333671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed2fc4e213b318cf2973f35fd8e54b6fd178e594","datavalue":{"value":{"amount":"+0.7239910960197449","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5094473$28C0EDD7-F208-4C9A-A0F4-BF65C4EFB69B","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"c39a117a349789e54237c0a3254f5a10c0a6517e","datavalue":{"value":{"entity-type":"item","numeric-id":6830565,"id":"Q6830565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5094473$247B69E0-F443-44AC-92E3-5A4D9E3541AE","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Formalizing ordinal partition relations using Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Formalizing_ordinal_partition_relations_using_Isabelle/HOL"}}}}}