theorem Th21: :: AMI_WSTD:21

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over N
for il being Element of NAT
for i being Instruction of S st i is sequential holds
NIC (i,il) = {(NextLoc (il,S))}