for p being PartState of SCM+FSA
for f being FinSeq-Location st not f in dom p holds
not f in dom (Initialized p)