let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on s & I is_halting_on s holds
( Directed I is_pseudo-closed_on s & pseudo-LifeSpan s,(Directed I) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on s & I is_halting_on s implies ( Directed I is_pseudo-closed_on s & pseudo-LifeSpan s,(Directed I) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 ) )
set s1 = s +* (I +* (Start-At 0 ,SCM+FSA ));
set s2 = s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ));
set m1 = LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )));
assume that
A1: I is_closed_on s and
A2: I is_halting_on s ; :: thesis: ( Directed I is_pseudo-closed_on s & pseudo-LifeSpan s,(Directed I) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 )
A3: dom I = dom (Directed I) by FUNCT_4:105;

A4: now

let n be Element of NAT ; :: thesis: ( n < (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 implies IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Directed I) )
assume n < (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 ; :: thesis: IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Directed I)
then n <= LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))) by NAT_1:13;
then IC (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),n) = IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),n) by A1, A2, Th35, COMPOS_1:24;
hence IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Directed I) by A1, A3, SCMFSA7B:def 7; :: thesis: verum

end;

ProgramPart (Directed I) = Directed I by RELAT_1:209;
then card I = card (ProgramPart (Directed I)) by Th33;
then A5: IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),((LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1)) = card (ProgramPart (Directed I)) by A1, A2, Th36;
hence A6: Directed I is_pseudo-closed_on s by A4, Def3; :: thesis: pseudo-LifeSpan s,(Directed I) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1
for n being Element of NAT st not IC (Comput (ProgramPart (s +* ((Directed I) +* (Start-At 0 ,SCM+FSA )))),(s +* ((Directed I) +* (Start-At 0 ,SCM+FSA ))),n) in dom (Directed I) holds
(LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 <= n by A4;
hence pseudo-LifeSpan s,(Directed I) = (LifeSpan (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA )))) + 1 by A5, A6, Def5; :: thesis: verum