:: deftheorem defines ";" SCMFSA6A:def 5 :
for I being Program of
for j being Instruction of SCM+FSA holds I ";" j = I ";" (Macro j);