let a be Int_position; :: thesis: JUMP (return a) = { k where k is Nat : k > 1 }
set A = { k where k is Nat : k > 1 } ;
set i = return a;
set X = { (NIC ((return a),l)) where l is Nat : verum } ;
JUMP (return a) c= NIC ((return a),0) by AMISTD_1:19;
hence JUMP (return a) c= { k where k is Nat : k > 1 } by Th4; :: according to XBOOLE_0:def 10 :: thesis: { k where k is Nat : k > 1 } c= JUMP (return a)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : k > 1 } or x in JUMP (return a) )
assume A1: x in { k where k is Nat : k > 1 } ; :: thesis: x in JUMP (return a)

now :: thesis: ( { (NIC ((return a),l)) where l is Nat : verum } <> {} & ( for y being set st y in { (NIC ((return a),l)) where l is Nat : verum } holds
x in y ) )

consider k being Nat such that
A2: x = k and
A3: k > 1 by A1;
reconsider k2 = k - 2 as Element of NAT by A3, Lm2;
NIC ((return a),0) in { (NIC ((return a),l)) where l is Nat : verum } ;
hence { (NIC ((return a),l)) where l is Nat : verum } <> {} ; :: thesis: for y being set st y in { (NIC ((return a),l)) where l is Nat : verum } holds
x in y
a in SCM-Data-Loc by AMI_2:def 16;
then consider j being Nat such that
A4: a = [1,j] by AMI_2:23;
set t = [1,(j + 1)];
set s = the State of SCMPDS;
let y be set ; :: thesis: ( y in { (NIC ((return a),l)) where l is Nat : verum } implies x in y )
A5: DataLoc (j,1) = [1,|.(j + 1).|]
.= [1,(j + 1)] by ABSVALUE:def 1 ;
[1,(j + 1)] in SCM-Data-Loc by AMI_2:24;
then reconsider t1 = [1,(j + 1)] as Int_position by AMI_2:def 16;
assume y in { (NIC ((return a),l)) where l is Nat : verum } ; :: thesis: x in y
then consider l being Nat such that
A6: y = NIC ((return a),l) ;
reconsider n = l as Element of NAT by ORDINAL1:def 12;
set I = return a;
reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
A7: IC u = n by MEMSTR_0:def 11;
set g = (a,t1) --> (j,k2);
reconsider v = u +* ((a,t1) --> (j,k2)) as Element of product (the_Values_of SCMPDS) by CARD_3:107;
j <> j + 1 ;
then A8: a <> t1 by A4, XTUPLE_0:1;
then A9: v . a = j by FUNCT_4:84;
A10: v . t1 = k2 by A8, FUNCT_4:84;
A11: dom ((a,t1) --> (j,k2)) = {a,t1} by FUNCT_4:62;
( a <> IC & t1 <> IC ) by SCMPDS_2:43;
then A12: not IC in dom ((a,t1) --> (j,k2)) by A11, TARSKI:def 2;
A13: IC v = l by A7, A12, FUNCT_4:11;
x = k2 + 2 by A2
.= |.(v . (DataLoc (j,1))).| + 2 by A10, A5, ABSVALUE:def 1
.= IC (Exec ((return a),v)) by A9, SCMPDS_2:58, SCMPDS_I:def 14 ;
hence x in y by A6, A13; :: thesis: verum

end;

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