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,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 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,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 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,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 ) )

set s1 = Initialize s;

set s2 = Initialize s;

set m1 = LifeSpan ((P +* I),(Initialize s));

IC (Initialize s) = 0 by MEMSTR_0:47;

then A1: IC (Initialize s) 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,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )

A4: dom I = dom (Directed I) by FUNCT_4:99;

then A6: IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card (Directed I) by A3, Th13;

hence A7: Directed I is_pseudo-closed_on s,P by A5; :: thesis: pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1

for n being Nat st not IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) holds

(LifeSpan ((P +* I),(Initialize s))) + 1 <= n by A5;

hence pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 by A6, A7, Def3; :: thesis: verum

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,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 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,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 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,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 ) )

set s1 = Initialize s;

set s2 = Initialize s;

set m1 = LifeSpan ((P +* I),(Initialize s));

IC (Initialize s) = 0 by MEMSTR_0:47;

then A1: IC (Initialize s) 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,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 )

A4: dom I = dom (Directed I) by FUNCT_4:99;

A5: now :: thesis: for n being Nat st n < (LifeSpan ((P +* I),(Initialize s))) + 1 holds

IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I)

card I = card (Directed I)
by SCMFSA6A:36;IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I)

let n be Nat; :: thesis: ( n < (LifeSpan ((P +* I),(Initialize s))) + 1 implies IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) )

assume n < (LifeSpan ((P +* I),(Initialize s))) + 1 ; :: thesis: IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I)

then n <= LifeSpan ((P +* I),(Initialize s)) by NAT_1:13;

then Comput ((P +* I),(Initialize s),n) = Comput ((P +* (Directed I)),(Initialize s),n) by A3, Th12;

then IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (Directed I)),(Initialize s),n)) ;

hence IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) by A4, AMISTD_1:21, A1, A2; :: thesis: verum

end;assume n < (LifeSpan ((P +* I),(Initialize s))) + 1 ; :: thesis: IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I)

then n <= LifeSpan ((P +* I),(Initialize s)) by NAT_1:13;

then Comput ((P +* I),(Initialize s),n) = Comput ((P +* (Directed I)),(Initialize s),n) by A3, Th12;

then IC (Comput ((P +* I),(Initialize s),n)) = IC (Comput ((P +* (Directed I)),(Initialize s),n)) ;

hence IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) by A4, AMISTD_1:21, A1, A2; :: thesis: verum

then A6: IC (Comput ((P +* (Directed I)),(Initialize s),((LifeSpan ((P +* I),(Initialize s))) + 1))) = card (Directed I) by A3, Th13;

hence A7: Directed I is_pseudo-closed_on s,P by A5; :: thesis: pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1

for n being Nat st not IC (Comput ((P +* (Directed I)),(Initialize s),n)) in dom (Directed I) holds

(LifeSpan ((P +* I),(Initialize s))) + 1 <= n by A5;

hence pseudo-LifeSpan (s,P,(Directed I)) = (LifeSpan ((P +* I),(Initialize s))) + 1 by A6, A7, Def3; :: thesis: verum