let s be State of SCMPDS; :: thesis: for m1, m2 being Nat st IC s = m1 + m2 holds
ICplusConst (s,(- m2)) = m1
let m1, m2 be 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)) = |.(m + (- m2)).| by SCMPDS_2:def 18;
A4: m = m1 + m2 by A1, A2
.= m1 + m2 ;
thus ICplusConst (s,(- m2)) = m1 by A3, A4, ABSVALUE:def 1
.= m1
.= m1 ; :: thesis: verum