theorem Th4: :: SCMFSA_7:4

for P being the InstructionsF of SCM+FSA -valued ManySortedSet of NAT
for c0 being Nat
for s being b₂ -started State of SCM+FSA st s . (intloc 0) = 1 holds
for a being Int-Location
for k being Integer st a <> intloc 0 & ( for c being Nat st c in dom (aSeq (a,k)) holds
(aSeq (a,k)) . c = P . (c0 + c) ) holds
( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = c0 + i & ( for b being Int-Location st b <> a holds
(Comput (P,s,i)) . b = s . b ) & ( for f being FinSeq-Location holds (Comput (P,s,i)) . f = s . f ) ) ) & (Comput (P,s,(len (aSeq (a,k))))) . a = k )