theorem Th68: :: SCMFSA_2:75

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