Define the Huffman binary encoding procedure and prove its optimality among decipherable codes.