C2 (as on slide 26 on the solutions) is defined as (b⇒1|(a⇒0|1). Now you might have two questions:
1. Why is (b⇒1|(a⇒0|1) the correct result of ITE(0,A3,A2)? As “0” is a unsatifiable, the result of the If-Then-Else-call will always depend precisely on the Else-branch, which is A2. This case is also shown on slide 20 of the solutions, left most column, lower entry. On slide 22, we defined A2 as (b⇒1|(a⇒0|1).
2. Why do we call it C2? That's a bit confusing. BDD packages (for example our online teaching tools, please play with them!) would just return the pointer of the existing (sub-)BDD. Here, A2, B2, and C2 are by coincidence the same (sub-)BDD. However, for easy navigation between the slides, we labeled everything on slide 22 starting with A, on slide 23 starting with B, and on slide 25 starting with C. That's why it switches names.
(A similar phenomenon can be observed on the following line in the solutions ITE(B1,A3,A2) = (b ? ITE(1, A1,1) : ITE(0,1,A1)) = (b ? C1 : C1) = C1 The second and third ITE-call of this line depend on constants. In both cases, the result is A1. We immediately rename it to C1. Note that in all cases it is a mere coincidence that after renaming the nodes, they indices stay the same.)
