The soundness of the proposed algorithm is stated below. The proof is given in Appendix A.

That is, the theorem guarantees that the Q-DAG nodes generated by the
algorithm will always evaluate to their corresponding probabilities under
any partial or full instantiation of evidence variables.

Darwiche&Provan