let s be 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 = (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));
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 SCMPDS_4:5;
A1:
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 I1, FUNCT_4:26;
A2:
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 I1, 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 A1, SCMPDS_4:63;
A3:
(IExec I,s) | NAT = s | NAT
by PBOOLE:157;
I2:
((Initialize s) +* (stop (I ';' J))) +* (Initialize (stop I)) = (Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)
by SCMPDS_4:5;
I3:
s +* (Initialize (stop (I ';' J))) = (Initialize s) +* (stop (I ';' J))
by SCMPDS_4:5;
(Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I) = ((Initialize s) +* (stop (I ';' J))) +* (stop I)
by I3, FUNCT_4:26, SCMPDS_4:34;
then A4:
(Initialize s) +* (stop (I ';' J)),((Initialize s) +* (stop (I ';' J))) +* (Initialize (stop I)) equal_outside NAT
by I2, FUNCT_7:132;
A5:
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 I1, FUNCT_4:26;
A6:
Initialize (stop J) c= (IExec I,s) +* (Initialize (stop J))
by FUNCT_4:26;
I4:
(Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)) = ((Initialize s) +* (stop I)) +* (Initialize (stop (I ';' J)))
by SCMPDS_4:5;
I5:
(Initialize s) +* (stop I) = s +* (Initialize (stop I))
by SCMPDS_4:5;
I6:
(Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop (I ';' J)) = ((Initialize s) +* (stop (I ';' J))) +* (Initialize (stop (I ';' J)))
by SCMPDS_4:5;
A7: (Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)) =
s +* ((Initialize (stop I)) +* (Initialize (stop (I ';' J))))
by I4, I5, FUNCT_4:15
.=
(Initialize s) +* (stop (I ';' J))
by Th17, I3
.=
(Initialize s) +* (stop (I ';' J))
;
I7:
(Initialize (IExec I,s)) +* (stop J) = (IExec I,s) +* (Initialize (stop J))
by SCMPDS_4:5;
A8:
Initialize (stop J) c= (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (Initialize (stop J))
by FUNCT_4:26;
A9:
Initialize (stop J) c= (Initialize (IExec I,s)) +* (stop J)
by I7, 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:
Initialize (stop I) c= (Initialize s) +* (stop I)
by I5, FUNCT_4:26;
then
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by SCMPDS_4:63;
then A12:
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 AMI_1:122;
A13:
(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
((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;
then
Result (ProgramPart ((IExec I,s) +* (Initialize (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 A10, A9, A2, A12, Th21, I1, I7;
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, I7, 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, AMI_1:122;
A15:
(Initialize s) +* (stop I),s +* (Start-At 0 ,SCMPDS ) equal_outside NAT
by FUNCT_7:28, FUNCT_7:132;
A16:
Initialize (stop I) c= (Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)
by I2, FUNCT_4:26;
X:
((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)) +* (Initialize (stop (I ';' J))) = ((Initialize s) +* (stop (I ';' J))) +* ((Initialize (stop I)) +* (Initialize (stop (I ';' J))))
by I2, FUNCT_4:15;
X1:
(Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop (I ';' J)) = s +* ((Initialize (stop (I ';' J))) +* (Initialize (stop (I ';' J))))
by I3, I6, FUNCT_4:15;
X2: ((Initialize s) +* (stop (I ';' J))) +* ((Initialize (stop I)) +* (Initialize (stop (I ';' J)))) =
((Initialize s) +* (stop (I ';' J))) +* (Initialize (stop (I ';' J)))
by Th17
.=
(Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop (I ';' J))
by I6
;
s +* (Start-At 0 ,SCMPDS ),(Initialize s) +* (stop (I ';' J)) equal_outside NAT
by FUNCT_7:132;
then
(Initialize s) +* (stop I),(Initialize s) +* (stop (I ';' J)) equal_outside NAT
by A15, FUNCT_7:29;
then
(Initialize s) +* (stop I),(Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I) equal_outside NAT
by A4, I2, FUNCT_7:29;
then A17:
LifeSpan (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)) = LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))
by A11, A16, Th21;
I7:
(Initialize ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))) +* (stop (I ';' J)) = ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)) +* (Initialize (stop (I ';' J)))
by SCMPDS_4:5;
set S1 = (Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I);
Comput (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))), Comput (ProgramPart ((Initialize ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) equal_outside NAT
by A16, A17, Th24;
then XX: DataPart (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) =
DataPart (Comput (ProgramPart ((Initialize ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))
by SCMPDS_4:24
.=
DataPart (Comput (ProgramPart (((Initialize s) +* (stop (I ';' J))) +* ((Initialize (stop I)) +* (Initialize (stop (I ';' J)))))),(((Initialize s) +* (stop (I ';' J))) +* ((Initialize (stop I)) +* (Initialize (stop (I ';' J))))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))
by X, I7
.=
DataPart (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))
by X2
.=
DataPart (Comput (ProgramPart (s +* ((Initialize (stop (I ';' J))) +* (Initialize (stop (I ';' J)))))),(s +* ((Initialize (stop (I ';' J))) +* (Initialize (stop (I ';' J))))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))
by X1
.=
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, I3, SCMPDS_4:24
;
A18: DataPart ((Comput (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (Initialize (stop J))) =
(DataPart (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (DataPart (Initialize (stop J)))
by FUNCT_4:75
.=
(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
.=
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:
Initialize (stop (I ';' J)) c= (Initialize s) +* (stop (I ';' J))
by I3, FUNCT_4:26;
then A20: 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 ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) +* (stop J))
by A17, Lm3
.=
DataPart ((Comput (ProgramPart ((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I))),((Initialize ((Initialize s) +* (stop (I ';' J)))) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (Initialize (stop J)))
by SCMPDS_4:5
;
A21:
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 A19, A17, Lm3;
A22:
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 A19, A17, Lm3;
then A23:
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 A20, A21, A5, A18, I1, SCMPDS_4:84;
T1:
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;
A24:
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 A22, A20, A21, A5, A18, I1, SCMPDS_4:84;
X:
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by A11, SCMPDS_4:63;
then 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 AMI_1:122;
IX:
(IExec I,s) +* (Initialize (stop J)) = (Initialize (IExec I,s)) +* (stop J)
by SCMPDS_4:5;
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 X, AMI_1:122;
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 A10, A13, A8, A6, Th21, I1, IX, COMPOS_1:24;
Y:
ProgramPart ((Initialize s) +* (stop (I ';' J))) halts_on (Initialize s) +* (stop (I ';' J))
by A19, SCMPDS_4:63;
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, AMI_1:122;
A27: IC (IExec (I ';' J),s) =
IC (Result (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))))
by Th22
.=
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 Y, AMI_1:122
.=
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 A25, Th37
.=
(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, AMI_1:51
.=
(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, AMI_1:122
.=
(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 XX
.=
(IC (IExec J,(IExec I,s))) + (card I)
by A26, Th22
;
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 Y, AMI_1:122
.=
(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 A25, Th37
;
then A28: 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 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, AMI_1:51
.=
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, SCMPDS_4:21;
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;