for p being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being really-closed Program of SCM+FSA
for a being Int-Location st not I destroys a & Initialize ((intloc 0) .--> 1) c= s & I c= p holds
for k being Nat holds (Comput (p,s,k)) . a = s . a