let P be Instruction-Sequence of SCM+FSA; :: thesis: 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)
let s be State of SCM+FSA; :: thesis: 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)
let I be Program of SCM+FSA; :: thesis: ( I is_pseudo-closed_on s,P implies 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) )
assume I is_pseudo-closed_on s,P ; :: thesis: 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)
then IC (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,I)))) = card I by SCMFSA8A:def 4;
then A1: not IC (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,I)))) in dom I ;
let k be Nat; :: thesis: ( ( for n being Nat st n <= k holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ) implies k < pseudo-LifeSpan (s,P,I) )
assume for n being Nat st n <= k holds
IC (Comput ((P +* I),(Initialize s),n)) in dom I ; :: thesis: k < pseudo-LifeSpan (s,P,I)
hence pseudo-LifeSpan (s,P,I) > k by A1; :: thesis: verum