:: deftheorem defines ";" SCMFSA6A:def 4 :
for i being Instruction of SCM+FSA
for J being Program of holds i ";" J = (Macro i) ";" J;