for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for i being Element of the InstructionsF of S st ( for l being Nat holds NIC (i,l) = {l} ) holds
JUMP i is empty