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
( I is_pseudo-closed_on Initialize s,P +* I & pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),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
( I is_pseudo-closed_on Initialize s,P +* I & pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) )
let I be Program of SCM+FSA; :: thesis: ( I is_pseudo-closed_on s,P implies ( I is_pseudo-closed_on Initialize s,P +* I & pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) ) )
set s2 = Initialize (Initialize s);
set P2 = (P +* I) +* I;
A1: (P +* I) +* I = P +* I by FUNCT_4:93;
assume A4: I is_pseudo-closed_on s,P ; :: thesis: ( I is_pseudo-closed_on Initialize s,P +* I & pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) )
then A5: for n being Element of NAT st not IC (Comput (((P +* I) +* I),(Initialize (Initialize s)),n)) in dom I holds
pseudo-LifeSpan (s,P,I) <= n by A1, SCMFSA8A:def 4;
A6: for n being Element of NAT st n < pseudo-LifeSpan (s,P,I) holds
IC (Comput (((P +* I) +* I),(Initialize (Initialize s)),n)) in dom I by A4, A1, SCMFSA8A:def 4;
IC (Comput (((P +* I) +* I),(Initialize (Initialize s)),(pseudo-LifeSpan (s,P,I)))) = card I by A4, A1, SCMFSA8A:def 4;
hence A7: I is_pseudo-closed_on Initialize s,P +* I by A6, SCMFSA8A:def 2; :: thesis: pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I)
IC (Comput (((P +* I) +* I),(Initialize (Initialize s)),(pseudo-LifeSpan (s,P,I)))) = card I by A4, A1, SCMFSA8A:def 4;
hence pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) by A5, A7, SCMFSA8A:def 4; :: thesis: verum