let s1, s2 be State of SCMPDS ; for I being Program of SCMPDS st I is_closed_on s1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k, Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (ProgramPart (s1 +* (Initialized (stop I)))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) = CurInstr (ProgramPart (s2 +* (Initialized (stop I)))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) )
let I be Program of SCMPDS ; ( I is_closed_on s1 & DataPart s1 = DataPart s2 implies for k being Element of NAT holds
( Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k, Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (ProgramPart (s1 +* (Initialized (stop I)))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) = CurInstr (ProgramPart (s2 +* (Initialized (stop I)))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) ) )
assume A1:
I is_closed_on s1
; ( not DataPart s1 = DataPart s2 or for k being Element of NAT holds
( Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k, Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (ProgramPart (s1 +* (Initialized (stop I)))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) = CurInstr (ProgramPart (s2 +* (Initialized (stop I)))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) ) )
set pI = stop I;
set IsI = Initialized (stop I);
set ss1 = s1 +* (Initialized (stop I));
set ss2 = s2 +* (Initialized (stop I));
A2:
stop I c= Initialized (stop I)
by SCMPDS_4:9;
Initialized (stop I) c= s2 +* (Initialized (stop I))
by FUNCT_4:26;
then A3:
stop I c= s2 +* (Initialized (stop I))
by A2, XBOOLE_1:1;
Initialized (stop I) c= s1 +* (Initialized (stop I))
by FUNCT_4:26;
then A4:
stop I c= s1 +* (Initialized (stop I))
by A2, XBOOLE_1:1;
assume A5:
DataPart s1 = DataPart s2
; for k being Element of NAT holds
( Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k, Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (ProgramPart (s1 +* (Initialized (stop I)))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) = CurInstr (ProgramPart (s2 +* (Initialized (stop I)))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) )
let k be Element of NAT ; ( Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k, Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k equal_outside NAT & CurInstr (ProgramPart (s1 +* (Initialized (stop I)))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) = CurInstr (ProgramPart (s2 +* (Initialized (stop I)))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) )
A6:
IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) in dom (stop I)
by A1, SCMPDS_6:def 2;
A7:
I is_closed_on s2
by A1, A5, SCMPDS_6:36;
then A8:
for m being Element of NAT st m < k holds
IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),m) in dom (stop I)
by SCMPDS_6:def 2;
s1 +* (Initialized (stop I)),s2 +* (Initialized (stop I)) equal_outside NAT
by A5, SCMPDS_6:12;
hence
Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k, Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k equal_outside NAT
by A4, A3, A8, SCMPDS_4:67; CurInstr (ProgramPart (s1 +* (Initialized (stop I)))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) = CurInstr (ProgramPart (s2 +* (Initialized (stop I)))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k)
then A9:
IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) = IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k)
by AMI_1:121;
A10:
IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) in dom (stop I)
by A7, SCMPDS_6:def 2;
Y:
(ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k)) /. (IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k)) = (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) . (IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k))
by AMI_1:150;
Z:
(ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k)) /. (IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k)) = (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k) . (IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k))
by AMI_1:150;
TX2:
ProgramPart (s2 +* (Initialized (stop I))) = ProgramPart (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k)
by AMI_1:123;
TX1:
ProgramPart (s1 +* (Initialized (stop I))) = ProgramPart (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k)
by AMI_1:123;
thus CurInstr (ProgramPart (s2 +* (Initialized (stop I)))),(Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k) =
(s2 +* (Initialized (stop I))) . (IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k))
by Y, TX2, AMI_1:54
.=
(stop I) . (IC (Comput (ProgramPart (s2 +* (Initialized (stop I)))),(s2 +* (Initialized (stop I))),k))
by A3, A10, GRFUNC_1:8
.=
(s1 +* (Initialized (stop I))) . (IC (Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k))
by A4, A9, A6, GRFUNC_1:8
.=
CurInstr (ProgramPart (s1 +* (Initialized (stop I)))),(Comput (ProgramPart (s1 +* (Initialized (stop I)))),(s1 +* (Initialized (stop I))),k)
by Z, TX1, AMI_1:54
; verum