:: deftheorem Def6 defines := SCMFSA_2:def 8 :
for a, b being Int-Location
for b₃ being Instruction of SCM+FSA holds
( b₃ = a := b iff ex A, B being Data-Location st
( a = A & b = B & b₃ = A := B ) );