for k1 being Integer st k1 <> 0 holds
not goto k1 is halting