for ins being Instruction of SCM+FSA st InsCode ins = 11 holds
ex a being Int-Location ex fa being FinSeq-Location st ins = a :=len fa