be an ordering of  (  ), where  1 and  2 are ma  blocks, mutuall  independent and cn e ual under the bindings of  ( )    . Then   N is blockwise e uivalent with 2 l Proof:
be a minimal ordering of  o binder consistent with   N .

orollar     does not O'N
violate the blocks of N, in particular , 1 and , 2 l
... et 2 ON
e must show that    is minimal, which implies blockwise e uivalence of 2 l N and . N
If   is empt , then 
( ) b    emma   (  1 and   2 are ad acent, mutuall independent and cn e  ual  thus, their transposition does not change the cost).

If is not empt , then b   orollar      is mutuall  independent of both      and is binder consistent with  N , therefore  (  )
( )
can be divided into several blocks, each one of them cn e ual to 1 and 2 since is minimal, N cannot be contradicting, and the claim follows from emma 1 .

emma 9, .  ( ) x
(1) x emma
( 2) x

$\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ $\left(\begin{array}{ccccc}\end{array}\right)$ \(\left(\begin{array}{ccccc}\end{array}\right)
inimalit  of   implies blockwise e uivalence of   N and N

$$\square$$

## Appendix B. Correctness Of The Dac Algorithm

In this section we show that the DAC algorithm is correct, i.e., given a set of subgoals 0, it returns its minimal ordering. It su ces to show that the candidate set of the root node of
( o ) is valid. In such a case, as follows from the definition of valid sets, it must contain a minimal ordering. The algorithm returns one of the cheapest candidates of the root. Therefore, if the candidate set of the root is valid, the DAC algorithm must return a minimal ordering of  o.

e start b  defining strong validity of sets of orderings.    e then prove that strong validit implies validit . inall , we use induction to prove a theorem, showing that the candidate set produced for each node in the divisibilit tree is strongl valid.

Definition:  et  o be a set of subgoals,    be a node in the divisibilit  tree of  o. The set
( )) is strongly valid, if ever ordering in ( ( )) CN is either    contradicting CN
or blockwise e uivalent to some member of CN, unless no ordering of  (  ) is min consistent.

$\begin{array}{ccccccccc}&&N_{\mathcal{S}_{0}}\left(\mathcal{C}_{N}\right)&&&&\\ \exists&_{N}&(&(&))&&_{N_{\mathcal{S}_{1}}}(&_{N})\rightarrow&_{N}&(&(&))&\mathcal{C}_{N}\rightarrow&_{N_{\mathcal{S}_{0}}}(&_{N})\\ &&&&&&&&(\exists&_{N}&\mathcal{C}_{N}&&_{N_{\mathcal{S}_{0}}}(&_{N}&_{N}))\end{array}$  **Lemma 11**: _A strongly valid set of orderings is valid._