let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; for I, J being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
let I, J be Program of SCM+FSA; for s being State of SCM+FSA st I is_closed_on Initialized s,P & I is_halting_on Initialized s,P holds
IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
let s be State of SCM+FSA; ( I is_closed_on Initialized s,P & I is_halting_on Initialized s,P implies IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) )
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)));
set P2 = P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA));
assume that
A1:
I is_closed_on Initialized s,P
and
A2:
I is_halting_on Initialized s,P
; IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s) = (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),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 ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) halts_on s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))) & LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialized I)))) + 2 )
by A1, A2, Lm6;
then A5:
Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))) = Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialized I)))) + 2))
by EXTPRO_1:23;
then
DataPart (Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))) = DataPart (Comput ((P +* I),(s +* (Initialized I)),(LifeSpan ((P +* I),(s +* (Initialized I))))))
by A1, A2, Lm6;
then A6: DataPart (Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (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) + (card J)) + 1),SCM+FSA)))
by Th10
;
IC (Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))) =
((card I) + (card J)) + 1
by A1, A2, A5, Lm6
.=
IC ((Result ((P +* I),(s +* (Initialized I)))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)))
by FUNCT_4:121
;
then A7:
Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))))),(Result ((P +* I),(s +* (Initialized I)))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)) equal_outside NAT
by A6, Th6;
dom (ProgramPart s) = NAT
by COMPOS_1:34;
then A8:
(Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))) +* (s | NAT) = ((Result ((P +* I),(s +* (Initialized I)))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) +* (s | NAT)
by A7, FUNCT_7:108;
A9:
dom (s | NAT) misses dom (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
by COMPOS_1:130;
thus IExec ((((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)),P,s) =
(Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialized (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Result ((P +* I),(s +* (Initialized I)))) +* ((Start-At ((((card I) + (card J)) + 1),SCM+FSA)) +* (s | NAT))
by A8, FUNCT_4:15
.=
(Result ((P +* I),(s +* (Initialized I)))) +* ((s | NAT) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)))
by A9, FUNCT_4:36
.=
((Result ((P +* I),(s +* (Initialized I)))) +* (s | NAT)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
by FUNCT_4:15
.=
(IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))
by SCMFSA6B:def 1
; verum