let s be State of SCMPDS; for I being halt-free Program of SCMPDS
for J being shiftable Program of SCMPDS st I is_closed_on s & I is_halting_on s & J is_closed_on IExec (I,s) & J is_halting_on IExec (I,s) holds
IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))
let I be halt-free Program of SCMPDS; for J being shiftable Program of SCMPDS st I is_closed_on s & I is_halting_on s & J is_closed_on IExec (I,s) & J is_halting_on IExec (I,s) holds
IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))
let J be shiftable Program of SCMPDS; ( I is_closed_on s & I is_halting_on s & J is_closed_on IExec (I,s) & J is_halting_on IExec (I,s) implies IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS)) )
set ps = s | NAT;
set IJ = I ';' J;
set s1 = (Initialize s) +* (stop I);
set m1 = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
set s2 = (Initialize s) +* (stop (I ';' J));
set s3 = (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J);
set m3 = LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)));
set sE = IExec (I,s);
I3:
(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (Initialize (stop J)) = (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)
by COMPOS_1:125;
assume that
A1:
I is_closed_on s
and
A2:
I is_halting_on s
and
A3:
J is_closed_on IExec (I,s)
and
A4:
J is_halting_on IExec (I,s)
; IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))
A5:
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = DataPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))
by A1, A2, A3, A4, Lm1;
J is_closed_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))
by A2, A3, A4, Th42;
then A6:
J is_closed_on (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)
by SCMPDS_6:38;
A7:
Initialize (stop J) c= (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)
by I3, FUNCT_4:26;
A8:
Shift ((stop J),(card I)) c= Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))
by A1, A2, A3, A4, Lm1;
A9:
IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I
by A1, A2, A3, A4, Lm1;
then A10:
IC (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))),(LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)))))) = (IC (Comput ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))))))) + (card I)
by A7, A5, A8, A6, SCMPDS_6:45;
A11:
DataPart (Comput ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))),(LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)))))) = DataPart (Comput ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))))))
by A7, A9, A5, A8, A6, SCMPDS_6:45;
I6:
(Initialize (IExec (I,s))) +* (stop J) = (IExec (I,s)) +* (Initialize (stop J))
by COMPOS_1:125;
A12:
Initialize (stop J) c= (Initialize (IExec (I,s))) +* (stop J)
by I6, FUNCT_4:26;
set R1 = (Initialize (IExec (I,s))) +* (stop J);
set R2 = (Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J);
I4:
(IExec (I,s)) +* (Initialize (stop J)) = (Initialize (IExec (I,s))) +* (stop J)
by COMPOS_1:125;
I5:
(Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (Initialize (stop J)) = (Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)
by COMPOS_1:125;
A13: dom (s | NAT) =
(dom s) /\ NAT
by RELAT_1:90
.=
(({(IC SCMPDS)} \/ SCM-Data-Loc) \/ NAT) /\ NAT
by SCMPDS_4:19
.=
NAT
by XBOOLE_1:21
;
A14:
Initialize (stop J) c= (Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)
by I5, FUNCT_4:26;
A15:
Initialize (stop J) c= (Initialize (IExec (I,s))) +* (stop J)
by I4, FUNCT_4:26;
A16:
(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (Initialize (stop J)),((Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (s | NAT)) +* (Initialize (stop J)) equal_outside dom (s | NAT)
by FUNCT_7:31, FUNCT_7:106;
then A17:
((Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (s | NAT)) +* (Initialize (stop J)),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (Initialize (stop J)) equal_outside dom (s | NAT)
by FUNCT_7:28;
A18:
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by A2, SCMPDS_6:def 3;
then A19:
(Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J) = (Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)
by EXTPRO_1:23;
A20:
DataPart (IExec (I,s)) = DataPart ((Initialize (IExec (I,s))) +* (stop J))
by SCMPDS_6:9;
then A21:
J is_closed_on (Initialize (IExec (I,s))) +* (stop J)
by A3, A4, SCMPDS_6:37;
A22:
J is_halting_on (Initialize (IExec (I,s))) +* (stop J)
by A3, A4, A20, SCMPDS_6:37;
Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) = Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))
by A18, EXTPRO_1:23;
then
((Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (s | NAT)) +* (Initialize (stop J)),(Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (Initialize (stop J)) equal_outside NAT
by A13, A16, FUNCT_7:28;
then A23:
IC (Result ((ProgramPart ((Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J)))) = IC (Result ((ProgramPart ((Initialize (IExec (I,s))) +* (stop J))),((Initialize (IExec (I,s))) +* (stop J))))
by A21, A22, A15, A14, Th28, I4, I5, COMPOS_1:24;
A24:
Initialize (stop J) c= (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)
by I3, FUNCT_4:26;
A25:
(IExec (I,s)) | NAT = s | NAT
by PBOOLE:157;
I ';' J is_halting_on s
by A1, A2, A3, A4, Th43;
then A26:
ProgramPart ((Initialize s) +* (stop (I ';' J))) halts_on (Initialize s) +* (stop (I ';' J))
by SCMPDS_6:def 3;
J is_halting_on Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))
by A2, A3, A4, Th42;
then A27:
ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)) halts_on (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)
by SCMPDS_6:def 3;
IExec (I,s) = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (s | NAT)
by A18, EXTPRO_1:23;
then
Result ((ProgramPart ((Initialize (IExec (I,s))) +* (stop J))),((Initialize (IExec (I,s))) +* (stop J))), Result ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))) equal_outside NAT
by A21, A22, A13, A17, A12, A24, Th28, I3, I4;
then
(Result ((ProgramPart ((Initialize (IExec (I,s))) +* (stop J))),((Initialize (IExec (I,s))) +* (stop J)))) +* (s | NAT) = (Result ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)))) +* (s | NAT)
by A13, FUNCT_7:108;
then A28:
IExec (J,(IExec (I,s))) = (Comput ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)))))) +* (s | NAT)
by A27, A25, EXTPRO_1:23;
T:
ProgramPart ((Initialize s) +* (stop (I ';' J))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by AMI_1:123;
X:
Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) = Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))
by A18, EXTPRO_1:23;
A29: IC (IExec ((I ';' J),s)) =
IC (Result ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J)))))
by SCMPDS_5:22
.=
IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J)))))))
by A26, EXTPRO_1:23
.=
IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)))))))
by A1, A2, A3, A4, A19, Lm1
.=
(IC (Comput ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))))))) + (card I)
by A10, T, EXTPRO_1:5
.=
(IC (Result ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))))) + (card I)
by A27, EXTPRO_1:23
.=
(IC (Result ((ProgramPart ((Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))),((Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))))) + (card I)
by X
.=
(IC (IExec (J,(IExec (I,s))))) + (card I)
by A23, SCMPDS_5:22
;
IExec ((I ';' J),s) =
(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))))))) +* (s | NAT)
by A26, EXTPRO_1:23
.=
(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))))))) +* (s | NAT)
by A1, A2, A3, A4, A19, Lm1
;
then A30: DataPart (IExec ((I ';' J),s)) =
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + (LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)))))))
by A13, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.=
DataPart (Comput ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J)),(LifeSpan ((ProgramPart ((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))),((Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))))))
by A11, T, EXTPRO_1:5
.=
DataPart (IExec (J,(IExec (I,s))))
by A13, A28, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
;
hereby verum
reconsider l =
(IC (IExec (J,(IExec (I,s))))) + (card I) as
Element of
NAT ;
A31:
dom (Start-At (l,SCMPDS)) = {(IC SCMPDS)}
by FUNCOP_1:19;
A32:
now let x be
set ;
( x in dom (IExec ((I ';' J),s)) implies (IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))) . b1 )assume A33:
x in dom (IExec ((I ';' J),s))
;
(IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))) . b1per cases
( x is Int_position or x = IC SCMPDS or x is Element of NAT )
by A33, SCMPDS_4:20;
suppose A34:
x is
Int_position
;
(IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))) . b1then
x <> IC SCMPDS
by SCMPDS_2:52;
then A35:
not
x in dom (Start-At (l,SCMPDS))
by A31, TARSKI:def 1;
(IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x
by A30, A34, SCMPDS_4:23;
hence
(IExec ((I ';' J),s)) . x = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))) . x
by A35, FUNCT_4:12;
verum end; suppose A36:
x = IC SCMPDS
;
(IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))) . b1then
x in {(IC SCMPDS)}
by TARSKI:def 1;
then A37:
x in dom (Start-At (l,SCMPDS))
by FUNCOP_1:19;
thus (IExec ((I ';' J),s)) . x =
(Start-At (l,SCMPDS)) . (IC SCMPDS)
by A29, A36, FUNCOP_1:87
.=
((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))) . x
by A36, A37, FUNCT_4:14
;
verum end; suppose A38:
x is
Element of
NAT
;
(IExec ((I ';' J),s)) . b1 = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))) . b1then
x <> IC SCMPDS
by COMPOS_1:3;
then A39:
not
x in dom (Start-At (l,SCMPDS))
by A31, TARSKI:def 1;
(IExec ((I ';' J),s)) | NAT =
s | NAT
by PBOOLE:157
.=
(IExec (J,(IExec (I,s)))) | NAT
by A25, PBOOLE:157
;
then
(IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x
by A38, COMPOS_1:127;
hence
(IExec ((I ';' J),s)) . x = ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))) . x
by A39, FUNCT_4:12;
verum end; end; dom (IExec ((I ';' J),s)) =
the
carrier of
SCMPDS
by PARTFUN1:def 4
.=
dom ((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS)))
by PARTFUN1:def 4
;
hence
IExec (
(I ';' J),
s)
= (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))
by A32, FUNCT_1:9;
verum
end;