reconsider m1 = IC s as Element of NAT by AMI_1:def 4;
consider k being Element of NAT such that
A1: m1 = k ;
reconsider m = abs (k + c) as Nat ;
reconsider l = m as Instruction-Location of SCMPDS by AMI_1:def 4;
take l ; :: thesis: ex m being Element of NAT st
( m = IC s & l = abs (m + c) )
thus ex m being Element of NAT st
( m = IC s & l = abs (m + c) ) by A1; :: thesis: verum