let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,()) = (LifeSpan ((P +* I),())) + 1 )

let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I is_halting_on s,P holds
( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,()) = (LifeSpan ((P +* I),())) + 1 )

let I be really-closed Program of SCM+FSA; :: thesis: ( I is_halting_on s,P implies ( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,()) = (LifeSpan ((P +* I),())) + 1 ) )
set s1 = Initialize s;
set s2 = Initialize s;
set m1 = LifeSpan ((P +* I),());
IC () = 0 by MEMSTR_0:47;
then A1: IC () in dom I by AFINSQ_1:65;
A2: I c= P +* I by FUNCT_4:25;
assume A3: I is_halting_on s,P ; :: thesis: ( Directed I is_pseudo-closed_on s,P & pseudo-LifeSpan (s,P,()) = (LifeSpan ((P +* I),())) + 1 )
A4: dom I = dom () by FUNCT_4:99;
A5: now :: thesis: for n being Nat st n < (LifeSpan ((P +* I),())) + 1 holds
IC (Comput ((P +* ()),(),n)) in dom ()
let n be Nat; :: thesis: ( n < (LifeSpan ((P +* I),())) + 1 implies IC (Comput ((P +* ()),(),n)) in dom () )
assume n < (LifeSpan ((P +* I),())) + 1 ; :: thesis: IC (Comput ((P +* ()),(),n)) in dom ()
then n <= LifeSpan ((P +* I),()) by NAT_1:13;
then Comput ((P +* I),(),n) = Comput ((P +* ()),(),n) by ;
then IC (Comput ((P +* I),(),n)) = IC (Comput ((P +* ()),(),n)) ;
hence IC (Comput ((P +* ()),(),n)) in dom () by ; :: thesis: verum
end;
card I = card () by SCMFSA6A:36;
then A6: IC (Comput ((P +* ()),(),((LifeSpan ((P +* I),())) + 1))) = card () by ;
hence A7: Directed I is_pseudo-closed_on s,P by A5; :: thesis: pseudo-LifeSpan (s,P,()) = (LifeSpan ((P +* I),())) + 1
for n being Nat st not IC (Comput ((P +* ()),(),n)) in dom () holds
(LifeSpan ((P +* I),())) + 1 <= n by A5;
hence pseudo-LifeSpan (s,P,()) = (LifeSpan ((P +* I),())) + 1 by A6, A7, Def3; :: thesis: verum