for N being with_zero set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
(Exec (i,s)) . (IC ) = (IC s) + 1 by Lm3;