# BDD2FDD, clarification in solving certain terms

I am  not able to figure out how the below terms marked in red are solved. I understood the algorithm but I am not able to figure out these below terms in red. Could you please explain this? (2022.02 Paper)

(0 ⊕ b ∧ 1) ⊕ a ∧ Apply(⊕,(0 ⊕ b ∧ BDD2FDD(n0)),(0 ⊕ b ∧ 1)

(0 ⊕ b ∧ 1) ⊕ a ∧ (0 ⊕ b ∧ Apply(⊕,(BDD2FDD(n0)), 1)

(0 ⊕ b ∧ 1) ⊕ a ∧ (0 ⊕ b ∧ Apply(⊕,(0 ⊕ c ∧ 1), 1)

(0 ⊕ b ∧ 1) ⊕ a ∧ (0 ⊕ b ∧ (1 ⊕ c ∧ (1 ⊕ 0)))

(0 ⊕ b ∧ 1) ⊕ a ∧ (0 ⊕ b ∧ (1 ⊕ c ∧ 1)

+1 vote

You have to consider the function BDD2FDD and also the Apply algorithm to understand the single steps. Indeed, the computation of the example solution has some unclarities which should be better explained here:

```    BDD2FDD(n3)
= BDD2FDD(n2) ⊕ a ∧ Apply(⊕, BDD2FDD(n1), BDD2FDD(n2))
// BDD2FDD(n2) = BDD2FDD(b) = (0⊕b∧1)
= (0⊕b∧1)⊕a∧Apply(⊕,BDD2FDD(n1),(0⊕b∧1))
// BDD2FDD(n1) = 0⊕b∧BDD2FDD(n0)
= (0⊕b∧1)⊕a∧Apply(⊕,(0⊕b∧BDD2FDD(n0)),(0⊕b∧1))
// Apply(⊕,(0⊕b∧BDD2FDD(n0)),(0⊕b∧1)) ```
```    = (0⊕0)⊕b∧Apply(⊕,BDD2FDD(n0),1)
= (0⊕b∧1)⊕a∧(0⊕b∧Apply(⊕,(BDD2FDD(n0)),1))
// BDD2FDD(n0) = 0⊕c∧1
= (0⊕b∧1)⊕a∧(0⊕b∧Apply(⊕,(0⊕c∧1),1))
// Apply(⊕,(0⊕c∧1),1) = (0⊕1)⊕c∧1
= (0⊕b∧1)⊕a∧(0⊕b∧(1⊕c∧1))```
by (142k points)