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