3.3.7 Correttezza e completezza di SLDCNF per alberi finiti

Chan ha dimostrato il seguente teorema

Teorema 3.6  

Se l'albero di derivazione SLDCNF con radice $\leftarrow Q = \leftarrow L_{1}, \ldots, L_{m}$ è finito e contiene k rami di successo con risposte $A_{1}, \ldots, A_{k}$ allora

$$\forall (Q \equiv ( \exists A_{1} \vee \ldots \vee \exists A_{k}))$$