:: deftheorem Def3 defines pseudo-LifeSpan SCMFSA8A:def 4 :
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA
for I being Program of SCM+FSA st I is_pseudo-closed_on s,P holds
for b₄ being Nat holds
( b₄ = pseudo-LifeSpan (s,P,I) iff ( IC (Comput ((P +* I),(Initialize s),b₄)) = card I & ( for n being Nat st not IC (Comput ((P +* I),(Initialize s),n)) in dom I holds
b₄ <= n ) ) );