Martin has written essentially everything that had to be written. Let me just add how you have to read the function "CreateNode" which is called in the BDD algorithms at the end. By the name, it suggests to just create a node, however, as revealed later in the chapter, currently on slide 112, you can see that first it checks whether such a node already exists by inspecting a unique table. That is very important to make BDDs work correctly. Clearly, if such a node does exist, it is reused, otherwise a new one has to be created.