Completezza dell'assiomatizzazione

Teorema 7..6 (Completezza)   Dati due processi P e Q tali che $P \simeq_{test}Q$, allora questo implica ${\bf (A1)}-{\bf (N4)}\vdash P=Q$.

Dimostrazione. (Traccia) Supponiamo che P e Q siano in forma normale (nel caso non lo fossero, abbiamo già mostrato che è possibile trasformarli in processi equivalenti ma in n.f.). Allora avremo $P=Q$ se ogni sommando in P è presente anche in Q.

Supponiamo, per assurdo, che P abbia un sommando che Q non ha, allora per la saturazione delle forme normali avremmo un insieme $L$ tale che $P$ must $L$ ma $Q$ not must $L$ che porta all'assurdo $P \not\simeq_{test} Q$. $\qedsymbol$

Si ha inoltre che

Teorema 7..7   $P \sqsubseteq_{may}Q$ implica ${\bf (A1)}-{\bf (N4)}-{\bf (F1)}\vdash P \sqsubseteq Q$

di cui non forniremo una dimostrazione.