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