let l be Element of NAT ; :: thesis: for k being Integer holds NIC ((goto k),l) = {(abs (k + l))}
let k be Integer; :: thesis: NIC ((goto k),l) = {(abs (k + l))}
set s = the State of SCMPDS;
set i = goto k;
set t = abs (k + l);
set I = goto k;
reconsider n = l as Element of NAT ;
reconsider il1 = l as Element of ObjectKind (IC ) by MEMSTR_0:def 3;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(abs (k + l))} c= NIC ((goto k),l)

let x be set ; :: thesis: ( x in NIC ((goto k),l) implies x in {(abs (k + l))} )
assume x in NIC ((goto k),l) ; :: thesis: x in {(abs (k + l))}
then consider s being Element of product the Object-Kind of SCMPDS such that
A1: x = IC (Exec ((goto k),s)) and
A2: IC s = l ;
A3: ex m1 being Element of NAT st
( m1 = IC s & ICplusConst (s,k) = abs (m1 + k) ) by SCMPDS_2:def 18;
x = abs (k + l) by A1, A2, A3, SCMPDS_2:54;
hence x in {(abs (k + l))} by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {(abs (k + l))} or x in NIC ((goto k),l) )
reconsider u = the n -started State of SCMPDS as Element of product the Object-Kind of SCMPDS by CARD_3:107;
A4: IC u = n by MEMSTR_0:def 8;
consider m1 being Element of NAT such that
A5: m1 = IC u and
A6: ICplusConst (u,k) = abs (m1 + k) by SCMPDS_2:def 18;
assume x in {(abs (k + l))} ; :: thesis: x in NIC ((goto k),l)
then x = abs (m1 + k) by A4, A5, TARSKI:def 1
.= IC (Exec ((goto k),u)) by A6, SCMPDS_2:54 ;
hence x in NIC ((goto k),l) by A4; :: thesis: verum