theorem Th23: :: SF_MASTR:23

for i being Instruction of SCM+FSA
for k being Nat holds UsedIntLoc i = UsedIntLoc (IncAddr (i,k))