theorem Th1: :: SCMFSA_M:1

for s being State of SCM+FSA
for x being set holds
( not x in dom s or x is Int-Location or x is FinSeq-Location or x = IC )