let a be Int_position ; :: thesis: for l being Element of NAT holds NIC ((return a),l) = { k where k is Element of NAT : k > 1 }
let l be Element of NAT ; :: thesis: NIC ((return a),l) = { k where k is Element of NAT : k > 1 }
consider s being State of SCMPDS;
set X = { k where k is Element of NAT : k > 1 } ;
set i = return a;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { k where k is Element of NAT : k > 1 } c= NIC ((return a),l)

let x be set ; :: thesis: ( x in NIC ((return a),l) implies x in { k where k is Element of NAT : k > 1 } )
assume x in NIC ((return a),l) ; :: thesis: x in { k where k is Element of NAT : k > 1 }
then consider s being Element of product the Object-Kind of SCMPDS such that
A1: x = IC (Exec ((return a),s)) and
IC s = l ;
reconsider k = x as Element of NAT by A1;
A4: (abs (s . (DataLoc ((s . a),1)))) + 2 >= 0 + 2 by XREAL_1:8;
k >= 1 + 1 by A4, A1, SCMPDS_1:def 23, SCMPDS_2:70;
then k > 1 by NAT_1:13;
hence x in { k where k is Element of NAT : k > 1 } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : k > 1 } or x in NIC ((return a),l) )
reconsider I = return a as Element of the Object-Kind of SCMPDS . l by COMPOS_1:def 8;
reconsider n = l as Element of NAT ;
assume x in { k where k is Element of NAT : k > 1 } ; :: thesis: x in NIC ((return a),l)
then consider k being Element of NAT such that
A5: x = k and
A6: k > 1 ;
reconsider il1 = l as Element of ObjectKind (IC SCMPDS) by COMPOS_1:def 6;
reconsider k2 = k - 2 as Element of NAT by A6, Lm1;
((IC SCMPDS),l) --> (il1,I) = ((IC SCMPDS) .--> il1) +* (l .--> I) by FUNCT_4:def 4;
then reconsider u = s +* (((IC SCMPDS),l) --> (il1,I)) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;
A7: u . (IC SCMPDS) = IC u
.= n by EXTPRO_1:26 ;
a in SCM-Data-Loc by SCMPDS_2:def 2;
then consider j being Element of NAT such that
A8: a = [1,j] by AMI_2:32;
set t = [1,(j + 1)];
reconsider t1 = [1,(j + 1)] as Int_position by AMI_2:33, SCMPDS_2:9;
A9: DataLoc (j,1) = [1,(abs (j + 1))] by SCMPDS_2:def 4
.= [1,(j + 1)] by ABSVALUE:def 1 ;
set g = (a,t1) --> (j,k2);
reconsider v = u +* ((a,t1) --> (j,k2)) as Element of product the Object-Kind of SCMPDS by PBOOLE:155;
A10: dom ((a,t1) --> (j,k2)) = {a,[1,(j + 1)]} by FUNCT_4:65;
j <> j + 1 ;
then A11: a <> [1,(j + 1)] by A8, ZFMISC_1:33;
then A12: v . a = j by FUNCT_4:89;
( a <> IC SCMPDS & t1 <> IC SCMPDS ) by SCMPDS_2:52;
then A14: not IC SCMPDS in dom ((a,t1) --> (j,k2)) by A10, TARSKI:def 2;
A15: IC v = l by A7, A14, FUNCT_4:12;
A16: v . [1,(j + 1)] = k2 by A11, FUNCT_4:89;
x = k2 + 2 by A5
.= (abs (v . (DataLoc (j,1)))) + 2 by A16, A9, ABSVALUE:def 1
.= IC (Exec ((return a),v)) by A12, SCMPDS_1:def 23, SCMPDS_2:70 ;
hence x in NIC ((return a),l) by A15; :: thesis: verum