let s be State of SCMPDS ; :: thesis: for I being parahalting No-StopCode 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)))
let I be parahalting No-StopCode Program of SCMPDS ; :: thesis: 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)))
let J be parahalting shiftable Program of SCMPDS ; :: thesis: IExec (I ';' J),s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))
set A = NAT ;
set D = SCM-Data-Loc ;
set ps = s | NAT ;
set sI = stop I;
set IsI = Initialized (stop I);
set IsJ = Initialized (stop J);
set sIJ = stop (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 = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J));
set m3 = LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)));
A1:
Initialized (stop I) c= s +* (Initialized (stop I))
by FUNCT_4:26;
A2:
Initialized (stop (I ';' J)) c= s +* (Initialized (stop (I ';' J)))
by FUNCT_4:26;
A3:
Initialized (stop J) c= (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))
by FUNCT_4:26;
A4: 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
;
A5:
(Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)),((Computation (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 A6:
((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (s | NAT )) +* (Initialized (stop J)),(Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) equal_outside dom (s | NAT )
by FUNCT_7:28;
Result ((IExec I,s) +* (Initialized (stop J))), Result ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) equal_outside NAT
proof
A7:
Initialized (stop J) c= (IExec I,s) +* (Initialized (stop J))
by FUNCT_4:26;
A8:
Initialized (stop J) c= (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))
by FUNCT_4:26;
IExec I,
s = (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (s | NAT )
by A1, AMI_1:122, SCMPDS_4:63;
hence
Result ((IExec I,s) +* (Initialized (stop J))),
Result ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) equal_outside NAT
by A4, A6, A7, A8, Th21;
:: thesis: verum
end;
then A9:
(Result ((IExec I,s) +* (Initialized (stop J)))) +* (s | NAT ) = (Result ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))) +* (s | NAT )
by A4, FUNCT_7:108;
A10:
(Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)) = (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))
by A1, AMI_1:122, SCMPDS_4:63;
A11: IExec (I ';' J),s =
(Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop (I ';' J)))))) +* (s | NAT )
by A2, AMI_1:122, SCMPDS_4:63
.=
(Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) +* (s | NAT )
by A10, Th37
;
A12:
(IExec I,s) | NAT = s | NAT
by CARD_3:99;
then A13:
IExec J,(IExec I,s) = (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) +* (s | NAT )
by A3, A9, AMI_1:122, SCMPDS_4:63;
set SA0 = Start-At (inspos 0 );
A14: s +* (Initialized (stop (I ';' J))) =
(s +* (stop (I ';' J))) +* (Start-At (inspos 0 ))
by FUNCT_4:15
.=
(s +* (Start-At (inspos 0 ))) +* (stop (I ';' J))
by SCMPDS_4:62
;
A15: s +* (Initialized (stop I)) =
(s +* (stop I)) +* (Start-At (inspos 0 ))
by FUNCT_4:15
.=
(s +* (Start-At (inspos 0 ))) +* (stop I)
by SCMPDS_4:62
;
A16:
(s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) = (s +* (Initialized (stop (I ';' J)))) +* (stop I)
by FUNCT_4:26, SCMPDS_4:34;
A17:
Initialized (stop I) c= (s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))
by FUNCT_4:26;
A18:
s +* (Initialized (stop (I ';' J))),(s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) equal_outside NAT
by A16, AMI_1:120;
A19:
s +* (Initialized (stop I)),s +* (Start-At (inspos 0 )) equal_outside NAT
by A15, AMI_1:120, FUNCT_7:28;
s +* (Start-At (inspos 0 )),s +* (Initialized (stop (I ';' J))) equal_outside NAT
by A14, AMI_1:120;
then
s +* (Initialized (stop I)),s +* (Initialized (stop (I ';' J))) equal_outside NAT
by A19, FUNCT_7:29;
then
s +* (Initialized (stop I)),(s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I)) equal_outside NAT
by A18, FUNCT_7:29;
then A20:
LifeSpan ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))) = LifeSpan (s +* (Initialized (stop I)))
by A1, A17, Th21;
then A21:
( IC (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) & DataPart (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart ((Computation ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) & Shift (stop J),(card I) c= Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I)))) )
by A2, Lm3;
A22:
( DataPart (Computation (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = DataPart (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) & IC (Computation (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = (IC (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) + (card I) )
proof
A23:
Initialized (stop J) c= (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))
by FUNCT_4:26;
A24:
(s +* (Initialized (stop I))) +* (Initialized (stop (I ';' J))) =
s +* ((Initialized (stop I)) +* (Initialized (stop (I ';' J))))
by FUNCT_4:15
.=
s +* (Initialized (stop (I ';' J)))
by Th17
;
DataPart (Computation ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) =
DataPart (Computation (((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))) +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))
by A17, A20, Th24, SCMPDS_4:24
.=
DataPart (Computation ((s +* (Initialized (stop (I ';' J)))) +* ((Initialized (stop I)) +* (Initialized (stop (I ';' J))))),(LifeSpan (s +* (Initialized (stop I)))))
by FUNCT_4:15
.=
DataPart (Computation ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))
by Th17
.=
DataPart (Computation (s +* ((Initialized (stop (I ';' J))) +* (Initialized (stop (I ';' J))))),(LifeSpan (s +* (Initialized (stop I)))))
by FUNCT_4:15
.=
DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))
by A1, A24, Th24, SCMPDS_4:24
;
then DataPart ((Computation ((s +* (Initialized (stop (I ';' J)))) +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))) =
(DataPart (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) +* (DataPart (Initialized (stop J)))
by FUNCT_4:75
.=
DataPart ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))
by FUNCT_4:75
;
hence
(
DataPart (Computation (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = DataPart (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) &
IC (Computation (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) = (IC (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) + (card I) )
by A21, A23, SCMPDS_4:84;
:: thesis: verum
end;
A25:
DataPart (IExec (I ';' J),s) = DataPart (IExec J,(IExec I,s))
proof
thus DataPart (IExec (I ';' J),s) =
DataPart (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))))
by A4, A11, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.=
DataPart (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))
by A22, AMI_1:51
.=
DataPart (IExec J,(IExec I,s))
by A4, A13, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
;
:: thesis: verum
end;
A26:
Result (s +* (Initialized (stop I))) = Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))
by A1, AMI_1:122, SCMPDS_4:63;
A27:
Initialized (stop J) c= (Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))
by FUNCT_4:26;
Initialized (stop J) c= (IExec I,s) +* (Initialized (stop J))
by FUNCT_4:26;
then A28:
IC (Result ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J)))) = IC (Result ((IExec I,s) +* (Initialized (stop J))))
by A4, A5, A26, A27, Th21, AMI_1:121;
A29: IC (IExec (I ';' J),s) =
IC (Result (s +* (Initialized (stop (I ';' J)))))
by Th22
.=
IC (Computation (s +* (Initialized (stop (I ';' J)))),(LifeSpan (s +* (Initialized (stop (I ';' J))))))
by A2, AMI_1:122, SCMPDS_4:63
.=
IC (Computation (s +* (Initialized (stop (I ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + (LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))))
by A10, Th37
.=
(IC (Computation ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))),(LifeSpan ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J)))))) + (card I)
by A22, AMI_1:51
.=
(IC (Result ((Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) +* (Initialized (stop J))))) + (card I)
by A3, AMI_1:122, SCMPDS_4:63
.=
(IC (Result ((Result (s +* (Initialized (stop I)))) +* (Initialized (stop J))))) + (card I)
by A1, AMI_1:122, SCMPDS_4:63
.=
(IC (IExec J,(IExec I,s))) + (card I)
by A28, Th22
;
hereby :: thesis: verum
A30:
dom (IExec (I ';' J),s) =
the
carrier of
SCMPDS
by AMI_1:79
.=
dom ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I))))
by AMI_1:79
;
reconsider l =
(IC (IExec J,(IExec I,s))) + (card I) as
Instruction-Location of
SCMPDS ;
A31:
dom (Start-At l) = {(IC SCMPDS )}
by FUNCOP_1:19;
now let x be
set ;
:: thesis: ( 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)))) . b1 )assume A32:
x in dom (IExec (I ';' J),s)
;
:: thesis: (IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1per cases
( x is Int_position or x = IC SCMPDS or x is Instruction-Location of SCMPDS )
by A32, SCMPDS_4:20;
suppose A33:
x is
Int_position
;
:: thesis: (IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1then A34:
(IExec (I ';' J),s) . x = (IExec J,(IExec I,s)) . x
by A25, SCMPDS_4:23;
x <> IC SCMPDS
by A33, SCMPDS_2:52;
then
not
x in dom (Start-At l)
by A31, TARSKI:def 1;
hence
(IExec (I ';' J),s) . x = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . x
by A34, FUNCT_4:12;
:: thesis: verum end; suppose A37:
x is
Instruction-Location of
SCMPDS
;
:: thesis: (IExec (I ';' J),s) . b1 = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . b1(IExec (I ';' J),s) | NAT =
s | NAT
by CARD_3:99
.=
(IExec J,(IExec I,s)) | NAT
by A12, CARD_3:99
;
then A38:
(IExec (I ';' J),s) . x = (IExec J,(IExec I,s)) . x
by A37, SCMPDS_4:21;
x <> IC SCMPDS
by A37, AMI_1:48;
then
not
x in dom (Start-At l)
by A31, TARSKI:def 1;
hence
(IExec (I ';' J),s) . x = ((IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))) . x
by A38, FUNCT_4:12;
:: thesis: verum end; end; hence
IExec (I ';' J),
s = (IExec J,(IExec I,s)) +* (Start-At ((IC (IExec J,(IExec I,s))) + (card I)))
by A30, FUNCT_1:9;
:: thesis: verum
end;