let s be State of SCM+FSA ; :: thesis: for I being Program of SCM+FSA st I is_closed_on Initialized s & I is_halting_on Initialized s holds
IExec (I ';' (Stop SCM+FSA )),s = (IExec I,s) +* (Start-At (card I),SCM+FSA )
let I be Program of SCM+FSA ; :: thesis: ( I is_closed_on Initialized s & I is_halting_on Initialized s implies IExec (I ';' (Stop SCM+FSA )),s = (IExec I,s) +* (Start-At (card I),SCM+FSA ) )
assume A1: I is_closed_on Initialized s ; :: thesis: ( not I is_halting_on Initialized s or IExec (I ';' (Stop SCM+FSA )),s = (IExec I,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 ; :: thesis: IExec (I ';' (Stop SCM+FSA )),s = (IExec I,s) +* (Start-At (card I),SCM+FSA )
s +* (Initialized I) = (Initialized s) +* (I +* (Start-At 0 ,SCM+FSA )) by Th13;
then A3: ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I) by A2, SCMFSA7B:def 8;
( ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA )))) halts_on s +* (Initialized (I ';' (Stop SCM+FSA ))) & LifeSpan (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))) = (LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1 ) by A1, A2, Lm4;
then A4: Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))) = Comput (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),((LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) + 1) by AMI_1:122;
then DataPart (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) = DataPart (Comput (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(LifeSpan (ProgramPart (s +* (Initialized I))),(s +* (Initialized I)))) by A1, A2, Lm4;
then A5: DataPart (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) = DataPart (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) by A3, AMI_1:122
.= DataPart ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Start-At (card I),SCM+FSA )) by Th10 ;
IC (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) = card I by A1, A2, A4, Lm4
.= IC ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Start-At (card I),SCM+FSA )) by FUNCT_4:121 ;
then A6: Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA )))),(Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Start-At (card I),SCM+FSA ) equal_outside NAT by A5, Th6;
dom (s | NAT ) = NAT by Th3;
then A7: (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) +* (s | NAT ) = ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (Start-At (card I),SCM+FSA )) +* (s | NAT ) by A6, FUNCT_7:108;
A8: dom (s | NAT ) misses dom (Start-At (card I),SCM+FSA ) by Th12;
thus IExec (I ';' (Stop SCM+FSA )),s = (Result (ProgramPart (s +* (Initialized (I ';' (Stop SCM+FSA ))))),(s +* (Initialized (I ';' (Stop SCM+FSA ))))) +* (s | NAT ) by SCMFSA6B:def 1
.= (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* ((Start-At (card I),SCM+FSA ) +* (s | NAT )) by A7, FUNCT_4:15
.= (Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* ((s | NAT ) +* (Start-At (card I),SCM+FSA )) by A8, FUNCT_4:36
.= ((Result (ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) +* (s | NAT )) +* (Start-At (card I),SCM+FSA ) by FUNCT_4:15
.= (IExec I,s) +* (Start-At (card I),SCM+FSA ) by SCMFSA6B:def 1 ; :: thesis: verum