theorem Th40: :: SF_MASTR:40

for p being preProgram of SCM+FSA
for k being Nat holds UsedI*Loc p = UsedI*Loc (IncAddr (p,k))