:: deftheorem defines good SCM_HALT:def 4 :
for i being Instruction of SCM+FSA holds
( i is good iff not i destroys intloc 0 );