let P1, P2 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for s1, s2 being State of SCMPDS
for I being Program of SCMPDS st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( NPP (Comput ((P1 +* (stop I)),(Initialize s1),k)) = NPP (Comput ((P2 +* (stop I)),(Initialize s2),k)) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )
let s1, s2 be State of SCMPDS; :: thesis: for I being Program of SCMPDS st I is_closed_on s1,P1 & DataPart s1 = DataPart s2 holds
for k being Element of NAT holds
( NPP (Comput ((P1 +* (stop I)),(Initialize s1),k)) = NPP (Comput ((P2 +* (stop I)),(Initialize s2),k)) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )
let I be Program of SCMPDS; :: thesis: ( I is_closed_on s1,P1 & DataPart s1 = DataPart s2 implies for k being Element of NAT holds
( NPP (Comput ((P1 +* (stop I)),(Initialize s1),k)) = NPP (Comput ((P2 +* (stop I)),(Initialize s2),k)) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) ) )
assume A1: I is_closed_on s1,P1 ; :: thesis: ( not DataPart s1 = DataPart s2 or for k being Element of NAT holds
( NPP (Comput ((P1 +* (stop I)),(Initialize s1),k)) = NPP (Comput ((P2 +* (stop I)),(Initialize s2),k)) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) ) )
set pI = stop I;
set ss1 = Initialize s1;
set PP1 = P1 +* (stop I);
set ss2 = Initialize s2;
set PP2 = P2 +* (stop I);
stop I c= P2 +* (stop I) by FUNCT_4:26;
then A5: stop I c= P2 +* (stop I) ;
stop I c= P1 +* (stop I) by FUNCT_4:26;
then A6: stop I c= P1 +* (stop I) ;
assume A7: DataPart s1 = DataPart s2 ; :: thesis: for k being Element of NAT holds
( NPP (Comput ((P1 +* (stop I)),(Initialize s1),k)) = NPP (Comput ((P2 +* (stop I)),(Initialize s2),k)) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )
let k be Element of NAT ; :: thesis: ( NPP (Comput ((P1 +* (stop I)),(Initialize s1),k)) = NPP (Comput ((P2 +* (stop I)),(Initialize s2),k)) & CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) )
A8: IC (Comput ((P1 +* (stop I)),(Initialize s1),k)) in dom (stop I) by A1, SCMPDS_6:def 2;
A9: I is_closed_on s2,P2 by A1, A7, SCMPDS_6:36;
then A10: for m being Element of NAT st m < k holds
IC (Comput ((P2 +* (stop I)),(Initialize s2),m)) in dom (stop I) by SCMPDS_6:def 2;
NPP (Initialize s1) = NPP (Initialize s2) by A7, SCMPDS_6:12;
hence NPP (Comput ((P1 +* (stop I)),(Initialize s1),k)) = NPP (Comput ((P2 +* (stop I)),(Initialize s2),k)) by A6, A5, A10, SCMPDS_4:67; :: thesis: CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) = CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k)))
then A11: IC (Comput ((P1 +* (stop I)),(Initialize s1),k)) = IC (Comput ((P2 +* (stop I)),(Initialize s2),k)) by COMPOS_1:230;
A12: IC (Comput ((P2 +* (stop I)),(Initialize s2),k)) in dom (stop I) by A9, SCMPDS_6:def 2;
A13: (P2 +* (stop I)) /. (IC (Comput ((P2 +* (stop I)),(Initialize s2),k))) = (P2 +* (stop I)) . (IC (Comput ((P2 +* (stop I)),(Initialize s2),k))) by PBOOLE:158;
A14: (P1 +* (stop I)) /. (IC (Comput ((P1 +* (stop I)),(Initialize s1),k))) = (P1 +* (stop I)) . (IC (Comput ((P1 +* (stop I)),(Initialize s1),k))) by PBOOLE:158;
thus CurInstr ((P2 +* (stop I)),(Comput ((P2 +* (stop I)),(Initialize s2),k))) = (P2 +* (stop I)) . (IC (Comput ((P2 +* (stop I)),(Initialize s2),k))) by A13
.= (stop I) . (IC (Comput ((P2 +* (stop I)),(Initialize s2),k))) by A5, A12, GRFUNC_1:8
.= (P1 +* (stop I)) . (IC (Comput ((P1 +* (stop I)),(Initialize s1),k))) by A6, A11, A8, GRFUNC_1:8
.= CurInstr ((P1 +* (stop I)),(Comput ((P1 +* (stop I)),(Initialize s1),k))) by A14 ; :: thesis: verum