theorem :: SF_MASTR:63

for f being FinSeq-Location
for I being Program of
for n being Nat
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) & not f in UsedI*Loc I holds
(Comput (P,s,n)) . f = s . f