theorem Th66: :: SCMFSA_2:73

for g being FinSeq-Location
for a, c being Int-Location
for s being State of SCM+FSA holds
( (Exec (((g,a) := c),s)) . (IC ) = (IC s) + 1 & ex k being Nat st
( k = |.(s . a).| & (Exec (((g,a) := c),s)) . g = (s . g) +* (k,(s . c)) ) & ( for b being Int-Location holds (Exec (((g,a) := c),s)) . b = s . b ) & ( for f being FinSeq-Location st f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )