for a, b being Int-Location
for f being FinSeq-Location
for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds
UsedInt*Loc i = {f}