let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of S st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of b₁ -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting IC-recognized AMI-Struct of N; :: thesis: ( S is CurIns-recognized implies for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of S st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )
assume A1: S is CurIns-recognized ; :: thesis: for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of S st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let p be non NAT -defined autonomic FinPartState of ; :: thesis: for s1, s2 being State of S st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let s1, s2 be State of S; :: thesis: ( NPP p c= s1 & NPP p c= s2 implies for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )
assume that
A2: NPP p c= s1 and
A3: NPP p c= s2 ; :: thesis: for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
let P1, P2 be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( ProgramPart p c= P1 & ProgramPart p c= P2 implies for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) ) )
assume that
A4: ProgramPart p c= P1 and
A5: ProgramPart p c= P2 ; :: thesis: for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
A6: dom (ProgramPart p) c= dom P1 by A4, RELAT_1:25;
A7: dom (ProgramPart p) c= dom P2 by A5, RELAT_1:25;
A8: IC in dom p by Th6;
let i be Element of NAT ; :: thesis: ( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
A9: IC (Comput (P1,s1,i)) in dom (ProgramPart p) by A4, Def4, A1, A2;
A10: IC (Comput (P2,s2,i)) in dom (ProgramPart p) by A5, Def4, A1, A3;
thus A11: IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) :: thesis: CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i)))

proof

assume A12: IC (Comput (P1,s1,i)) <> IC (Comput (P2,s2,i)) ; :: thesis: contradiction
( ((Comput (P1,s1,i)) | (dom (NPP p))) . (IC ) = (Comput (P1,s1,i)) . (IC ) & ((Comput (P2,s2,i)) | (dom (NPP p))) . (IC ) = (Comput (P2,s2,i)) . (IC ) ) by A8, COMPOS_1:179, FUNCT_1:72;
hence contradiction by A12, A4, A5, A2, A3, EXTPRO_1:def 9; :: thesis: verum

end;

thus CurInstr (P1,(Comput (P1,s1,i))) = P1 . (IC (Comput (P1,s1,i))) by A9, A6, PARTFUN1:def 8
.= (ProgramPart p) . (IC (Comput (P1,s1,i))) by A9, A4, GRFUNC_1:8
.= P2 . (IC (Comput (P2,s2,i))) by A10, A5, A11, GRFUNC_1:8
.= CurInstr (P2,(Comput (P2,s2,i))) by A10, A7, PARTFUN1:def 8 ; :: thesis: verum