let P1, P2 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of SCMPDS st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let p be non NAT -defined autonomic FinPartState of ; :: thesis: for s1, s2 being State of SCMPDS st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let s1, s2 be State of SCMPDS; :: thesis: ( NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p c= P2 implies for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 ) )
assume that
A1: ( NPP p c= s1 & NPP p c= s2 ) and
A2: ( ProgramPart p c= P1 & ProgramPart p c= P2 ) ; :: thesis: for i, m being Element of NAT
for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
B1: ( NPP p c= s1 & NPP p c= s2 ) by A1, XBOOLE_1:1;
let i, m be Element of NAT ; :: thesis: for a being Int_position
for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let a be Int_position ; :: thesis: for k1, k2 being Integer st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 holds
( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
let k1, k2 be Integer; :: thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 & m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 implies ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 ) )
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i1 = Comput (P2,s2,(i + 1));
A3: ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & (Comput (P1,s1,(i + 1))) | (dom (NPP p)) = (Comput (P2,s2,(i + 1))) | (dom (NPP p)) ) by A1, AMISTD_5:7, EXTPRO_1:def 9, A2, B1;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A5: m + 1 >= 0 by NAT_1:2;
IC in dom p by AMISTD_5:6;
then IC in dom (NPP p) by COMPOS_1:179;
then A6: ( ((Comput (P1,s1,(i + 1))) | (dom (NPP p))) . (IC ) = (Comput (P1,s1,(i + 1))) . (IC ) & ((Comput (P2,s2,(i + 1))) | (dom (NPP p))) . (IC ) = (Comput (P2,s2,(i + 1))) . (IC ) ) by FUNCT_1:72;
A7: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A8: CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) <>0_goto k2 and
A9: ( m = IC (Comput (P1,s1,i)) & m + k2 >= 0 & k2 <> 1 ) ; :: thesis: ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 )
A10: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, AMISTD_5:7, A2;

A11: now

assume that
A12: (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 and
A13: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) <> 0 ; :: thesis: contradiction
A14: (Comput (P1,s1,(i + 1))) . (IC ) = ICplusConst ((Comput (P1,s1,i)),k2) by A4, A8, A13, SCMPDS_2:67;
(Comput (P2,s2,(i + 1))) . (IC ) = succ (IC (Comput (P2,s2,i))) by A10, A7, A8, A12, SCMPDS_2:67
.= ICplusConst ((Comput (P2,s2,i)),1) by Th20 ;
hence contradiction by A6, A3, A9, A5, A14, Th18; :: thesis: verum

end;

now

assume that
A15: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 and
A16: (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) <> 0 ; :: thesis: contradiction
A17: (Comput (P2,s2,(i + 1))) . (IC ) = ICplusConst ((Comput (P2,s2,i)),k2) by A10, A7, A8, A16, SCMPDS_2:67;
(Comput (P1,s1,(i + 1))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A4, A8, A15, SCMPDS_2:67
.= ICplusConst ((Comput (P1,s1,i)),1) by Th20 ;
hence contradiction by A6, A3, A9, A5, A17, Th18; :: thesis: verum

end;

hence ( (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = 0 iff (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = 0 ) by A11; :: thesis: verum