for a being Int-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 a in UsedILoc I holds
(Comput (P,s,n)) . a = s . a