for s being State of SCM+FSA
for d being Int-Location holds d in dom s