let s be State of SCM+FSA; 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; 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; ( 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
; ( 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 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)let n be
Nat;
( 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
;
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;
verum end;
card I = card (Directed I)
by SCMFSA6A:36;
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; 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; verum