let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s holds
DataPart (Result (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Directed I)))
set D = Int-Locations \/ FinSeq-Locations ;
let I be Program of SCM+FSA ; :: thesis: ( Directed I is_pseudo-closed_on s implies DataPart (Result (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Directed I))) )
set I0 = Directed I;
set I1 = I ';' (Stop SCM+FSA );
set s2 = s +* (I +* (Start-At 0 ,SCM+FSA ));
set s10 = s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ));
set k = pseudo-LifeSpan s,(Directed I);
assume A1: Directed I is_pseudo-closed_on s ; :: thesis: DataPart (Result (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Directed I)))
then A2: DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Directed I))) = DataPart (Comput (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Directed I))) by Th58;
I ';' (Stop SCM+FSA ) is_halting_on s by A1, Th58;
then A3: ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) halts_on s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) by SCMFSA7B:def 8;
LifeSpan (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) = pseudo-LifeSpan s,(Directed I) by A1, Th58;
hence DataPart (Result (ProgramPart (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),(s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) = DataPart (Comput (ProgramPart (s +* (I +* (Start-At 0 ,SCM+FSA )))),(s +* (I +* (Start-At 0 ,SCM+FSA ))),(pseudo-LifeSpan s,(Directed I))) by A2, A3, AMI_1:122; :: thesis: verum