theorem Th12: :: AMISTD_1:12

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