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 being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
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 being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
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 being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) )
assume that
A1: ( NPP p c= s1 & NPP p c= s2 ) and
A2: ( ProgramPart p c= P1 & ProgramPart p c= P2 ) ; :: thesis: for i being Element of NAT
for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
B1: ( NPP p c= s1 & NPP p c= s2 ) by A1, XBOOLE_1:1;
let i be Element of NAT ; :: thesis: for k1, k2 being Integer
for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let k1, k2 be Integer; :: thesis: for a, b being Int_position st CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p holds
(Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
let a, b be Int_position ; :: thesis: ( CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) & a in dom p & DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p implies (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) )
set I = CurInstr (P1,(Comput (P1,s1,i)));
set Cs1i = Comput (P1,s1,i);
set Cs2i = Comput (P2,s2,i);
assume that
A3: CurInstr (P1,(Comput (P1,s1,i))) = (a,k1) := (b,k2) and
A4: a in dom p and
A5: DataLoc (((Comput (P1,s1,i)) . a),k1) in dom p ; :: thesis: (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2))
( a in dom (NPP p) implies ( ((Comput (P1,s1,i)) | (dom (NPP p))) . a = (Comput (P1,s1,i)) . a & ((Comput (P2,s2,i)) | (dom (NPP p))) . a = (Comput (P2,s2,i)) . a ) ) by FUNCT_1:72;
then A6: (Comput (P1,s1,i)) . a = (Comput (P2,s2,i)) . a by A4, EXTPRO_1:def 9, A2, Lm1, B1;
set Cs1i1 = Comput (P1,s1,(i + 1));
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))) ;
then A7: (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) by A3, SCMPDS_2:59;
set Cs2i1 = Comput (P2,s2,(i + 1));
A8: 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))) ;
A9: ( DataLoc (((Comput (P1,s1,i)) . a),k1) in dom (NPP p) implies ( ((Comput (P1,s1,(i + 1))) | (dom (NPP p))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P1,s1,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) & ((Comput (P2,s2,(i + 1))) | (dom (NPP p))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) = (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P1,s1,i)) . a),k1)) ) ) by FUNCT_1:72;
CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) by A1, AMISTD_5:7, A2;
then (Comput (P2,s2,(i + 1))) . (DataLoc (((Comput (P2,s2,i)) . a),k1)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) by A8, A3, SCMPDS_2:59;
hence (Comput (P1,s1,i)) . (DataLoc (((Comput (P1,s1,i)) . b),k2)) = (Comput (P2,s2,i)) . (DataLoc (((Comput (P2,s2,i)) . b),k2)) by A9, A5, A6, A7, EXTPRO_1:def 9, A2, Lm1, B1; :: thesis: verum