let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; for s being 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),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
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),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
let I be halt-free parahalting Program of SCMPDS; for J being parahalting shiftable Program of SCMPDS holds IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
let J be parahalting shiftable Program of SCMPDS; IExec ((I ';' J),P,s) = IncIC ((IExec (J,P,(IExec (I,P,s)))),(card I))
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;
set P1 = P +* (stop I);
set m1 = LifeSpan ((P +* (stop I)),(Initialize s));
set s2 = s;
set P2 = P +* (stop (I ';' J));
set s3 = Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))));
set P3 = (P +* (stop I)) +* (stop J);
set m3 = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))));
A2:
stop J c= (P +* (stop I)) +* (stop J)
by FUNCT_4:26;
A3:
(P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by FUNCT_4:26, SCMPDS_4:def 10;
A4:
(IExec (I,P,s)) | NAT = s | NAT
by PBOOLE:157;
A6:
Initialize s = s
by COMPOS_1:78;
A9:
stop J c= P +* (stop J)
by FUNCT_4:26;
A10: dom (s | NAT) =
(dom s) /\ NAT
by RELAT_1:90
.=
(({(IC )} \/ SCM-Data-Loc) \/ NAT) /\ NAT
by SCMPDS_4:19
.=
NAT
by XBOOLE_1:21
;
A11:
stop I c= P +* (stop I)
by FUNCT_4:26;
P +* (stop I) halts_on Initialize s
by FUNCT_4:26, SCMPDS_4:def 10;
then
Result ((P +* (stop I)),(Initialize s)) = Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))
by EXTPRO_1:23;
then
IExec (I,P,s) = (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) +* (s | NAT)
;
then A12:
(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) +* (s | NAT) = Initialize (IExec (I,P,s))
by COMPOS_1:83;
NPP (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) =
NPP (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))
.=
NPP ((Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) +* (s | NAT))
by COMPOS_1:236
.=
NPP ((Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) +* (s | NAT))
;
then
NPP (Initialize (IExec (I,P,s))) = NPP (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))
by A12;
then
NPP (Result ((P +* (stop J)),(Initialize (IExec (I,P,s))))) = NPP (Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))
by A2, A9, Th21;
then
(Result ((P +* (stop J)),(Initialize (IExec (I,P,s))))) +* (s | NAT) = (Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))) +* (s | NAT)
by A10, COMPOS_1:238;
then A13:
IExec (J,P,(IExec (I,P,s))) = (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))) +* (s | NAT)
by A3, A4, EXTPRO_1:23;
A15:
stop I c= (P +* (stop (I ';' J))) +* (stop I)
by FUNCT_4:26;
A16:
Initialize s = s
by COMPOS_1:78;
A18:
(P +* (stop (I ';' J))) +* (stop (I ';' J)) = P +* ((stop (I ';' J)) +* (stop (I ';' J)))
by FUNCT_4:15;
A19: ((P +* (stop (I ';' J))) +* (stop I)) +* (stop (I ';' J)) =
(P +* (stop (I ';' J))) +* ((stop I) +* (stop (I ';' J)))
by FUNCT_4:15
.=
(P +* (stop (I ';' J))) +* (stop (I ';' J))
by Th17
;
NPP (Initialize s) = NPP (Initialize s)
;
then A20:
LifeSpan (((P +* (stop (I ';' J))) +* (stop I)),(Initialize s)) = LifeSpan ((P +* (stop I)),(Initialize s))
by A11, A15, Th21;
set S1 = Initialize s;
set E1 = (P +* (stop (I ';' J))) +* (stop I);
X1:
NPP (Comput (((P +* (stop (I ';' J))) +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = NPP (Comput ((((P +* (stop (I ';' J))) +* (stop I)) +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),(Initialize s)))))
by A15, A20, Th24, A16;
X2:
NPP (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = NPP (Comput (((P +* (stop I)) +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by A11, Th24;
(P +* (stop I)) +* (stop (I ';' J)) =
P +* ((stop I) +* (stop (I ';' J)))
by FUNCT_4:15
.=
P +* (stop (I ';' J))
by Th17
.=
P +* ((stop (I ';' J)) +* (stop (I ';' J)))
.=
(P +* (stop (I ';' J))) +* (stop (I ';' J))
by A18
.=
((P +* (stop (I ';' J))) +* (stop I)) +* (stop (I ';' J))
by A19
;
then A21: DataPart (Comput (((P +* (stop (I ';' J))) +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) =
DataPart (Comput (((P +* (stop I)) +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),(Initialize s)))))
by X1, COMPOS_1:138
.=
DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by A16, X2, COMPOS_1:138
;
A22: DataPart (Comput (((P +* (stop (I ';' J))) +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) =
DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by A21
.=
DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
;
A23:
stop (I ';' J) c= P +* (stop (I ';' J))
by FUNCT_4:26;
then A24: DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),(Initialize s))))) =
DataPart (Initialize (Comput (((P +* (stop (I ';' J))) +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))
by A20, Lm4, A16
.=
DataPart (Comput (((P +* (stop (I ';' J))) +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by COMPOS_1:80
;
A25:
Shift ((stop J),(card I)) c= P +* (stop (I ';' J))
by A23, A20, Lm4;
A26:
IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
by A23, A20, Lm4, A16;
B29: DataPart (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) =
DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by COMPOS_1:80
.=
DataPart (Comput (((P +* (stop (I ';' J))) +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by A22
.=
DataPart (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),(Initialize s)))))
by A24
;
then A27:
IC (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),(Initialize s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))) = (IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))))) + (card I)
by A25, A2, SCMPDS_4:84, A26;
A29:
DataPart (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop I)),(Initialize s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))) = DataPart (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))))
by A26, A25, A2, SCMPDS_4:84, B29;
A30:
P +* (stop I) halts_on Initialize s
by FUNCT_4:26, SCMPDS_4:def 10;
A31:
Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = Initialize (Result ((P +* (stop I)),(Initialize s)))
by A11, EXTPRO_1:23, SCMPDS_4:def 10;
set SS1 = (Initialize (Result ((P +* (stop I)),(Initialize s)))) +* (stop J);
set SS2 = (Initialize (IExec (I,P,s))) +* (stop J);
A32:
Result ((P +* (stop I)),(Initialize s)) = Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))
by A11, EXTPRO_1:23, SCMPDS_4:def 10;
NPP (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) =
NPP (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))
.=
NPP ((Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) +* (s | NAT))
by COMPOS_1:236
.=
NPP (Initialize (IExec (I,P,s)))
by A12
;
then
NPP (Result (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),(Initialize s)))))) = NPP (Result ((P +* (stop J)),(Initialize (IExec (I,P,s)))))
by Th21, A2, A9, A32;
then A33:
IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Result ((P +* (stop I)),(Initialize s)))))) = IC (Result ((P +* (stop J)),(Initialize (IExec (I,P,s)))))
by COMPOS_1:230;
A34:
Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = Initialize (Result ((P +* (stop I)),(Initialize s)))
by A30, EXTPRO_1:23;
A35: IC (IExec ((I ';' J),P,s)) =
IC (Result ((P +* (stop (I ';' J))),(Initialize s)))
by Th22
.=
IC (Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s))))
by A23, A6, EXTPRO_1:23, SCMPDS_4:def 10
.=
IC (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))))
by A31, Th37, A6
.=
(IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))))) + (card I)
by A27, EXTPRO_1:5
.=
(IC (Result (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))) + (card I)
by A3, EXTPRO_1:23
.=
(IC (IExec (J,P,(IExec (I,P,s))))) + (card I)
by A33, Th22, A34
;
IExec ((I ';' J),P,s) =
(Comput ((P +* (stop (I ';' J))),s,(LifeSpan ((P +* (stop (I ';' J))),s)))) +* (s | NAT)
by A23, A6, EXTPRO_1:23, SCMPDS_4:def 10
.=
(Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))))) +* (s | NAT)
by A31, Th37, A6
;
then A36: DataPart (IExec ((I ';' J),P,s)) =
DataPart (Comput ((P +* (stop (I ';' J))),s,((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))))
by A10, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.=
DataPart (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))))))
by A29, EXTPRO_1:5
.=
DataPart (IExec (J,P,(IExec (I,P,s))))
by A10, A13, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
;
hereby verum
reconsider l =
(IC (IExec (J,P,(IExec (I,P,s))))) + (card I) as
Element of
NAT ;
A37:
dom (Start-At (l,SCMPDS)) = {(IC )}
by FUNCOP_1:19;
A38:
now let x be
set ;
( x in dom (IExec ((I ';' J),P,s)) implies (IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCMPDS))) . b1 )assume A39:
x in dom (IExec ((I ';' J),P,s))
;
(IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCMPDS))) . b1per cases
( x is Int_position or x = IC or x is Element of NAT )
by A39, SCMPDS_4:20;
suppose A40:
x is
Int_position
;
(IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCMPDS))) . b1then
x <> IC
by SCMPDS_2:52;
then A41:
not
x in dom (Start-At (l,SCMPDS))
by A37, TARSKI:def 1;
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x
by A36, A40, SCMPDS_4:23;
hence
(IExec ((I ';' J),P,s)) . x = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCMPDS))) . x
by A41, FUNCT_4:12;
verum end; suppose A42:
x = IC
;
(IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCMPDS))) . b1then
x in {(IC )}
by TARSKI:def 1;
then A43:
x in dom (Start-At (l,SCMPDS))
by FUNCOP_1:19;
thus (IExec ((I ';' J),P,s)) . x =
(Start-At (l,SCMPDS)) . (IC )
by A35, A42, FUNCOP_1:87
.=
((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCMPDS))) . x
by A42, A43, FUNCT_4:14
;
verum end; suppose A44:
x is
Element of
NAT
;
(IExec ((I ';' J),P,s)) . b1 = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCMPDS))) . b1then
x <> IC
by COMPOS_1:3;
then A45:
not
x in dom (Start-At (l,SCMPDS))
by A37, TARSKI:def 1;
(IExec ((I ';' J),P,s)) | NAT =
s | NAT
by PBOOLE:157
.=
(IExec (J,P,(IExec (I,P,s)))) | NAT
by A4, PBOOLE:157
;
then
(IExec ((I ';' J),P,s)) . x = (IExec (J,P,(IExec (I,P,s)))) . x
by A44, COMPOS_1:127;
hence
(IExec ((I ';' J),P,s)) . x = ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCMPDS))) . x
by A45, FUNCT_4:12;
verum end; end; dom (IExec ((I ';' J),P,s)) =
the
carrier of
SCMPDS
by PARTFUN1:def 4
.=
dom ((IExec (J,P,(IExec (I,P,s)))) +* (Start-At (((IC (IExec (J,P,(IExec (I,P,s))))) + (card I)),SCMPDS)))
by PARTFUN1:def 4
;
hence
IExec (
(I ';' J),
P,
s)
= IncIC (
(IExec (J,P,(IExec (I,P,s)))),
(card I))
by A38, FUNCT_1:9;
verum
end;