let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds
DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) = DataPart (Comput ((P +* I),(s +* (Initialize I)),(pseudo-LifeSpan (s,P,(Directed I)))))
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA st Directed I is_pseudo-closed_on s,P holds
DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) = DataPart (Comput ((P +* I),(s +* (Initialize I)),(pseudo-LifeSpan (s,P,(Directed I)))))
set D = Data-Locations SCM+FSA;
let I be Program of SCM+FSA; :: thesis: ( Directed I is_pseudo-closed_on s,P implies DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) = DataPart (Comput ((P +* I),(s +* (Initialize I)),(pseudo-LifeSpan (s,P,(Directed I))))) )
set I0 = Directed I;
set I1 = I ';' (Stop SCM+FSA);
set s2 = s +* (Initialize I);
set P2 = P +* I;
set s10 = s +* (Initialize (I ';' (Stop SCM+FSA)));
set P10 = P +* (I ';' (Stop SCM+FSA));
A1: ProgramPart (I ';' (Stop SCM+FSA)) = I ';' (Stop SCM+FSA) by RELAT_1:209;
set k = pseudo-LifeSpan (s,P,(Directed I));
assume A2: Directed I is_pseudo-closed_on s,P ; :: thesis: DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) = DataPart (Comput ((P +* I),(s +* (Initialize I)),(pseudo-LifeSpan (s,P,(Directed I)))))
then A3: DataPart (Comput ((P +* I),(s +* (Initialize I)),(pseudo-LifeSpan (s,P,(Directed I))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(pseudo-LifeSpan (s,P,(Directed I))))) by Th58;
I ';' (Stop SCM+FSA) is_halting_on s,P by A2, Th58;
then A4: P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) by SCMFSA7B:def 8, A1;
LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = pseudo-LifeSpan (s,P,(Directed I)) by A2, Th58;
then Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(pseudo-LifeSpan (s,P,(Directed I)))) by A4, EXTPRO_1:23;
hence DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))))) = DataPart (Comput ((P +* I),(s +* (Initialize I)),(pseudo-LifeSpan (s,P,(Directed I))))) by A3; :: thesis: verum