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;
assume A1: 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 A2: for n being Nat st not IC (Comput (((P +* I) +* I),(Initialize (Initialize s)),n)) in dom I holds
pseudo-LifeSpan (s,P,I) <= n by SCMFSA8A:def 4;
A3: for n being Nat st n < pseudo-LifeSpan (s,P,I) holds
IC (Comput (((P +* I) +* I),(Initialize (Initialize s)),n)) in dom I by A1, SCMFSA8A:def 4;
IC (Comput (((P +* I) +* I),(Initialize (Initialize s)),(pseudo-LifeSpan (s,P,I)))) = card I by A1, SCMFSA8A:def 4;
hence A4: I is_pseudo-closed_on Initialize s,P +* I by A3; :: 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 A1, SCMFSA8A:def 4;
hence pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) by A2, A4, SCMFSA8A:def 4; :: thesis: verum