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