let s1, s2 be State of SCMPDS; :: thesis: for k1, k2 being Element of NAT st IC s1 = IC s2 & k1 <> k2 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
let k1, k2 be Element of NAT ; :: thesis: ( IC s1 = IC s2 & k1 <> k2 implies ICplusConst (s1,k1) <> ICplusConst (s2,k2) )
reconsider m = IC s1 as Element of NAT ;
set mm = m + 2;
((m + 2) - 2) + k1 = m + k1 ;
then A1: ((m + 2) - 2) + k1 >= 0 by NAT_1:2;
((m + 2) - 2) + k2 = m + k2 ;
then A2: ((m + 2) - 2) + k2 >= 0 by NAT_1:2;
assume ( IC s1 = IC s2 & k1 <> k2 ) ; :: thesis: ICplusConst (s1,k1) <> ICplusConst (s2,k2)
hence ICplusConst (s1,k1) <> ICplusConst (s2,k2) by A1, A2, Th18; :: thesis: verum