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