:: deftheorem defines ';' SCMPDS_4:def 3 :
for I being Program of
for j being Instruction of SCMPDS holds I ';' j = I ';' (Load j);