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 +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,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)))
thus DataPart (IExec (I ';' (Stop SCM+FSA )),s) = DataPart ((Result (s +* (Initialized (I ';' (Stop SCM+FSA ))))) +* (s | NAT )) by SCMFSA6B:def 1
.= DataPart (Result (s +* (Initialized (I ';' (Stop SCM+FSA ))))) by Th35
.= DataPart (Result (s +* ((I ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) by A1, Th18
.= 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