Diskuse:

Mějme proces , splňující . Aplikujme na něj výše uvedený algoritmus TransformujProces, P, , . Jelikož uvažujeme pouze konečné přechodové systémy jako procesy, můžeme předpokládat |Q|=n, pro nějaké . Výpočet tohoto algoritmu zřejmě skončí ve chvíli, kdy (to určitě nastane, neboť v každém kroku se do přidá prvek), a vrátí systém CCS jakožto množinu definic popisujících proces .