- Auxiliary functions and theorems
- Uniqueness of keys in association lists
- Frequency lists from messages and some of their properties
- Codes as association lists and some of their properties
- Ordered lists and their properties
- Sorting by insertion and its correctness
- Weights of encodings
- Binary trees and some of their properties
- Tree covers and their properties
- Ordered covers and some of their properties
- Weights of binary trees
- Properties of products between an integer list and a list of trees
- A predicate for relating a height list with a cover
- Tree substitutions with respect to a cover
- Minimal trees for a cover
- Equality of sum leaves
- One step of the building process (merging the smallest tree)
- Build process to iteratively merge two smaller trees
- Partial binary trees (nodes having up to 2 sons)
- Translation from partial trees to binary trees
- Restriction of a code (only the keys of a message appears)
- The Huffman algorithm and its correctness