theorem :: AMI_WSTD:18

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
IC (Exec (i,s)) = NextLoc ((IC s),(STC N))