for I, J being Program of SCM+FSA
for a being Int-Location st not I destroys a & not J destroys a holds
not I ";" J destroys a