theorem Th12: :: SCMBSORT:13

for t being FinPartState of SCM+FSA
for p being Program of
for x being set st dom t c= Int-Locations \/ FinSeq-Locations & x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) & x is not Int-Location holds
x is FinSeq-Location