theorem :: AMISTD_1:5

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