:: deftheorem Def1 defines good SFMASTR1:def 1 :
for i being Instruction of SCM+FSA holds
( i is good iff Macro i is good );