let a be Int_position ; :: thesis: JUMP (return a) = { k where k is Element of NAT : k > 1 }
set A = { k where k is Element of NAT : k > 1 } ;
set i = return a;
set X = { (NIC (return a),l) where l is Instruction-Location of SCMPDS : verum } ;
JUMP (return a) c= NIC (return a),(inspos 0 ) by AMISTD_1:58;
hence JUMP (return a) c= { k where k is Element of NAT : k > 1 } by Th10; :: according to XBOOLE_0:def 10 :: thesis: { k where k is Element of NAT : k > 1 } c= JUMP (return a)
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 JUMP (return a) )
assume A1: x in { k where k is Element of NAT : k > 1 } ; :: thesis: x in JUMP (return a)

now

consider k being Element of NAT such that
A2: x = k and
A3: k > 1 by A1;
reconsider k2 = k - 2 as Element of NAT by A3, Lm1;
NIC (return a),(inspos 0 ) in { (NIC (return a),l) where l is Instruction-Location of SCMPDS : verum } ;
hence { (NIC (return a),l) where l is Instruction-Location of SCMPDS : verum } <> {} ; :: thesis: for y being set st y in { (NIC (return a),l) where l is Instruction-Location of SCMPDS : verum } holds
x in y
a in SCM-Data-Loc by SCMPDS_2:def 2;
then consider j being Element of NAT such that
A4: a = [1,j] by AMI_2:32;
set t = [1,(j + 1)];
consider s being State of ;
let y be set ; :: thesis: ( y in { (NIC (return a),l) where l is Instruction-Location of SCMPDS : verum } implies x in y )
A5: DataLoc j,1 = [1,(abs (j + 1))] by SCMPDS_2:def 4
.= [1,(j + 1)] by ABSVALUE:def 1 ;
reconsider t1 = [1,(j + 1)] as Int_position by AMI_2:33, SCMPDS_2:9;
assume y in { (NIC (return a),l) where l is Instruction-Location of SCMPDS : verum } ; :: thesis: x in y
then consider l being Instruction-Location of SCMPDS such that
A6: y = NIC (return a),l ;
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);
A7: (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 ;
set g = a,t1 --> j,k2;
set v = (s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2);
j <> j + 1 ;
then A8: a <> t1 by A4, ZFMISC_1:33;
then A9: ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) . a = j by FUNCT_4:89;
A10: ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) . t1 = k2 by A8, FUNCT_4:89;
A11: dom (a,t1 --> j,k2) = {a,t1} by FUNCT_4:65;
( l <> a & l <> t1 ) by SCMPDS_2:53;
then ( (s +* ((IC SCMPDS ),l --> il1,I)) . l = return a & not l in dom (a,t1 --> j,k2) ) by A11, AMI_1:129, TARSKI:def 2;
then A12: ((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) . l = return a by 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 A11, 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 A7, A13, FUNCT_4:12 ;
x = k2 + 2 by A2
.= (abs (((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2)) . (DataLoc j,1))) + 2 by A10, A5, ABSVALUE:def 1
.= (Exec (return a),((s +* ((IC SCMPDS ),l --> il1,I)) +* (a,t1 --> j,k2))) . (IC SCMPDS ) by A9, 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 y by A6, A12, A14; :: thesis: verum

end;

hence x in JUMP (return a) by SETFAM_1:def 1; :: thesis: verum