:: deftheorem Def1 defines UsedIntLoc SF_MASTR:def 1 :
for i being Instruction of SCM+FSA
for b₂ being Element of Fin Int-Locations holds
( ( InsCode i in {1,2,3,4,5} implies ( b₂ = UsedIntLoc i iff ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b₂ = {a,b} ) ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) implies ( b₂ = UsedIntLoc i iff ex a being Int-Location ex l being Nat st
( ( i = a =0_goto l or i = a >0_goto l ) & b₂ = {a} ) ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ( b₂ = UsedIntLoc i iff ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b₂ = {a,b} ) ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ( b₂ = UsedIntLoc i iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b₂ = {a} ) ) ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ( b₂ = UsedIntLoc i iff b₂ = {} ) ) );