theorem Th67: :: SCMFSA_2:74

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