let s1, s2 be State of SCMPDS; for k1, k2 being Nat st IC s1 = IC s2 & k1 <> k2 holds
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
let k1, k2 be Nat; ( 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;
A1:
((m + 2) - 2) + k1 >= 0
;
A2:
((m + 2) - 2) + k2 >= 0
;
assume
( IC s1 = IC s2 & k1 <> k2 )
; ICplusConst (s1,k1) <> ICplusConst (s2,k2)
hence
ICplusConst (s1,k1) <> ICplusConst (s2,k2)
by A1, A2, Th7; verum