{"entities":{"Q2362108":{"pageid":2372851,"ns":120,"title":"Item:Q2362108","lastrevid":73998786,"modified":"2026-04-14T18:00:14Z","type":"item","id":"Q2362108","labels":{"en":{"language":"en","value":"Proving divide and conquer complexities in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6740210"}},"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":"Q2362108$5FE584F9-B5A1-4CFE-A880-A4B9A1781FCD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"6b43d9a22929513897491a8c177fd781cb75d613","datavalue":{"value":{"text":"Proving divide and conquer complexities in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2362108$491EEC42-9263-4C7B-97E3-47055CFDA309","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3e4e53eaee84ab95d187ad7167cc6c111554adbb","datavalue":{"value":"1414.68101","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362108$F9B0EEAD-D65D-4584-99DD-457BF30D2AF2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cc3155209aecfa73c406ca3d6ea19dfb5eb798dd","datavalue":{"value":{"entity-type":"item","numeric-id":1791157,"id":"Q1791157"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$21E6E847-A5D0-4551-A97C-B4399A4FECE6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$A9EE3919-186B-4351-B775-AF1047C38CB9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1a7c9d02f6a4a594410711d22dd1a021deb4336e","datavalue":{"value":{"time":"+2017-07-06T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2362108$6C95A3C9-B132-4676-9A51-946ABBC903E3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362108$7C99D564-9E41-477C-B31B-289497676085","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"44bc3f4b62b406982652a23d68d9c7868a54f1c6","datavalue":{"value":"11B37","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362108$4EC15751-06DB-47BE-8002-6B13FD1279DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdd9498216d1fd2eff80e5a7d18782b649eb7b2f","datavalue":{"value":"68Q25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362108$94CF3514-A070-4B64-B95C-BFC2DA37CC76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a7ddaa80bf0a693a36c1113ff6b7ad576f729940","datavalue":{"value":"68W40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362108$8DD3FB86-2C34-45BF-B5D7-EDA1F4F59A48","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"1013d32068b539302b32491dee208e5dc34e6805","datavalue":{"value":"6740210","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362108$572AF915-1F67-41E7-A9A0-F8FD3B780710","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"42f0513e500ea6cb630e73925875c7d53ca8d8e1","datavalue":{"value":"Isabelle/HOL","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362108$83F8E102-13C7-460F-847B-0260BCF90FC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9737f2eb43102479e3690c2e4a0bc51b9c713f4a","datavalue":{"value":"master theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362108$410C868E-C015-45F1-99BB-288AC1FAB97B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0eccb55bb14eb00051ebb90021abf587fd99fd3f","datavalue":{"value":"Akra-Bazzi method","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362108$A4E4F366-9F36-4929-92BE-7C7A76300974","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ab7f5cc6872a3f307708a71344585db2582ae61","datavalue":{"value":"divide and conquer algorithms","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362108$1C915F75-C247-4A9E-9486-C49229BA1306","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"822cf761320ae981600fa5131c4ef28d23165994","datavalue":{"value":"recurrences","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362108$7441D15C-EE3B-46E4-A4B4-364514710EB6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c5f8382ba04f9f05f645b4d0e4b9ea28f0619583","datavalue":{"value":"complexity","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362108$C29A3308-F34D-41C4-93A4-F15350D5E63A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3919614b15baf685cf251ec0f8f0d280752ec3de","datavalue":{"value":"Landau symbols","type":"string"},"datatype":"string"},"type":"statement","id":"Q2362108$AD8A631A-361B-451D-9AC4-6F6F22DE4BE0","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$D45F23F8-0E34-4216-B8B3-9352D9498385","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2ad21f150c621099eebc7c2e673cd9cf43b81a4e","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$36C70A1C-DCCA-4685-8517-E82D94DC569F","rank":"normal"},{"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":"Q2362108$24FF7B32-6325-4AAA-A9E0-190103AB5311","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":"Q2362108$A1446780-E652-4728-8434-4FD0C9C34985","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$C2D15708-F9FF-48F3-93F6-8393C93BD93C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"06cbd430a522cc7ac15df8059f9a9059e73bcf27","datavalue":{"value":{"entity-type":"item","numeric-id":40309,"id":"Q40309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$992CC3FF-33AC-4CCE-B77E-61170DAD449C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"29cdafe150c2f905fae45ec9e0724a076d6dee21","datavalue":{"value":{"entity-type":"item","numeric-id":41251,"id":"Q41251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$1E276753-08CE-4109-B79F-B911C32C9DF1","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":"Q2362108$6946F027-A791-41CC-9D39-6C5B8607A08D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f0c5c0ab1481a262342ba9032917c1160d66669d","datavalue":{"value":"https://doi.org/10.1007/s10817-016-9378-0","type":"string"},"datatype":"url"},"type":"statement","id":"Q2362108$5924607C-95F3-41EE-AD3E-6F8B431A6052","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"c718e352ee4528705a10ddf4d6484c3f527caa99","datavalue":{"value":"W2439261032","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362108$8E2DC2EA-2B3B-46C4-90D8-C18A9E810170","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f9d5bcfcc14baede38744ad40f0edaa936f41a5","datavalue":{"value":{"entity-type":"item","numeric-id":1384098,"id":"Q1384098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$0D47DABD-017E-4AAB-B53B-0BB0EA4EBEC7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b614d2d330f36bdd9ecd3e94fb292809877a0f54","datavalue":{"value":{"entity-type":"item","numeric-id":5307073,"id":"Q5307073"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$92A2B627-6F2B-4BC4-96D1-3CE94166E528","rank":"normal"},{"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":"Q2362108$8AA2B729-7507-4092-9CE7-C62D46ABD35F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4738798d9702e646d9743f53f948745583da971","datavalue":{"value":{"entity-type":"item","numeric-id":2352487,"id":"Q2352487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$57B0140D-525F-4805-B772-20266621653A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e17626c1e3e9192fae00966e078b91a6b8e2bf1","datavalue":{"value":{"entity-type":"item","numeric-id":1402216,"id":"Q1402216"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$1702901D-9CA2-4E87-B0AA-E96C7C009B0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5979a4a5d63c67afe6c18affb7f1968a7f2f2ddf","datavalue":{"value":{"entity-type":"item","numeric-id":4307367,"id":"Q4307367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$05C230D5-9C4E-4E08-9090-D6E62CC2B84D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9194e9b150f8488fef979658da21ddd0e60751fc","datavalue":{"value":{"entity-type":"item","numeric-id":3651735,"id":"Q3651735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$01A15D1F-1A75-4C01-9C79-044809931A14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb6782a66ef7f31e37d89d8a293f958ea0d831d0","datavalue":{"value":{"entity-type":"item","numeric-id":5395714,"id":"Q5395714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$06C9D83D-0460-4D43-AC05-E7AD3FE9A678","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"931c42c28f22f89fe1b66164f9ececc2021ac1a2","datavalue":{"value":{"entity-type":"item","numeric-id":3558332,"id":"Q3558332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2362108$60B439FC-6AF0-4681-A8D8-19FBF909A203","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"93ecbe14058a11c6e1891baef9ebfdcb93d30b0c","datavalue":{"value":"10.1007/S10817-016-9378-0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2362108$318CA46E-B12A-4CA7-B0A6-5CE9A0D7C651","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2d15a252dba354bc809c968447be7f718d12cdb2","datavalue":{"value":{"entity-type":"item","numeric-id":4289841,"id":"Q4289841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"48136de901acf413ac39915c271b650c818521b6","datavalue":{"value":{"amount":"+0.7684710025787354","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":"Q2362108$A10463A2-E49B-4FA3-9CAC-9CEC61A3D2AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ce36279d9f16748ade3aa0dea07c25cef3847fd8","datavalue":{"value":{"entity-type":"item","numeric-id":4571976,"id":"Q4571976"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce9c35b52d368e611f27d76fd50df24829aa41de","datavalue":{"value":{"amount":"+0.7557930946350098","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":"Q2362108$7715D41C-76CF-426D-8C14-C9E7DE81AA35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ea2147be9ac76d6efb1010457a087e07b06b6700","datavalue":{"value":{"entity-type":"item","numeric-id":3578209,"id":"Q3578209"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"37b5af096446fa12a25faae90cdf6685bc7e8a3a","datavalue":{"value":{"amount":"+0.7478653788566589","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":"Q2362108$EABA0E2C-0391-442B-B191-C05395581C6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bdd8629d35d77d162d5b8ee546d6ed3df9fe45fe","datavalue":{"value":{"entity-type":"item","numeric-id":1847368,"id":"Q1847368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"97c2368acbf25d19cad55ef7dd2d353a572001f2","datavalue":{"value":{"amount":"+0.7173070907592773","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":"Q2362108$6AAA6AE4-587C-43FA-882F-C590BDDCE891","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a5a98c176a419a8a3a0823cfef662262d45208c4","datavalue":{"value":{"entity-type":"item","numeric-id":4337634,"id":"Q4337634"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"df6eb32cf4bfaef36432b436b346a3758cd5c16d","datavalue":{"value":{"amount":"+0.7165141105651855","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":"Q2362108$8CE60B08-A9F5-4FEF-8F66-FB97E004AE0E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proving divide and conquer complexities in Isabelle/HOL","badges":[]}}}}}