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 +* (Initialize ((intloc 0) .--> 1));
set s2 = s +* (Initialize ((intloc 0) .--> 1));
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))
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 ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA)) halts_on s +* (Initialize ((intloc 0) .--> 1)) & LifeSpan ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = (LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2 )
by A1, A2, Lm6;
then A5:
Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1)))) = Comput ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) + 2))
by EXTPRO_1:23;
then
DataPart (Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (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, Lm6;
then A6: DataPart (Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (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) + (card J)) + 1),SCM+FSA)))
by Th10
;
IC (Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) =
((card I) + (card J)) + 1
by A1, A2, A5, Lm6
.=
IC ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)))
by FUNCT_4:121
;
then A7:
NPP (Result ((P +* (((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCM+FSA))),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)))
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 +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT) = ((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA))) +* (s | NAT)
by A7, COMPOS_1:238;
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 +* (Initialize ((intloc 0) .--> 1))))) +* (s | NAT)
by SCMFSA6B:def 1
.=
(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* ((Start-At ((((card I) + (card J)) + 1),SCM+FSA)) +* (s | NAT))
by A8, FUNCT_4:15
.=
(Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* ((s | NAT) +* (Start-At ((((card I) + (card J)) + 1),SCM+FSA)))
by A9, FUNCT_4:36
.=
((Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) +* (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