Have a look at the code of the Apply algorithm: When being called for two nodes a and b and some operation op, it inspects first the variables v_a and v_b in the labels of the root nodes of the given BDDs. The maximum of them becomes the label of the new root node, and the two children are computed by recursive calls of the Apply algorithm. The arguments of these recursive calls are determined by three cases:
- v_a = v_b : low = Apply(op,low(a),low(b)) and high = Apply(op,high(a),high(b))
- v_a < v_b : low = Apply(op,a,low(b)) and high = Apply(op,a,high(b))
- v_a > v_b : low = Apply(op,low(a),b) and high = Apply(op,high(a),b)
The result BDD is then (max(v_a,v_b) ? high : low), but before creating such a new node, we check whether it already exists. Does this help? You may also check slide 103 for a one page description of the algorithm covering all cases.