{"entities":{"Q839031":{"pageid":840879,"ns":120,"title":"Item:Q839031","lastrevid":64724319,"modified":"2026-04-11T21:48:12Z","type":"item","id":"Q839031","labels":{"en":{"language":"en","value":"Proof pearl: Mechanizing the textbook proof of Huffman's algorithm"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5600745"}},"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":"Q839031$312281DE-C420-4F6D-91C0-20905B35EC76","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8e04aef280a77986709869d2355e8fb65ea1f847","datavalue":{"value":{"text":"Proof pearl: Mechanizing the textbook proof of Huffman's algorithm","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q839031$B7258B5B-6E13-440B-BCB1-1925B82D826E","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c719708f34003da6bddfb2fd782bf22bc9748a44","datavalue":{"value":"1187.68523","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839031$22EB3FC3-FD02-406E-A875-414B4BC94D98","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"42c29c686dffd678d9f155b05a4a1aa93e85953c","datavalue":{"value":{"entity-type":"item","numeric-id":287335,"id":"Q287335"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839031$F4688418-338C-4DD7-885A-5F9F8B3CBB21","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":"Q839031$EDC7DCDA-1474-4432-B4C4-E734F55C3CD8","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cb4a7b11cbf8a3591d56dfc973401a20f55cc386","datavalue":{"value":{"time":"+2009-09-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q839031$627A5CB1-7A03-45E3-A84B-C87F98A4B9BC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839031$A96A659F-D7B8-4E13-B098-5B088AF5F5AE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"74c4af807e83b8d9190366644e977245c580e2cf","datavalue":{"value":"5600745","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839031$0CED8DD4-03C0-489F-AD35-C522FD7E9738","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c32d9a0804c50fc70d2c7cdb6acd844d7d1106fc","datavalue":{"value":"Huffman coding","type":"string"},"datatype":"string"},"type":"statement","id":"Q839031$F685CA96-5817-4376-965B-56B804EF20B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"82db2410f7cb36b26154919ad626ca1e681d8b2b","datavalue":{"value":"interactive theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q839031$CDCA8EAE-D82F-427A-887D-2E6D25E91ED2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q839031$75DC7FCD-C71A-465D-9896-1DE51BA17215","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":"Q839031$982D98DB-4C92-4DCB-B102-F85823BDDEC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a2db887ae3c9f1131cefea2f0ad9b0ef81409f14","datavalue":{"value":{"entity-type":"item","numeric-id":43929,"id":"Q43929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839031$884C9D2B-A288-43A0-92AB-FA9CF38FF2CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839031$3BED8EC8-049D-4C81-AE55-EA3EFF171C05","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":"Q839031$CF799F47-5D83-4119-9B19-010619BA5334","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":"Q839031$B9FE5BAE-AB55-4E80-9A51-A859D518D4E4","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":"Q839031$54ECD794-8AFB-479D-9686-29E4820EB7F2","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":"Q839031$4B988C77-666F-4B2B-B693-758B3114BBE7","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"01d5e2bae8c1f4a547571d2c6741b73a2bf08c80","datavalue":{"value":"https://doi.org/10.1007/s10817-009-9116-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q839031$A33AFC59-BE59-499E-B25B-2C039086F564","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f198b7a3a86ff90672aba515a8755b1093c531da","datavalue":{"value":"W2026960838","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839031$BC517E07-029C-486E-9F3B-B41633FFDB90","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b59b9a95c5ede48fa66f5efb685b30e863d99e05","datavalue":{"value":{"entity-type":"item","numeric-id":3948568,"id":"Q3948568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839031$F5EE0C5B-819A-4BC2-B925-5D4152CF1EF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d7aea7368304c81d99f05a85147c94cac452455e","datavalue":{"value":{"entity-type":"item","numeric-id":3523164,"id":"Q3523164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839031$BEC90263-FB08-4EB5-9752-7C07ED33BF79","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bffe48c7c76b90bf68970921698e19786e1600b","datavalue":{"value":{"entity-type":"item","numeric-id":2747613,"id":"Q2747613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839031$0E33716B-67B7-4D0C-BC54-CAA4A7625F73","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839031$EA418172-A3C7-4F4D-A9C8-2E3539B00314","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f51ab68fb93638e8648c08fc21c5c749fc87f3e4","datavalue":{"value":{"entity-type":"item","numeric-id":5510070,"id":"Q5510070"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839031$33987B13-E74B-4EB5-B8FD-3F2216B0F5A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a634cbc29683300650d9989a01808c0a4931ead5","datavalue":{"value":{"entity-type":"item","numeric-id":4398780,"id":"Q4398780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q839031$20C5C822-8F23-48CF-871E-5B28CEE361A3","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":"Q839031$B80B52AB-1975-4DF7-9922-B7DA369EE261","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1430224fa2b7a5387c09c503be432fc8cda5ae76","datavalue":{"value":"10.1007/S10817-009-9116-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q839031$10C505EB-0EAA-41C2-B70B-F5535564237E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f8b1e3ed7dab842dacd71719cef2cea62e1e29d6","datavalue":{"value":{"entity-type":"item","numeric-id":467784,"id":"Q467784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e096ba4e661831a2085e33ab35dac39b4e573e9","datavalue":{"value":{"amount":"+0.7279680967330933","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":"Q839031$90931C70-F45F-4C75-8133-C767CC2707EB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4f2cc416bb905f6cc671d100374ad7a999ffcbf2","datavalue":{"value":{"entity-type":"item","numeric-id":2351394,"id":"Q2351394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"86da627a3a1f2aa46481e43b0c4cd20e40cd6709","datavalue":{"value":{"amount":"+0.7135844826698303","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":"Q839031$48A31529-3E9A-42F8-95D4-E86670F2F40C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a5901dc64ead168a4c5d4245da43e96c8a67c047","datavalue":{"value":{"entity-type":"item","numeric-id":5670536,"id":"Q5670536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88050459d60e2c0c691b7c2f65d91e33970737bc","datavalue":{"value":{"amount":"+0.7101395130157471","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":"Q839031$41260A51-330A-4118-B5C5-E7D79720E56F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3e76e89983f49dd3b61e5343eea6b5b3c4bdadcd","datavalue":{"value":{"entity-type":"item","numeric-id":1567200,"id":"Q1567200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d89cf562838d5141f31b00379afb246a4711741e","datavalue":{"value":{"amount":"+0.7027180194854736","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":"Q839031$5B3D18D2-4C87-48CB-9F8D-8D7FDBEAF684","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe229241ec597fb6bcb1e635ce0c2f30adb11d28","datavalue":{"value":{"entity-type":"item","numeric-id":3219102,"id":"Q3219102"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"933dac9b586f5d960e8c09ed702e9a6b7c9028f3","datavalue":{"value":{"amount":"+0.6998165249824524","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":"Q839031$32D587B8-CE41-4C7D-A7E2-79F7B7F8351F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proof pearl: Mechanizing the textbook proof of Huffman's algorithm","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proof_pearl:_Mechanizing_the_textbook_proof_of_Huffman%27s_algorithm"}}}}}