let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: 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:99;
A2: Initialize (Initialize s) = Initialize s by FUNCT_4:99;
A3: ProgramPart I = I by RELAT_1:209;
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 A2, A3, A1, SCMFSA8A:def 5;
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, A2, A3, A1, SCMFSA8A:def 5;
IC (Comput (((P +* I) +* I),(Initialize (Initialize s)),(pseudo-LifeSpan (s,P,I)))) = card I by A4, A2, A3, A1, SCMFSA8A:def 5;
hence A7: I is_pseudo-closed_on Initialize s,P +* I by A6, A3, SCMFSA8A:def 3; :: 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, A2, A3, A1, SCMFSA8A:def 5;
hence pseudo-LifeSpan (s,P,I) = pseudo-LifeSpan ((Initialize s),(P +* I),I) by A5, A7, A3, SCMFSA8A:def 5; :: thesis: verum