:: deftheorem Def4 defines UsedInt*Loc SF_MASTR:def 4 :
for i being Instruction of SCM+FSA
for b₂ being Element of Fin FinSeq-Locations holds
( ( ( InsCode i = 9 or InsCode i = 10 ) implies ( b₂ = UsedInt*Loc i iff ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b₂ = {f} ) ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ( b₂ = UsedInt*Loc i iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b₂ = {f} ) ) ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ( b₂ = UsedInt*Loc i iff b₂ = {} ) ) );