let s be State of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((I ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being Program of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((I ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))
let I be Program of SCM+FSA; :: thesis: ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies IExec ((I ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) )
assume A1: I is_closed_on Initialized s,P ; :: thesis: ( not I is_halting_on Initialized s,P or IExec ((I ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) )
set s2 = s +* (Initialize ((intloc 0) .--> 1));
set s1 = s +* (Initialize ((intloc 0) .--> 1));
assume A2: I is_halting_on Initialized s,P ; :: thesis: IExec ((I ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA))
s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by Th13;
then A4: P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by A2, SCMFSA7B:def 8;
( P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1 ) by A1, A2, Lm4;
then A5: Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 1)) by EXTPRO_1:23;
then DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) = DataPart (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))))) by A1, A2, Lm4;
then A6: DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) = DataPart (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) by A4, EXTPRO_1:23
.= DataPart ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Start-At ((card I),SCM+FSA))) by Th10 ;
IC (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) = card I by A1, A2, A5, Lm4
.= IC ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Start-At ((card I),SCM+FSA))) by FUNCT_4:121 ;
then A7: NPP (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Start-At ((card I),SCM+FSA))) by A6, Th6;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then A8: (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) = ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Start-At ((card I),SCM+FSA))) +* (s | NAT) by A7, COMPOS_1:238;
A9: dom (s | NAT) misses dom (Start-At ((card I),SCM+FSA)) by COMPOS_1:130;
thus IExec ((I ';' (Stop SCM+FSA)),P,s) = (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* ((Start-At ((card I),SCM+FSA)) +* (s | NAT)) by A8, FUNCT_4:15
.= (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* ((s | NAT) +* (Start-At ((card I),SCM+FSA))) by A9, FUNCT_4:36
.= ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)) +* (Start-At ((card I),SCM+FSA)) by FUNCT_4:15
.= (IExec (I,P,s)) +* (Start-At ((card I),SCM+FSA)) by SCMFSA6B:def 1 ; :: thesis: verum