:: deftheorem defines refers SCMFSA7B:def 2 :
for I being preProgram of SCM+FSA
for a being Int-Location holds
( I refers a iff ex i being Instruction of SCM+FSA st
( i in rng I & i refers a ) );