{"entities":{"Q43929":{"pageid":43985,"ns":120,"title":"Item:Q43929","lastrevid":105429395,"modified":"2026-10-09T10:11:56Z","type":"item","id":"Q43929","labels":{"en":{"language":"en","value":"Huffman"}},"descriptions":{"en":{"language":"en","value":"AFP entry Huffman"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"152a75f714d315a4326095f8d9d55030402bdd16","datavalue":{"value":"32218","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43929$DA92317A-0EF5-4D1B-9D8E-B3AEAE00C811","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":"Q43929$E7E61765-0BC7-4297-A318-6341BE3B94B8","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"e9f40411d7a12b0564285545427072e796f97a25","datavalue":{"value":"https://www.isa-afp.org/entries/Huffman.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43929$FB36D190-7AD7-4822-A880-1352DD5185A3","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q43929$DFA6A75C-84D7-4178-958E-E55E271D93F2","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":"Q43929$10F90BE1-BB33-4145-9E54-A3E54D612B8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43929$F39306F3-8D48-484B-97D0-3BE0D6F33416","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":"Q43929$E2336E8E-9BC1-4867-A6B0-5287C0C09852","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ff80b41d03c65073c007c903a317be0a9c94293e","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43929$664FF052-36FA-4CE0-81D6-CACE7A971D6B","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":"Q43929$12CCF916-4499-43C1-A6F4-D4A05D703177","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ffcef6969153f616dfc5a0ee2edecbd991c42f53","datavalue":{"value":"https://isa-afp.org/entries/Huffman.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q43929$26D71FA7-2524-4D55-B857-433496693846","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"d593b6f197721b1ecf9f17d8e5bbb2bb5a1f7f8a","datavalue":{"value":"Jasmin Christian Blanchette","type":"string"},"datatype":"string"},"type":"statement","id":"Q43929$A43AE8DD-55EF-4A64-BCAC-1B27709E608D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"d6f6926c6d4d51ec34748f09f78e5885db1a5b5d","datavalue":{"value":"Huffman's algorithm is a procedure for constructing a binary tree with minimum weighted path length. This report presents a formal proof of the correctness of Huffman's algorithm written using Isabelle/HOL. Our proof closely follows the sketches found in standard algorithms textbooks, uncovering a few snags in the process. Another distinguishing feature of our formalization is the use of custom induction rules to help Isabelle's automatic tactics, leading to very short proofs for most of the lemmas.","type":"string"},"datatype":"string"},"type":"statement","id":"Q43929$47F0A59E-3772-4EA4-8725-F65780006706","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"67016f8e809472ef1c8b390819b02053dfb97c8d","datavalue":{"value":{"time":"+2008-10-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q43929$22B546BE-0813-463A-A2BD-7B9F5F34E30F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9826e9519869075fb1d6daa3c20a8e76091dae0f","datavalue":{"value":{"text":"The Textbook Proof of Huffman's Algorithm","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q43929$762657EA-2390-430F-925C-7115FEC977F3","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":"Q43929$667AAA02-3EFA-4BBA-A9A9-4781A31FB736","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"ef7bddd24a035fe32f48fd95ea6033928a9b8e67","datavalue":{"value":{"entity-type":"item","numeric-id":7360788,"id":"Q7360788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q43929$E2222D3C-243A-4A93-AFFB-3D3261BE9A58","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Huffman","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Huffman"}}}}}