let s be 0 -started State of SCMPDS; for I being halt-free parahalting Program of SCMPDS
for J being parahalting shiftable Program of SCMPDS holds IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))
set SA0 = Start-At (0,SCMPDS);
let I be halt-free parahalting Program of SCMPDS; for J being parahalting shiftable Program of SCMPDS holds IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))
let J be parahalting shiftable Program of SCMPDS; IExec ((I ';' J),s) = (IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))
set A = NAT ;
set D = SCM-Data-Loc ;
set ps = s | NAT;
set sI = stop I;
set sIJ = stop (I ';' J);
set s1 = (Initialize s) +* (stop I);
set m1 = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
set s2 = 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)));
I1:
(Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (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))
by COMPOS_1:125;
A1:
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 FUNCT_4:26;
B1:
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 FUNCT_4:26, SCMPDS_4:def 10;
A3:
(IExec (I,s)) | NAT = s | NAT
by PBOOLE:157;
I2:
(s +* (stop (I ';' J))) +* (Initialize (stop I)) = (Initialize (s +* (stop (I ';' J)))) +* (stop I)
by COMPOS_1:125;
AA:
Initialize s = s
by COMPOS_1:78;
(Initialize (s +* (stop (I ';' J)))) +* (stop I) = (s +* (stop (I ';' J))) +* (stop I)
by COMPOS_1:78;
then A4:
s +* (stop (I ';' J)),(s +* (stop (I ';' J))) +* (Initialize (stop I)) equal_outside NAT
by I2, FUNCT_7:132;
A7: ((Initialize s) +* (stop I)) +* (stop (I ';' J)) =
s +* ((stop I) +* (stop (I ';' J)))
by AA, FUNCT_4:15
.=
s +* (stop (I ';' J))
by Th17
;
A9:
stop J c= (Initialize (IExec (I,s))) +* (stop J)
by FUNCT_4:26;
A10: 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
;
A11:
stop I c= (Initialize s) +* (stop I)
by FUNCT_4:26;
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by FUNCT_4:26, SCMPDS_4:def 10;
then
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 EXTPRO_1:23;
then B12:
(Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (s | NAT) = Initialize (IExec (I,s))
by COMPOS_1:83;
(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))))))) +* (s | NAT)) +* (stop J) equal_outside dom (s | NAT)
by FUNCT_7:31, FUNCT_7:106;
then
(Initialize (IExec (I,s))) +* (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 B12, A10, FUNCT_7:28;
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 A1, A9, Th21;
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 A10, FUNCT_7:108;
then A14:
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 B1, A3, EXTPRO_1:23;
A15:
(Initialize s) +* (stop I),s +* (Start-At (0,SCMPDS)) equal_outside NAT
by FUNCT_7:28, FUNCT_7:132;
A16:
stop I c= (Initialize (s +* (stop (I ';' J)))) +* (stop I)
by FUNCT_4:26;
LL:
Initialize (s +* (stop (I ';' J))) = s +* (stop (I ';' J))
by COMPOS_1:78;
X:
((Initialize (s +* (stop (I ';' J)))) +* (stop I)) +* (stop (I ';' J)) = (s +* (stop (I ';' J))) +* ((stop I) +* (stop (I ';' J)))
by LL, FUNCT_4:15;
X1:
(Initialize (s +* (stop (I ';' J)))) +* (stop (I ';' J)) = s +* ((stop (I ';' J)) +* (stop (I ';' J)))
by LL, FUNCT_4:15;
X2:
(s +* (stop (I ';' J))) +* ((stop I) +* (stop (I ';' J))) = (s +* (stop (I ';' J))) +* (stop (I ';' J))
by Th17;
s +* (Start-At (0,SCMPDS)),s +* (stop (I ';' J)) equal_outside NAT
by AA, FUNCT_7:132;
then
(Initialize s) +* (stop I),s +* (stop (I ';' J)) equal_outside NAT
by A15, FUNCT_7:29;
then
(Initialize s) +* (stop I),(Initialize (s +* (stop (I ';' J)))) +* (stop I) equal_outside NAT
by A4, I2, FUNCT_7:29;
then A17:
LifeSpan ((ProgramPart ((Initialize (s +* (stop (I ';' J)))) +* (stop I))),((Initialize (s +* (stop (I ';' J)))) +* (stop I))) = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))
by A11, A16, Th21;
set S1 = (Initialize (s +* (stop (I ';' J)))) +* (stop I);
XX: DataPart (Comput ((ProgramPart ((Initialize (s +* (stop (I ';' J)))) +* (stop I))),((Initialize (s +* (stop (I ';' J)))) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) =
DataPart (Comput ((ProgramPart ((s +* (stop (I ';' J))) +* (stop (I ';' J)))),((s +* (stop (I ';' J))) +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by X2, X, A16, A17, Th24, COMPOS_1:138
.=
DataPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by A11, A7, Th24, X1, LL, COMPOS_1:138
;
A18: DataPart ((Comput ((ProgramPart ((Initialize (s +* (stop (I ';' J)))) +* (stop I))),((Initialize (s +* (stop (I ';' J)))) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (Initialize (stop J))) =
(DataPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (DataPart (Initialize (stop J)))
by XX, FUNCT_4:75
.=
DataPart ((Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (Initialize (stop J)))
by FUNCT_4:75
;
A19:
stop (I ';' J) c= s +* (stop (I ';' J))
by FUNCT_4:26;
then A20: DataPart (Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) =
DataPart ((Initialize (Comput ((ProgramPart ((Initialize (s +* (stop (I ';' J)))) +* (stop I))),((Initialize (s +* (stop (I ';' J)))) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J))
by A17, Lm3, LL
.=
DataPart ((Comput ((ProgramPart ((Initialize (s +* (stop (I ';' J)))) +* (stop I))),((Initialize (s +* (stop (I ';' J)))) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) +* (Initialize (stop J)))
by COMPOS_1:125
;
A21:
Shift ((stop J),(card I)) c= Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))
by A19, A17, Lm3, LL;
A22:
IC (Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I
by A19, A17, Lm3, LL;
then A23:
IC (Comput ((ProgramPart (Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart (s +* (stop (I ';' J)))),(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 A20, A21, A18, I1, A1, SCMPDS_4:84;
T1:
ProgramPart (s +* (stop (I ';' J))) = ProgramPart (Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))
by AMI_1:123;
A24:
DataPart (Comput ((ProgramPart (Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart (s +* (stop (I ';' J)))),(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 A22, A20, A21, A18, I1, A1, SCMPDS_4:84;
X:
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by FUNCT_4:26, SCMPDS_4:def 10;
A25:
(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 A11, EXTPRO_1:23, SCMPDS_4:def 10;
set SS1 = (Initialize (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J);
set SS2 = (Initialize (IExec (I,s))) +* (stop J);
yy:
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 A11, EXTPRO_1:23, SCMPDS_4:def 10;
(Initialize (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) +* (stop J),(Initialize (IExec (I,s))) +* (stop J) equal_outside NAT
by B12, A10, FUNCT_7:31, FUNCT_7:106;
then A26:
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 Th21, A1, A9, yy, COMPOS_1:24;
XX:
(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 X, EXTPRO_1:23;
A27: IC (IExec ((I ';' J),s)) =
IC (Result ((ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J)))))
by Th22
.=
IC (Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),(LifeSpan ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J)))))))
by A19, AA, EXTPRO_1:23, SCMPDS_4:def 10
.=
IC (Comput ((ProgramPart (s +* (stop (I ';' J)))),(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 A25, Th37, AA
.=
(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 A23, T1, 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 B1, EXTPRO_1:23
.=
(IC (IExec (J,(IExec (I,s))))) + (card I)
by A26, Th22, XX
;
IExec ((I ';' J),s) =
(Comput ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))),(LifeSpan ((ProgramPart (s +* (stop (I ';' J)))),(s +* (stop (I ';' J))))))) +* (s | NAT)
by A19, AA, EXTPRO_1:23, SCMPDS_4:def 10
.=
(Comput ((ProgramPart (s +* (stop (I ';' J)))),(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 A25, Th37, AA
;
then A28: DataPart (IExec ((I ';' J),s)) =
DataPart (Comput ((ProgramPart (s +* (stop (I ';' J)))),(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 A10, 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 A24, T1, EXTPRO_1:5
.=
DataPart (IExec (J,(IExec (I,s))))
by A10, A14, 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 ;
A29:
dom (Start-At (l,SCMPDS)) = {(IC SCMPDS)}
by FUNCOP_1:19;
A30:
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 A31:
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 A31, SCMPDS_4:20;
suppose A32:
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 A33:
not
x in dom (Start-At (l,SCMPDS))
by A29, TARSKI:def 1;
(IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x
by A28, A32, 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 A33, FUNCT_4:12;
verum end; suppose A34:
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 A35:
x in dom (Start-At (l,SCMPDS))
by FUNCOP_1:19;
thus (IExec ((I ';' J),s)) . x =
(Start-At (l,SCMPDS)) . (IC SCMPDS)
by A27, A34, FUNCOP_1:87
.=
((IExec (J,(IExec (I,s)))) +* (Start-At (((IC (IExec (J,(IExec (I,s))))) + (card I)),SCMPDS))) . x
by A34, A35, FUNCT_4:14
;
verum end; suppose A36:
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 A37:
not
x in dom (Start-At (l,SCMPDS))
by A29, TARSKI:def 1;
(IExec ((I ';' J),s)) | NAT =
s | NAT
by PBOOLE:157
.=
(IExec (J,(IExec (I,s)))) | NAT
by A3, PBOOLE:157
;
then
(IExec ((I ';' J),s)) . x = (IExec (J,(IExec (I,s)))) . x
by A36, 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 A37, 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 A30, FUNCT_1:9;
verum
end;