for N being with_zero set
for I being Instruction of (STC N) holds JumpPart I = 0 ;