let s be State of SCMPDS; :: thesis: for m1, m2 being Element of NAT st IC s = m1 + m2 holds
ICplusConst (s,(- m2)) = m1
let m1, m2 be Element of NAT ; :: thesis: ( IC s = m1 + m2 implies ICplusConst (s,(- m2)) = m1 )
assume A1: IC s = m1 + m2 ; :: thesis: ICplusConst (s,(- m2)) = m1
consider m being Element of NAT such that
A2: m = IC s and
A3: ICplusConst (s,(- m2)) = abs (m + (- m2)) by SCMPDS_2:def 18;
A4: m = m1 + m2 by A1, A2
.= m1 + m2 ;
m1 >= 0 by NAT_1:2;
hence ICplusConst (s,(- m2)) = m1 by A3, A4, ABSVALUE:def 1
.= m1
.= m1 ;
:: thesis: verum