:: deftheorem defines ';' SCMPDS_4:def 1 :
for I, J being Program of holds I ';' J = I +* (Shift (J,(card I)));