let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being Program of SCM+FSA st s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s,P holds
DataPart (IExec ((I ";" (Stop SCM+FSA)),P,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 s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s,P holds
DataPart (IExec ((I ";" (Stop SCM+FSA)),P,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: ( s . (intloc 0) = 1 & Directed I is_pseudo-closed_on s,P implies DataPart (IExec ((I ";" (Stop SCM+FSA)),P,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: s . (intloc 0) = 1 ; :: thesis: ( not Directed I is_pseudo-closed_on s,P or DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s)) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I))))) )
assume A2: Directed I is_pseudo-closed_on s,P ; :: thesis: DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s)) = DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I)))))
A3: Initialize s = Initialized s by A1, SCMFSA_M:18;
thus DataPart (IExec ((I ";" (Stop SCM+FSA)),P,s)) = DataPart (Result ((P +* (I ";" (Stop SCM+FSA))),(Initialize s))) by A3
.= DataPart (Comput ((P +* I),(Initialize s),(pseudo-LifeSpan (s,P,(Directed I))))) by A2, Th22 ; :: thesis: verum