theorem :: SCMPDS_5:21

for k1 being Integer holds goto k1 is No-StopCode