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