let P be Instruction-Sequence of SCM+FSA; :: 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))),(Initialize s))) = DataPart (Comput ((P +* I),(Initialize s),(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))),(Initialize s))) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I)))))
set D = Data-Locations ;
let I be Program of SCM+FSA; :: thesis: ( Directed I is_pseudo-closed_on s,P implies DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I))))) )
set I0 = Directed I;
set I1 = I ";" (Stop SCM+FSA);
set s2 = Initialize s;
set P2 = P +* I;
set s10 = Initialize s;
set P10 = P +* (I ";" (Stop SCM+FSA));
set k = pseudo-LifeSpan (s,P,(Directed I));
assume A1: Directed I is_pseudo-closed_on s,P ; :: thesis: DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I)))))
then A2: DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I))))) = DataPart (Comput ((P +* (I ";" (Stop SCM+FSA))),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I))))) by Th21;
I ";" (Stop SCM+FSA) is_halting_on s,P by A1, Th21;
then A3: P +* (I ";" (Stop SCM+FSA)) halts_on Initialize s ;
LifeSpan ((P +* (I ";" (Stop SCM+FSA))),(Initialize s)) = pseudo-LifeSpan (s,P,(Directed I)) by A1, Th21;
hence DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I))))) by A2, A3, EXTPRO_1:23; :: thesis: verum