theorem :: SCMPDS_4:24

for I being shiftable Program of
for k1, k2 being Integer
for a being Int_position st (card I) + k2 >= 0 holds
I ';' ((a,k1) <>0_goto k2) is shiftable