Inductive step \((l \rightarrow l+1)\)
Case 1: The node (u, ∅) was added to S because of the ∨-gate \(u \in V \cup \overline {V}\).
W.l.o.g. let u ∈ V. Let v be d-node(u) in T and let p be a shell restriction w.r.t. v such that \(u\in R(\mathcal {D}_{p},v)\). The sets \(R^{+}(\mathcal {D}_{p},v)\) and \(R^{+}(\overline {\mathcal {D}}_{p},v)\) contain only ∧-gates because of the definition of the sets, \(\mathcal {D}\) and \(\overline {\mathcal {D}}\) being simple, and the fact that vars(v) contains at least three variables. Therefore, u is not in \(R^{+}(\mathcal {D}_{p},v)\) but the child nodes of u are in the set.
The node (u, ∅) is an ∨-gate which is connected to every ∧-gate \((u,u^{\prime })\) for \(u^{\prime } \in R^{+}(\mathcal {D}_{p},v) \cup R^{+}(\overline {\mathcal {D}}_{p},v)\). These ∧-gates are connected to further nodes \((u^{\prime },\emptyset )\) and (u,⊤) for \((u,u^{\prime })\in E\) or (u,⊥) otherwise. Thus, S(u, ∅) is inductively defined. Now, our aim is to show that S(u, ∅) is a syntactically correct SDD respecting the subtree rooted at node(u) in \(T^{\prime }\) that represents fu. For this reason, we prove that the subgraphs rooted at \((u^{\prime },\emptyset )\) in S are syntactically correct SDDs w.r.t. the subtree \(T^{\prime }_{\text {node}({u^{\prime }})}\) which represent \(f_{u^{\prime }}\) for \(u^{\prime }\in V\) or \(\overline {f}_{u^{\prime }}\) for \(u^{\prime }\in \overline {V}\). Moreover, we have to show that they represent Boolean functions which form a partition.
The subgraph \(S_{(u^{\prime },\emptyset )}\) has at most depth l − 1 for each \(u^{\prime } \in R^{+}(\mathcal {D}_{p},v) \cup R^{+}(\overline {\mathcal {D}}_{p},v)\) because by assumption S(u, ∅) is a subgraph of depth at most l + 1 and (u, ∅) is connected to each \((u^{\prime }, \emptyset )\) by a path of length two. Thus, by the use of the inductive hypothesis \(S_{(u^{\prime }, \emptyset )}\) is a syntactically correct SDD w.r.t. the subtree rooted at \(\text {node}({u^{\prime }})\) in \(T^{\prime }\). We know that \(\text {d-node}({u^{\prime }})=\text {d-node}({u})=v\) since the given structured d-DNNFs are smooth. Moreover, \(S_{(u^{\prime }, \emptyset )}\) represents the function \(f_{u^{\prime }}\) for \(u^{\prime }\in V\) or \(\overline {f}_{u^{\prime }}\) for \(u^{\prime }\in \overline {V}\).
S(u,⊥) and S(u,⊤) are SDDs representing ⊥ and ⊤, respectively. Therefore, they respect the right subtree of \(T_{v^{\prime }}\), a leaf labeled by an auxiliary variable, where \(v^{\prime }\) is the parent of v in \(T^{\prime }\). Therefore, S(u, ∅) respects \(T_{v^{\prime }}\).
By induction hypothesis we know that \(S_{(u^{\prime }, \emptyset )} = f_{u^{\prime }}\) for each \(u^{\prime } \in R^{+}(\mathcal {D}_{p},v)\) and \(S_{(u^{\prime }, \emptyset )} = \overline {f}_{u^{\prime }}\) for each \(u^{\prime } \in R^{+}(\overline {\mathcal {D}}_{p},v)\). Using Proposition 3 and the fact that the given structured d-DNNFs are simple, we can conclude that all functions \(S_{(u^{\prime }, \emptyset )}\) for \(u^{\prime }\in R^{+}(\mathcal {D}_{p},v) \cup R^{+}(\overline {\mathcal {D}}_{p},v)\) form a partition.
Finally, we get the equivalence of S(u, ∅) and fu by applying the inductive hypothesis on \(S_{(u^{\prime }, \emptyset )}\) for each \(u^{\prime } \in R^{+}(\mathcal {D}_{p},v) \cup R^{+}(\overline {\mathcal {D}}_{p},v)\).
$$ \begin{array}{@{}rcl@{}} S_{(u, \emptyset)} &=& \bigvee\limits_{{\substack{u^{\prime} \in R^{+}(\mathcal{D}_{p},v), \\ (u,u^{\prime}) \in E}}} (S_{(u^{\prime}, \emptyset)} \wedge S_{(u,\top)}) \vee \bigvee\limits_{{\substack{u^{\prime} \in R^{+}(\mathcal{D}_{p},v) \\ (u,u^{\prime}) \notin E}}} (S_{(u^{\prime}, \emptyset)} \wedge S_{(u,\bot)}) \vee \bigvee\limits_{{u^{\prime} \in R^{+}(\overline{\mathcal{D}}_{p},v)}} (S_{(u^{\prime}, \emptyset)}\wedge S_{(u,\bot)}) \\ &=& \bigvee\limits_{\substack{u^{\prime} \in R^{+}(\mathcal{D}_{p},v), \\ (u,u^{\prime}) \in E}} (S_{(u^{\prime}, \emptyset)} \wedge \top) \vee \bigvee\limits_{\substack{u^{\prime} \in R^{+}(\mathcal{D}_{p},v), \\ (u,u^{\prime}) \notin E}} (S_{(u^{\prime}, \emptyset)} \wedge \bot) \vee \bigvee\limits_{u^{\prime} \in R^{+}(\overline{\mathcal{D}}_{p},v)} (S_{(u^{\prime}, \emptyset)} \wedge \bot) \\ &=& \bigvee\limits_{\substack{u^{\prime} \in R^{+}(\mathcal{D}_{p},v), \\ (u,u^{\prime}) \in E}} (S_{(u^{\prime}, \emptyset)} \wedge \top) = \bigvee\limits_{(u,u^{\prime}) \in E} S_{(u^{\prime}, \emptyset)} \overset{\text{(ind.)}}{=} \bigvee\limits_{(u,u^{\prime}) \in E} f_{u^{\prime}} = f_{u} \end{array} $$
Case 2: The node (
u,
∅) was added to
S because of the ∧-gate
\(u \in V \cup \overline {V}\).
W.l.o.g. let u ∈ V. Furthermore, let uℓ and ur be the left and right child of u. Let v be d-node(u) in T and vℓ be the left child of v in T. Furthermore, let p be a shell restriction w.r.t. vℓ for which there exists an assignment \(r^{\prime }\) to the remaining variables such that there is a 1-certificate in \(\mathcal {D}\) for the joint assignment \(p+r^{\prime }\) to the x-variables that contains the node uℓ. Moreover, let \(R^{++}(\mathcal {D}_{p}, v_{\ell })\) contain all nodes from \(R^{+}(\mathcal {D}_{p}, v_{\ell })\) without uℓ or any child node of uℓ.
The node (u, ∅) is connected to the ∧-gate (u,∧) and to all ∧-gates \((u,u^{\prime })\) for \(u^{\prime }\in R^{++}(\mathcal {D}_{p}, v_{\ell })\cup R^{+}(\overline {\mathcal {D}}_{p}, v_{\ell })\). The node (u,∧) is connected to (uℓ,∅) and (ur,∅), the other ∧-gates are connected to \((u^{\prime },\emptyset )\) and (u,⊥).
S(u,⊥) represents the function ⊥ and is an SDD w.r.t. any vtree. The subgraphs \(S_{(u_{\ell },\emptyset )}\), \(S_{(u_{r},\emptyset )}\), and \(S_{(u^{\prime },\emptyset )}\) have at most depth l − 1 because by assumption S(u, ∅) is a subgraph of depth at most l + 1 and (u, ∅) is connected to the nodes by paths of length two. Thus, by the use of the inductive hypothesis \(S_{(u_{\ell }, \emptyset )}\), \(S_{(u_{r},\emptyset )}\), and \(S_{(u^{\prime },\emptyset )}\) are syntactically correct SDDs w.r.t. subtrees rooted at node(uℓ), node(ur), and \(\text {node}({u^{\prime }})\), respectively, in \(T^{\prime }\). Moreover, node(uℓ) and \(\text {node}({u^{\prime }})\) are in the left subtree of v and node(ur) is in the right subtree of v. The subgraph S(u,∧) represents the conjunction of the functions represented at \(S_{(u_{\ell },\emptyset )}\) and \(S_{(u_{r},\emptyset )}\) and S(u, u) represents the conjunction of \(S_{(u^{\prime },\emptyset )}\) and S(u,⊥). Therefore, S(u,∧) and \(S_{(u^{\prime },\emptyset )}\) respect v in \(T^{\prime }\) and as a consequence also S(u, ∅) respect v.
If uℓ is an ∧-gate, \(u_{\ell }\in R^{+}(\mathcal {D}_{p},v_{\ell })\). Therefore, the set of gates \(u_{\ell } \cup R^{++}(\mathcal {D}_{p},v_{\ell })\) is equal to \(R^{+}(\mathcal {D}_{p},v_{\ell })\). We know that \(R^{+}(\mathcal {D}_{p}, v_{\ell })\cup R^{+}(\overline {\mathcal {D}}_{p}, v_{\ell })\) form a partition because of Proposition 3 and \(\mathcal {D}\) being simple. By the induction hypothesis the same holds for the functions represented by \(S_{(u_{\ell },\emptyset )}\) and \(S_{(u^{\prime },\emptyset )}\) for \(u^{\prime }\) in \(R^{++}(\mathcal {D}_{p}, v_{\ell })\cup R^{+}(\overline {\mathcal {D}}_{p}, v_{\ell })\). If uℓ is an ∨-gate, the function represented at uℓ is the disjunction of the functions represented at the child nodes of uℓ. Because of Proposition 2 and \(\mathcal {D}\) being simple we know that all functions represented at a node in \(\{u_{\ell }\} \cup R^{++}(\mathcal {D}_{p}, v_{\ell })\) are mutually disjoint. The disjunction of these functions is equal to fA, p where A = shell(vℓ). Now, because of Proposition 3 and \(\mathcal {D}\) as well as \(\overline {\mathcal {D}}\) being simple we can conclude that all functions represented at a node \(\{u_{\ell }\} \cup R^{++}(\mathcal {D}_{p}, v_{\ell })\cup R^{+}(\overline {\mathcal {D}}_{p}, v_{\ell })\) form a partition. By the induction hypothesis the same holds for the corresponding functions in S.
Finally, we get the equivalence of S(u, ∅) and fu by applying the inductive hypothesis on \(S_{(u_{\ell }, \emptyset )}\) and \(S_{(u_{r}, \emptyset )}\).
$$ \begin{array}{@{}rcl@{}} S_{(u, \emptyset)} &=& (S_{(u_{\ell}, \emptyset)} \wedge S_{(u_{r},\emptyset)}) \vee \bigvee\limits_{u^{\prime} \in R^{++}(\mathcal{D}_{p},v_{\ell})} (S_{(u^{\prime}, \emptyset)} \wedge S_{(u,\bot)}) \vee \bigvee\limits_{u^{\prime} \in R^{+}(\overline{\mathcal{D}}_{p},v_{\ell})} (S_{(u^{\prime}, \emptyset)}\wedge S_{(u,\bot)}) \\ &=& (S_{(u_{\ell}, \emptyset)} \wedge S_{(u_{r},\emptyset)}) \vee \bigvee\limits_{u^{\prime} \in R^{++}(\mathcal{D}_{p},v_{\ell})} (S_{(u^{\prime}, \emptyset)} \wedge \bot) \vee \bigvee\limits_{u^{\prime} \in R^{+}(\overline{\mathcal{D}}_{p},v_{\ell})} (S_{(u^{\prime}, \emptyset)}\wedge \bot) \\ &=& (S_{(u_{\ell}, \emptyset)} \wedge S_{(u_{r},\emptyset)}) \overset{\text{(ind.)}}{=} f_{u_{\ell}} \wedge f_{u_{r}} = f_{u} \end{array} $$