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

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 State of SCMPDS such that
A1: x = IC (Following s) and
A2: IC s = l and
A3: s . l = return a ;
A4: x = (Exec (return a),s) . (IC SCMPDS ) by A1, A2, A3, AMI_1:131
.= (abs (s . (DataLoc (s . a),1))) + 2 by SCMPDS_1:def 23, SCMPDS_2:70 ;
x in NAT by A1, AMI_1:def 4;
then consider k being Element of NAT such that
A5: x = k ;
(abs (s . (DataLoc (s . a),1))) + 2 >= 0 + 2 by XREAL_1:8;
then k >= 1 + 1 by A4, A5;
then k > 1 by NAT_1:13;
hence x in { k where k is Element of NAT : k > 1 } by A5; :: 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 )
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
A6: x = k and
A7: k > 1 ;
reconsider k2 = k - 2 as Element of NAT by A7, Lm2;
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;
consider s being State of SCMPDS ;
l in NAT by AMI_1:def 4;
then reconsider il1 = l as Element of ObjectKind (IC SCMPDS ) by AMI_1:def 11;
reconsider I = return a as Element of ObjectKind l by AMI_1:def 14;
set u = s +* ((IC SCMPDS ),l --> il1,I);
set t = [1,(j + 1)];
reconsider t1 = [1,(j + 1)] as Int_position by AMI_2:33, SCMPDS_2:9;
set g = a,t1 --> j,k2;
set v = (s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2);
A9: dom (a,t1 --> j,k2) = {a,[1,(j + 1)]} by FUNCT_4:65;
A10: (s +* ((IC SCMPDS ),l --> il1,I)) . l = return a by AMI_1:129;
A11: (s +* ((IC SCMPDS ),l --> il1,I)) . (IC SCMPDS ) = IC (s +* ((IC SCMPDS ),l --> il1,I)) by AMI_1:def 15
.= l by AMI_1:129 ;
( l <> a & l <> t1 ) by SCMPDS_2:53;
then not l in dom (a,t1 --> j,k2) by A9, TARSKI:def 2;
then A12: ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) . l = return a by A10, FUNCT_4:12;
( a <> IC SCMPDS & t1 <> IC SCMPDS ) by SCMPDS_2:52;
then A13: not IC SCMPDS in dom (a,t1 --> j,k2) by A9, TARSKI:def 2;
A14: IC ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) = ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) . (IC SCMPDS ) by AMI_1:def 15
.= l by A11, A13, FUNCT_4:12 ;
j <> j + 1 ;
then A15: a <> [1,(j + 1)] by A8, ZFMISC_1:33;
then A16: ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) . a = j by FUNCT_4:89;
A17: ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) . [1,(j + 1)] = k2 by A15, FUNCT_4:89;
A18: DataLoc j,1 = [1,(abs (j + 1))] by SCMPDS_2:def 4
.= [1,(j + 1)] by ABSVALUE:def 1 ;
x = k2 + 2 by A6
.= (abs (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) . (DataLoc j,1))) + 2 by A17, ABSVALUE:def 1, A18
.= (Exec (return a),((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2))) . (IC SCMPDS ) by A16, SCMPDS_1:def 23, SCMPDS_2:70
.= IC (Following ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2))) by A12, A14, AMI_1:131 ;
hence x in NIC (return a),l by A12, A14; :: thesis: verum