theorem Th6: :: SCMBSORT:7

for p being preProgram of SCM+FSA
for ic being Instruction of SCM+FSA
for a, b being Int-Location st ic in rng p & ( ic = a := b or ic = AddTo (a,b) or ic = SubFrom (a,b) or ic = MultBy (a,b) or ic = Divide (a,b) ) holds
( a in UsedILoc p & b in UsedILoc p )