let s1, s2 be State of SCMPDS ; :: thesis: for n, m being Element of 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 Element of 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:16;
ex n1 being Element of NAT st
( n1 = IC s1 & ICplusConst s1,k1 = abs (n1 + k1) ) by SCMPDS_2:def 20;
then ( ex n2 being Element of NAT st
( n2 = IC s2 & ICplusConst s2,k1 = abs (n2 + k1) ) & nk = mk ) by A1, ABSVALUE:def 1, SCMPDS_2:def 20;
hence (ICplusConst s1,k1) + n = ICplusConst s2,k1 by A1, A3, ABSVALUE:def 1; :: thesis: verum