theorem :: AMISTD_2:8

for N being with_zero set
for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0 by Lm1;