let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 )
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 ) )
set s1 = s +* (Initialize I);
set s2 = s +* (Initialize (Directed I));
set m1 = LifeSpan ((P +* I),(s +* (Initialize I)));
A1: ProgramPart I = I by RELAT_1:209;
A2: ProgramPart (Directed I) = Directed I by RELAT_1:209;
assume that
A3: I is_closed_on s,P and
A4: I is_halting_on s,P ; :: thesis: ( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 )
A5: dom I = dom (Directed I) by FUNCT_4:105;

A6: now

let n be Element of NAT ; :: thesis: ( n < (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 implies IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) in dom (Directed I) )
assume n < (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 ; :: thesis: IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) in dom (Directed I)
then n <= LifeSpan ((P +* I),(s +* (Initialize I))) by NAT_1:13;
then Comput ((P +* I),(s +* (Initialize I)),n), Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n) equal_outside NAT by A3, A4, Th35;
then IC (Comput ((P +* I),(s +* (Initialize I)),n)) = IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) by COMPOS_1:24;
hence IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) in dom (Directed I) by A3, A5, SCMFSA7B:def 7, A1; :: thesis: verum

end;

ProgramPart (Directed I) = Directed I by RELAT_1:209;
then card I = card (ProgramPart (Directed I)) by Th33;
then A7: IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card (ProgramPart (Directed I)) by A3, A4, Th36;
hence A8: Directed I is_pseudo-closed_on s,P by A6, Def3, A2; :: thesis: pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1
for n being Element of NAT st not IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),n)) in dom (Directed I) holds
(LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 <= n by A6;
hence pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 by A7, A8, Def5, A2; :: thesis: verum