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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

FMutex

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

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

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

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

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

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

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