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))}
consider s being State of SCMPDS ;
set i = goto k;
set t = abs (k + l);
reconsider I = goto k as Element of the Object-Kind of SCMPDS . l by COMPOS_1:def 8;
reconsider n = l as Element of NAT ;
reconsider il1 = l as Element of ObjectKind (IC SCMPDS ) by COMPOS_1:def 6;
X: ((IC SCMPDS ) .--> il1) +* (l .--> (goto k)) is the Object-Kind of SCMPDS -compatible PartState of SCMPDS ;
(IC SCMPDS ),l --> il1,I = ((IC SCMPDS ) .--> il1) +* (l .--> I) by FUNCT_4:def 4;
then reconsider u = s +* ((IC SCMPDS ),l --> il1,(goto k)) as Element of product the Object-Kind of SCMPDS by X, PBOOLE:155;
A1: u . n = goto k by AMI_1:129;

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
A3: x = IC (Following (ProgramPart s),s) and
A4: IC s = l and
A5: (ProgramPart s) /. l = goto k ;
A6: ex m1 being Element of NAT st
( m1 = IC s & ICplusConst s,k = abs (m1 + k) ) by SCMPDS_2:def 20;
(ProgramPart s) . l = goto k by A5, PBOOLE:158;
then x = (Exec (goto k),s) . (IC SCMPDS ) by A3, A4, AMI_1:131
.= abs (k + l) by A4, A6, SCMPDS_2:66 ;
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 )
A7: IC u = n by AMI_1:129;
consider m1 being Element of NAT such that
A8: m1 = IC u and
A9: ICplusConst u,k = abs (m1 + k) by SCMPDS_2:def 20;
X: (ProgramPart u) /. l = u . l by COMPOS_1:38;
Y: (ProgramPart u) . l = u . l by COMPOS_1:2;
assume x in {(abs (k + l))} ; :: thesis: x in NIC (goto k),l
then x = abs (m1 + k) by A7, A8, TARSKI:def 1
.= (Exec (goto k),u) . (IC SCMPDS ) by A9, SCMPDS_2:66
.= IC (Following (ProgramPart u),u) by A1, A7, Y, AMI_1:131 ;
hence x in NIC (goto k),l by A1, A7, X; :: thesis: verum