theorem :: SCMPDS_4:23

for I being shiftable Program of
for k1 being Integer st (card I) + k1 >= 0 holds
I ';' (goto k1) is shiftable