theorem Th3: :: SCMFSA6A:3

for i being Instruction of SCM+FSA
for s being State of SCM+FSA holds
( InsCode i in {0,6,7,8} or (Exec (i,s)) . (IC ) = (IC s) + 1 )