La definizione alternativa del preordine di must non è così diretta come la precedente: abbiamo bisogno di alcune premesse per poter proseguire:
Tramite queste premesse, possiamo introdurre la caratterizzazione alternativa di must:
se , con finito, implica:
Il vantaggio di questa diversa caratterizzazione è che la sequenza di azioni interessanti sono un numero finito e quindi la prova si riduce drasticamente in quanto per ogni sequenza non interessante si ha che (P after x)= , come mostra il seguente
( ) Supponiamo che Traces(P). Allora sappiamo che esiste un tale che e per nessun si ha che e quindi si ha che (P after s) not must.
Morpheus 2004-02-10