let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s holds
DataPart (IExec ((I ';' (Stop SCM+FSA)),s)) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s,(Directed I)))))
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations;
let I be Program of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s implies DataPart (IExec ((I ';' (Stop SCM+FSA)),s)) = 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 +* (Initialize (I ';' (Stop SCM+FSA)));
set k = pseudo-LifeSpan (s,(Directed I));
assume A1: s . (intloc 0) = 1 ; :: thesis: ( not Directed I is_pseudo-closed_on s or DataPart (IExec ((I ';' (Stop SCM+FSA)),s)) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s,(Directed I))))) )
assume A2: Directed I is_pseudo-closed_on s ; :: thesis: DataPart (IExec ((I ';' (Stop SCM+FSA)),s)) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s,(Directed I)))))
X: s +* (Initialize (I ';' (Stop SCM+FSA))) = s +* (Initialized (I ';' (Stop SCM+FSA))) by A1, Th18;
thus DataPart (IExec ((I ';' (Stop SCM+FSA)),s)) = DataPart ((Result ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) +* (s | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA))))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) by Th35
.= DataPart (Result ((ProgramPart (s +* (Initialize (I ';' (Stop SCM+FSA))))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) by X
.= DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(pseudo-LifeSpan (s,(Directed I))))) by A2, Th59 ; :: thesis: verum