let s1, s2 be State of SCMPDS; :: thesis: for n, m being Nat

for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds

(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)

let n, m be Nat; :: thesis: for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds

(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)

let k1 be Integer; :: thesis: ( IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 implies (ICplusConst (s1,k1)) + n = ICplusConst (s2,k1) )

assume that

A1: IC s1 = m and

A2: m + k1 >= 0 and

A3: (IC s1) + n = IC s2 ; :: thesis: (ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)

reconsider nk = ICplusConst (s1,k1) as Element of NAT ;

reconsider mk = m + k1 as Element of NAT by A2, INT_1:3;

ex n1 being Element of NAT st

( n1 = IC s1 & ICplusConst (s1,k1) = |.(n1 + k1).| ) by SCMPDS_2:def 18;

then ( ex n2 being Element of NAT st

( n2 = IC s2 & ICplusConst (s2,k1) = |.(n2 + k1).| ) & nk = mk ) by A1, ABSVALUE:def 1, SCMPDS_2:def 18;

hence (ICplusConst (s1,k1)) + n = ICplusConst (s2,k1) by A1, A3, ABSVALUE:def 1; :: thesis: verum

for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds

(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)

let n, m be Nat; :: thesis: for k1 being Integer st IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 holds

(ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)

let k1 be Integer; :: thesis: ( IC s1 = m & m + k1 >= 0 & (IC s1) + n = IC s2 implies (ICplusConst (s1,k1)) + n = ICplusConst (s2,k1) )

assume that

A1: IC s1 = m and

A2: m + k1 >= 0 and

A3: (IC s1) + n = IC s2 ; :: thesis: (ICplusConst (s1,k1)) + n = ICplusConst (s2,k1)

reconsider nk = ICplusConst (s1,k1) as Element of NAT ;

reconsider mk = m + k1 as Element of NAT by A2, INT_1:3;

ex n1 being Element of NAT st

( n1 = IC s1 & ICplusConst (s1,k1) = |.(n1 + k1).| ) by SCMPDS_2:def 18;

then ( ex n2 being Element of NAT st

( n2 = IC s2 & ICplusConst (s2,k1) = |.(n2 + k1).| ) & nk = mk ) by A1, ABSVALUE:def 1, SCMPDS_2:def 18;

hence (ICplusConst (s1,k1)) + n = ICplusConst (s2,k1) by A1, A3, ABSVALUE:def 1; :: thesis: verum