theorem Th4: :: AMISTD_1:4

for N being with_zero set
for i being Instruction of (STC N) st InsCode i = 0 holds
i is halting