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 +* (Initialized (I ';' (Stop SCM+FSA)));
set s1 = s +* (Initialized I);
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))
A3: ProgramPart I = I by RELAT_1:209;
s +* (Initialized I) = (Initialized s) +* (Initialize I) by Th13;
then A4: P +* I halts_on s +* (Initialized I) by A2, SCMFSA7B:def 8, A3;
( P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialized (I ';' (Stop SCM+FSA))) & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialized I)))) + 1 ) by A1, A2, Lm4;
then A5: Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA))))) = Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 1)) by EXTPRO_1:23;
then DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) = DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I)))))) by A1, A2, Lm4;
then A6: DataPart (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) = DataPart (Result ((P +* I),(s +* (Initialized I)))) by A4, EXTPRO_1:23
.= DataPart ((Result ((P +* I),(s +* (Initialized I)))) +* (Start-At ((card I),SCM+FSA))) by Th10 ;
IC (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) = card I by A1, A2, A5, Lm4
.= IC ((Result ((P +* I),(s +* (Initialized I)))) +* (Start-At ((card I),SCM+FSA))) by FUNCT_4:121 ;
then A7: Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA))))),(Result ((P +* I),(s +* (Initialized I)))) +* (Start-At ((card I),SCM+FSA)) equal_outside NAT by A6, Th6;
dom (ProgramPart s) = NAT by COMPOS_1:34;
then A8: (Result ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialized (I ';' (Stop SCM+FSA)))))) +* (s | NAT) = ((Result ((P +* I),(s +* (Initialized I)))) +* (Start-At ((card I),SCM+FSA))) +* (s | NAT) by A7, FUNCT_7:108;
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 +* (Initialized (I ';' (Stop SCM+FSA)))))) +* (s | NAT) by SCMFSA6B:def 1
.= (Result ((P +* I),(s +* (Initialized I)))) +* ((Start-At ((card I),SCM+FSA)) +* (s | NAT)) by A8, FUNCT_4:15
.= (Result ((P +* I),(s +* (Initialized I)))) +* ((s | NAT) +* (Start-At ((card I),SCM+FSA))) by A9, FUNCT_4:36
.= ((Result ((P +* I),(s +* (Initialized I)))) +* (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