let n be Element of NAT ; :: thesis: for R being good Ring
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st p c= s1 & p c= s2 holds
( IC (Comput ((ProgramPart s1),s1,n)) = IC (Comput ((ProgramPart s2),s2,n)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) )
let R be good Ring; :: thesis: for s1, s2 being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st p c= s1 & p c= s2 holds
( IC (Comput ((ProgramPart s1),s1,n)) = IC (Comput ((ProgramPart s2),s2,n)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) )
let s1, s2 be State of (SCM R); :: thesis: ( not R is trivial implies for p being non NAT -defined autonomic FinPartState of st p c= s1 & p c= s2 holds
( IC (Comput ((ProgramPart s1),s1,n)) = IC (Comput ((ProgramPart s2),s2,n)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) ) )
assume A1: not R is trivial ; :: thesis: for p being non NAT -defined autonomic FinPartState of st p c= s1 & p c= s2 holds
( IC (Comput ((ProgramPart s1),s1,n)) = IC (Comput ((ProgramPart s2),s2,n)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) )
set Cs2i = Comput ((ProgramPart s2),s2,n);
set Cs1i = Comput ((ProgramPart s1),s1,n);
let p be non NAT -defined autonomic FinPartState of ; :: thesis: ( p c= s1 & p c= s2 implies ( IC (Comput ((ProgramPart s1),s1,n)) = IC (Comput ((ProgramPart s2),s2,n)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) ) )
assume that
A2: p c= s1 and
A3: p c= s2 ; :: thesis: ( IC (Comput ((ProgramPart s1),s1,n)) = IC (Comput ((ProgramPart s2),s2,n)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) )
ProgramPart p c= p by RELAT_1:88;
then A4: dom (ProgramPart p) c= dom p by GRFUNC_1:8;
thus A5: IC (Comput ((ProgramPart s1),s1,n)) = IC (Comput ((ProgramPart s2),s2,n)) :: thesis: CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n)))

proof

assume A6: IC (Comput ((ProgramPart s1),s1,n)) <> IC (Comput ((ProgramPart s2),s2,n)) ; :: thesis: contradiction
( ((Comput ((ProgramPart s1),s1,n)) | (dom p)) . (IC (SCM R)) = (Comput ((ProgramPart s1),s1,n)) . (IC (SCM R)) & ((Comput ((ProgramPart s2),s2,n)) | (dom p)) . (IC (SCM R)) = (Comput ((ProgramPart s2),s2,n)) . (IC (SCM R)) ) by A1, Th25, FUNCT_1:72;
hence contradiction by A2, A3, A6, EXTPRO_1:def 9; :: thesis: verum

end;

IC (Comput ((ProgramPart s2),s2,n)) in dom (ProgramPart p) by A1, A3, Th27;
then A7: ((Comput ((ProgramPart s2),s2,n)) | (dom p)) . (IC (Comput ((ProgramPart s2),s2,n))) = (Comput ((ProgramPart s2),s2,n)) . (IC (Comput ((ProgramPart s2),s2,n))) by A4, FUNCT_1:72;
Y: (ProgramPart (Comput ((ProgramPart s1),s1,n))) /. (IC (Comput ((ProgramPart s1),s1,n))) = (Comput ((ProgramPart s1),s1,n)) . (IC (Comput ((ProgramPart s1),s1,n))) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart s2),s2,n))) /. (IC (Comput ((ProgramPart s2),s2,n))) = (Comput ((ProgramPart s2),s2,n)) . (IC (Comput ((ProgramPart s2),s2,n))) by COMPOS_1:38;
IC (Comput ((ProgramPart s1),s1,n)) in dom (ProgramPart p) by A1, A2, Th27;
then A8: ((Comput ((ProgramPart s1),s1,n)) | (dom p)) . (IC (Comput ((ProgramPart s1),s1,n))) = (Comput ((ProgramPart s1),s1,n)) . (IC (Comput ((ProgramPart s1),s1,n))) by A4, FUNCT_1:72;
assume not CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) ; :: thesis: contradiction
hence contradiction by A2, A3, A5, A8, A7, Y, Z, EXTPRO_1:def 9; :: thesis: verum