Mutex2

--- tau ---> ((User | v.Sem) | enter.exit.'v.User)\{p,v}
--- tau ---> ((enter.exit.'v.User | v.Sem) | User)\{p,v}

((User | v.Sem) | exit.'v.User)\{p,v}

--- exit ---> ((User | v.Sem) | 'v.User)\{p,v}

((exit.'v.User | v.Sem) | User)\{p,v}

--- exit ---> (('v.User | v.Sem) | User)\{p,v}

((User | v.Sem) | 'v.User)\{p,v}

--- tau ---> ((User | Sem) | User)\{p,v}

(('v.User | v.Sem) | User)\{p,v}

--- tau ---> ((User | Sem) | User)\{p,v}

((User | Sem) | User)\{p,v}

--- tau ---> ((User | v.Sem) | enter.exit.'v.User)\{p,v}
--- tau ---> ((enter.exit.'v.User | v.Sem) | User)\{p,v}

((User | v.Sem) | enter.exit.'v.User)\{p,v}

--- enter ---> ((User | v.Sem) | exit.'v.User)\{p,v}

((enter.exit.'v.User | v.Sem) | User)\{p,v}

--- enter ---> ((exit.'v.User | v.Sem) | User)\{p,v}