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 (SCM R) st p c= s1 & p c= s2 holds
( IC (Computation s1,n) = IC (Computation s2,n) & CurInstr (Computation s1,n) = CurInstr (Computation 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 (SCM R) st p c= s1 & p c= s2 holds
( IC (Computation s1,n) = IC (Computation s2,n) & CurInstr (Computation s1,n) = CurInstr (Computation 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 (SCM R) st p c= s1 & p c= s2 holds
( IC (Computation s1,n) = IC (Computation s2,n) & CurInstr (Computation s1,n) = CurInstr (Computation s2,n) ) )
assume A1: not R is trivial ; :: thesis: for p being non NAT -defined autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 holds
( IC (Computation s1,n) = IC (Computation s2,n) & CurInstr (Computation s1,n) = CurInstr (Computation s2,n) )
let p be non NAT -defined autonomic FinPartState of (SCM R); :: thesis: ( p c= s1 & p c= s2 implies ( IC (Computation s1,n) = IC (Computation s2,n) & CurInstr (Computation s1,n) = CurInstr (Computation s2,n) ) )
assume A2: ( p c= s1 & p c= s2 ) ; :: thesis: ( IC (Computation s1,n) = IC (Computation s2,n) & CurInstr (Computation s1,n) = CurInstr (Computation s2,n) )
set Cs1i = Computation s1,n;
set Cs2i = Computation s2,n;
thus A3: IC (Computation s1,n) = IC (Computation s2,n) :: thesis: CurInstr (Computation s1,n) = CurInstr (Computation s2,n)

proof

assume A4: IC (Computation s1,n) <> IC (Computation s2,n) ; :: thesis: contradiction
( ((Computation s1,n) | (dom p)) . (IC (SCM R)) = (Computation s1,n) . (IC (SCM R)) & ((Computation s2,n) | (dom p)) . (IC (SCM R)) = (Computation s2,n) . (IC (SCM R)) ) by A1, Th38, FUNCT_1:72;
hence contradiction by A2, A4, AMI_1:def 25; :: thesis: verum

end;

assume A5: not CurInstr (Computation s1,n) = CurInstr (Computation s2,n) ; :: thesis: contradiction
A6: ( IC (Computation s1,n) in dom (ProgramPart p) & IC (Computation s2,n) in dom (ProgramPart p) ) by A1, A2, Th40;
ProgramPart p c= p by RELAT_1:88;
then dom (ProgramPart p) c= dom p by GRFUNC_1:8;
then ( ((Computation s1,n) | (dom p)) . (IC (Computation s1,n)) = (Computation s1,n) . (IC (Computation s1,n)) & ((Computation s2,n) | (dom p)) . (IC (Computation s2,n)) = (Computation s2,n) . (IC (Computation s2,n)) ) by A6, FUNCT_1:72;
hence contradiction by A2, A3, A5, AMI_1:def 25; :: thesis: verum