:: deftheorem defines ';' SCMPDS_4:def 4 :
for i, j being Instruction of SCMPDS holds i ';' j = (Load i) ';' (Load j);