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