theorem :: SCMFSA_7:6

for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT
for s being 0 -started State of SCM+FSA st s . (intloc 0) = 1 holds
for a being Int-Location
for k being Integer st a := k c= P & a <> intloc 0 holds
( P halts_on s & (Result (P,s)) . a = k & ( for b being Int-Location st b <> a holds
(Result (P,s)) . b = s . b ) & ( for f being FinSeq-Location holds (Result (P,s)) . f = s . f ) )