:: deftheorem defines ';' SCMPDS_4:def 2 :
for i being Instruction of SCMPDS
for J being Program of holds i ';' J = (Load i) ';' J;