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