theorem Th5: :: SCMFSA_7:5

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 aSeq (a,k) c= P & a <> intloc 0 holds
( ( for i being Nat st i <= len (aSeq (a,k)) holds
( IC (Comput (P,s,i)) = 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 )