theorem Th45: :: SCMFSA8C:54

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