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) = |.(i + k1).| ) by SCMPDS_2:def 18;
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) = |.(j + k2).| ) by SCMPDS_2:def 18;
then ICplusConst (s2,k2) = m + k2 by A1, A3, A5, ABSVALUE:def 1;
hence contradiction by A2, A7, A6; :: thesis: verum