{"entities":{"Q437040":{"pageid":438807,"ns":120,"title":"Item:Q437040","lastrevid":61857405,"modified":"2026-04-11T02:08:00Z","type":"item","id":"Q437040","labels":{"en":{"language":"en","value":"Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6057742"}},"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":"Q437040$DDD5FC25-CC30-4400-97AA-DF9B87653FAE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f42d85990899a099cd81d6046947c309ba4ce9f5","datavalue":{"value":{"text":"Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q437040$41674D1F-5552-4D56-BD58-4F245A8EED5D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"89383cb1427b5178a3c7a7b0ec84784a107a567e","datavalue":{"value":"1242.68284","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q437040$E4883E44-6E3F-40E2-9024-10A36182E921","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d4bf01e8df1c87de639938e4e74854e4e2315839","datavalue":{"value":{"entity-type":"item","numeric-id":437038,"id":"Q437038"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$94F06F71-2835-4F94-835D-E147FE127054","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"34804e6a2215a0425fe35226b8ec01b24c6b23d2","datavalue":{"value":{"entity-type":"item","numeric-id":437039,"id":"Q437039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$5013B044-EAE8-48C7-A1D4-BD8CFDC2A674","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":"Q437040$E051AAE9-563D-4E2D-819B-2CDB8E7D45F9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"84ece3a61d19e8a79724038a31d8c2f410ad0a43","datavalue":{"value":{"time":"+2012-07-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q437040$52A93B76-78A0-4CE7-BEFD-F7DB4D823F4D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q437040$B34DA742-27B5-45B7-AAE8-E2C313B3ECCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ca8c16691e9ec83d46a3995338b09d48ac9660ac","datavalue":{"value":"68M10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q437040$A9DD46E4-5223-443B-8F3D-962FE6CB3A1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"344f62a15ccd40e690364bd758985e8313f47f4a","datavalue":{"value":"68R10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q437040$710B46E2-C459-4E98-8060-100948574656","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"125351f57395493891bce0af407f619f2b7b669d","datavalue":{"value":"6057742","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q437040$4D1CD0D4-CE0D-4EEC-9A40-5A3428FE6D12","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0639fa0857b9d8519bd9cd7d3086786a4f44d41b","datavalue":{"value":"deadlock-free routing","type":"string"},"datatype":"string"},"type":"statement","id":"Q437040$C3EA4A12-6DA2-42A9-98E4-9AD9566CDD08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q437040$891576FC-FE82-48AF-944E-0E648B081E65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"24dd5926fa2c4f0ee181b086899e10f05b3e9148","datavalue":{"value":"ACL2","type":"string"},"datatype":"string"},"type":"statement","id":"Q437040$7525A960-6BF9-4E01-8CF2-2C51B01CF3F5","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8c652637493e8de65377ba80065ca4183c6dc627","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$4CCCC316-13A4-4EDE-983C-12A37440DDEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$937367FA-AD67-43F4-A70D-F6395BDEEA02","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":"Q437040$3F468D91-4217-49CA-A9A1-FB8EFAFD4BE3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8dcfdf7bea644bdf5862372c295b6cc60221f821","datavalue":{"value":"https://doi.org/10.1007/s10817-010-9206-x","type":"string"},"datatype":"url"},"type":"statement","id":"Q437040$7C6A9C1E-1864-4494-9CAB-F943A1C95EDF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"a78b176434fc04c8f9f2c3fc1ab076fde10fad33","datavalue":{"value":"W2056997919","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q437040$A09D3AF8-3D36-4473-A3EA-506BB783FA1D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"df99d010c323d1ce4719d0c5115c3a289e30a204","datavalue":{"value":{"entity-type":"item","numeric-id":1107510,"id":"Q1107510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$F9D81BA1-EF9F-4647-B792-BECC6907EAA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$ED4A4B1E-9131-4C83-8119-8966264EBB0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"11eefd7e7dc86c1755a8db4c6825e6e9fdeb6d39","datavalue":{"value":{"entity-type":"item","numeric-id":3619797,"id":"Q3619797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$E8187053-64F1-4EA1-AD86-56E1FA1B4790","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd8a75b14ef6584f98a6f5cd1f51da6af90626a7","datavalue":{"value":{"entity-type":"item","numeric-id":4727425,"id":"Q4727425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$0CE9585D-501C-4765-B63C-F524D4AA0C5E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca6926d9a2864657c63c8ba6d81f03198b036942","datavalue":{"value":{"entity-type":"item","numeric-id":1595929,"id":"Q1595929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$3B42AFA9-D5FD-4250-B619-BA136FF971C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f7396a7d7693b676318207b9fce821ae1fe747e9","datavalue":{"value":{"entity-type":"item","numeric-id":1425160,"id":"Q1425160"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$9E0F91C7-202C-4556-940A-EADC7D8AAA36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b00ea8dcddd12b85e22417f7ab71b67ef496b153","datavalue":{"value":{"entity-type":"item","numeric-id":2917406,"id":"Q2917406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$A4F26BF0-1D41-4A74-971B-7E692E1251BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f9118593b08e77c318c68fff0f50123d05f6233","datavalue":{"value":{"entity-type":"item","numeric-id":931433,"id":"Q931433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$D58D3439-6D80-4CAA-A42E-3E0DD85C8ADA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f588e1f20f8fac4f68de33144bd2608b46fa9a8","datavalue":{"value":{"entity-type":"item","numeric-id":1898211,"id":"Q1898211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q437040$D3CD946D-65B5-4AC3-9630-D8C88F4D4B88","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"52688f4c7f66e485b93dffbf6b2644fff3310045","datavalue":{"value":"10.1007/S10817-010-9206-X","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q437040$FF2BDFB4-D8EE-45F3-97F1-DA0E3C305E21","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1f963f62b22b753f06f0ea6d6bbdfb2badc996c3","datavalue":{"value":{"entity-type":"item","numeric-id":5747642,"id":"Q5747642"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8f3f01f021c500e1dc24d1b799b368f9480456da","datavalue":{"value":{"amount":"+0.8713434934616089","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":"Q437040$04323BB7-A23D-421D-8171-83DA7EC7B6C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b959c4faa8a54faa6d15d5b3b0763f8be0c197b6","datavalue":{"value":{"entity-type":"item","numeric-id":3455563,"id":"Q3455563"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d4e339ccfdda4f6ee27ffd648401804c814ae84","datavalue":{"value":{"amount":"+0.7985174655914307","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":"Q437040$4EB9F696-00A1-4367-BD36-4ECB45046457","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e6f30fb825b322b9b5a869ec9f046aa8f49eb8d5","datavalue":{"value":{"entity-type":"item","numeric-id":4727425,"id":"Q4727425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"52e4e01f3d7636995ccbcf9b7646ba30251ad9aa","datavalue":{"value":{"amount":"+0.7899463176727295","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":"Q437040$8B1D7503-D7C7-494F-91DB-D003F0B3ECFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ae27fbf047d7fb1d9e041fa35e830eb089b91dbc","datavalue":{"value":{"entity-type":"item","numeric-id":4327423,"id":"Q4327423"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e668a7dec7b144b21ae6644a2aba419f1eec9ed3","datavalue":{"value":{"amount":"+0.7460037469863892","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":"Q437040$F74A6823-8C16-4C81-9A67-1613C647BEE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f804cf18159ddb207bf79069e1cdbb9160b6a7c1","datavalue":{"value":{"entity-type":"item","numeric-id":580970,"id":"Q580970"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e4c4f8a310db63ba6dc57d0aaed5e31cd6609cab","datavalue":{"value":{"amount":"+0.7434320449829102","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":"Q437040$DD3EBF63-FB6B-4A58-989F-BEFA1700B2F9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof pearl: a formal proof of Dally and Seitz' necessary and sufficient condition for deadlock-free routing in interconnection networks","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_pearl:_a_formal_proof_of_Dally_and_Seitz%27_necessary_and_sufficient_condition_for_deadlock-free_routing_in_interconnection_networks"}}}}}