La dimostrazione della correttezza e della completezza del metodo di negazione esposto si ottiene facilmente facendo riferimento alle corrispondenti proprietà della negazione intensionale e della negazione costruttiva di Chan.
La correttezza si ottiene considerando che, data la partizione dei predicati fornita dal criterio, ad uno dei due sottoinsiemi viene applicata la NI, corretta per la classe di programmi considerata, mentre l'altro viene trattato lasciando indicata la negazione che, a tempo di esecuzione, viene risolta con la negazione costruttiva di Chan, corretta per alberi di derivazione finiti.
La completezza deriva dal fatto che, per quei predicati che il criterio giudica non terminanti, si può senz'altro applicare la NI, dimostrata completa per la classe di programmi considerata.
L'ipotesi che il programma sia stratificato non riguarda la correttezza e la completezza del metodo in generale, ma è una condizione che viene sfruttata dal criterio sulla terminazione proposto. Il metodo naturalmente può essere modificato applicando una qualunque altra tecnica che testi la terminazione di programmi logici, secondo il grado di precisione dello studio desiderato in relazione al reale utilizzo del programma.