theorem :: AMI_WSTD:19

for N being with_zero set
for l being Element of NAT
for i being Element of the InstructionsF of (STC N) st InsCode i = 1 holds
NIC (i,l) = {(NextLoc (l,(STC N)))}