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, EXTPRO_1:23; :: thesis: verum