for ins being Instruction of SCM+FSA st InsCode ins = 9 holds
ex a, b being Int-Location ex fa being FinSeq-Location st ins = b := (fa,a)