for P being Instruction-Sequence of SCM+FSA
for s being State of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for k being Nat st ( for n being Nat st n <= k holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) holds
k < pseudo-LifeSpan (s,P,I)