let l be Instruction-Location of SCMPDS ; :: 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 ;
set i = goto k;
set t = abs (k + l);
reconsider I = goto k as Element of ObjectKind l by AMI_1:def 14;
l in NAT by AMI_1:def 4;
then reconsider il1 = l as Element of ObjectKind (IC SCMPDS ) by AMI_1:def 11;
set u = s +* ((IC SCMPDS ),l --> il1,I);
A1: (s +* ((IC SCMPDS ),l --> il1,I)) . l = 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 State of such that
A3: x = IC (Following s) and
A4: IC s = l and
A5: 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;
x = (Exec (goto k),s) . (IC SCMPDS ) by A3, A4, A5, 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 (s +* ((IC SCMPDS ),l --> il1,I)) = l by AMI_1:129;
consider m1 being Element of NAT such that
A8: m1 = IC (s +* ((IC SCMPDS ),l --> il1,I)) and
A9: ICplusConst (s +* ((IC SCMPDS ),l --> il1,I)),k = abs (m1 + k) by SCMPDS_2:def 20;
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),(s +* ((IC SCMPDS ),l --> il1,I))) . (IC SCMPDS ) by A9, SCMPDS_2:66
.= IC (Following (s +* ((IC SCMPDS ),l --> il1,I))) by A1, A7, AMI_1:131 ;
hence x in NIC (goto k),l by A1, A7; :: thesis: verum