:: deftheorem defines ";" SCMFSA6A:def 6 :
for i, j being Instruction of SCM+FSA holds i ";" j = (Macro i) ";" (Macro j);