let s be State of SCMPDS ; for I being No-StopCode 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 No-StopCode 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 IsI = Initialized (stop I);
set IsJ = Initialized (stop J);
set IJ = I ';' J;
set IsIJ = Initialized (stop (I ';' J));
set s1 = s +* (Initialized (stop I));
set m1 = LifeSpan (s +* (Initialized (stop I)));
set s2 = s +* (Initialized (stop (I ';' J)));
set s3 = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J));
set m3 = LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)));
set sE = IExec I,s;
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 (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))
by A1, A2, A3, A4, Lm1;
J is_closed_on Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))
by A2, A3, A4, Th42;
then A6:
J is_closed_on (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))
by SCMPDS_6:38;
A7:
Initialized (stop J) c= (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))
by FUNCT_4:26;
A8:
Shift (stop J),(card I) c= Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))
by A1, A2, A3, A4, Lm1;
A9:
IC (Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I
by A1, A2, A3, A4, Lm1;
then A10:
IC (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = (IC (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) + (card I)
by A7, A5, A8, A6, SCMPDS_6:45;
A11:
DataPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = DataPart (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))
by A7, A9, A5, A8, A6, SCMPDS_6:45;
A12:
Initialized (stop J) c= (IExec I,s) +* (Initialized (stop J))
by FUNCT_4:26;
set R1 = (IExec I,s) +* (Initialized (stop J));
set R2 = (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J));
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:
Initialized (stop J) c= (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))
by FUNCT_4:26;
A15:
Initialized (stop J) c= (IExec I,s) +* (Initialized (stop J))
by FUNCT_4:26;
A16:
(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (s | NAT )) +* (Initialized (stop J)) equal_outside dom (s | NAT )
by FUNCT_7:31, FUNCT_7:106;
then A17:
((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (s | NAT )) +* (Initialized (stop J)),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) equal_outside dom (s | NAT )
by FUNCT_7:28;
A18:
ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I))
by A2, SCMPDS_6:def 3;
then A19:
(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) = (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))
by AMI_1:122;
A20:
DataPart (IExec I,s) = DataPart ((IExec I,s) +* (Initialized (stop J)))
by SCMPDS_6:9;
then A21:
J is_closed_on (IExec I,s) +* (Initialized (stop J))
by A3, A4, SCMPDS_6:37;
A22:
J is_halting_on (IExec I,s) +* (Initialized (stop J))
by A3, A4, A20, SCMPDS_6:37;
Result (s +* (Initialized (stop I))) = Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))
by A18, AMI_1:122;
then
((Result (s +* (Initialized (stop I)))) +* (s | NAT )) +* (Initialized (stop J)),(Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)) equal_outside NAT
by A13, A16, FUNCT_7:28;
then A23:
IC (Result ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) = IC (Result ((IExec I,s) +* (Initialized (stop J))))
by A21, A22, A15, A14, Th28, AMI_1:121;
A24:
Initialized (stop J) c= (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))
by 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 (s +* (Initialized (stop (I ';' J)))) halts_on s +* (Initialized (stop (I ';' J)))
by SCMPDS_6:def 3;
J is_halting_on Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))
by A2, A3, A4, Th42;
then A27:
ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) halts_on (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))
by SCMPDS_6:def 3;
IExec I,s = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (s | NAT )
by A18, AMI_1:122;
then
Result ((IExec I,s) +* (Initialized (stop J))), Result ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) equal_outside NAT
by A21, A22, A13, A17, A12, A24, Th28;
then
(Result ((IExec I,s) +* (Initialized (stop J)))) +* (s | NAT ) = (Result ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))) +* (s | NAT )
by A13, FUNCT_7:108;
then A28:
IExec J,(IExec I,s) = (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) +* (s | NAT )
by A27, A25, AMI_1:122;
T:
ProgramPart (s +* (Initialized (stop (I ';' J)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))
by AMI_1:144;
A29: IC (IExec (I ';' J),s) =
IC (Result (s +* (Initialized (stop (I ';' J)))))
by SCMPDS_5:22
.=
IC (Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop (I ';' J))))))
by A26, AMI_1:122
.=
IC (Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))))
by A1, A2, A3, A4, A19, Lm1
.=
(IC (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) + (card I)
by A10, AMI_1:51, T
.=
(IC (Result ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) + (card I)
by A27, AMI_1:122
.=
(IC (Result ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))))) + (card I)
by A18, AMI_1:122
.=
(IC (IExec J,(IExec I,s))) + (card I)
by A23, SCMPDS_5:22
;
IExec (I ';' J),s =
(Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop (I ';' J)))))) +* (s | NAT )
by A26, AMI_1:122
.=
(Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) +* (s | NAT )
by A1, A2, A3, A4, A19, Lm1
;
then A30: DataPart (IExec (I ';' J),s) =
DataPart (Comput (ProgramPart (s +* (Initialized (stop (I ';' J))))),(s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))))
by A13, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.=
DataPart (Comput (ProgramPart ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))),((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))
by A11, AMI_1:51, T
.=
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 AMI_1:48;
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, 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 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;