let s1, s2 be State of SCMPDS ; :: thesis: for k1, k2, m being Integer st IC s1 = IC s2 & k1 <> k2 & m = IC s1 & m + k1 >= 0 & m + k2 >= 0 holds
ICplusConst s1,k1 <> ICplusConst s2,k2
let k1, k2, m be Integer; :: thesis: ( IC s1 = IC s2 & k1 <> k2 & m = IC s1 & m + k1 >= 0 & m + k2 >= 0 implies ICplusConst s1,k1 <> ICplusConst s2,k2 )
assume that
A1: IC s1 = IC s2 and
A2: k1 <> k2 and
A3: m = IC s1 and
A4: m + k1 >= 0 and
A5: m + k2 >= 0 ; :: thesis: ICplusConst s1,k1 <> ICplusConst s2,k2
ex i being Element of NAT st
( i = IC s1 & ICplusConst s1,k1 = abs (i + k1) ) by SCMPDS_2:def 20;
then A6: ICplusConst s1,k1 = m + k1 by A3, A4, ABSVALUE:def 1;
assume A7: ICplusConst s1,k1 = ICplusConst s2,k2 ; :: thesis: contradiction
ex j being Element of NAT st
( j = IC s2 & ICplusConst s2,k2 = abs (j + k2) ) by SCMPDS_2:def 20;
then ICplusConst s2,k2 = m + k2 by A1, A3, A5, ABSVALUE:def 1;
hence contradiction by A2, A7, A6; :: thesis: verum