let a be Int_position; :: thesis: JUMP () = { k where k is Nat : k > 1 }
set A = { k where k is Nat : k > 1 } ;
set i = return a;
set X = { (NIC ((),l)) where l is Nat : verum } ;
JUMP () c= NIC ((),0) by AMISTD_1:19;
hence JUMP () 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 ()
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : k > 1 } or x in JUMP () )
assume A1: x in { k where k is Nat : k > 1 } ; :: thesis: x in JUMP ()
now :: thesis: ( { (NIC ((),l)) where l is Nat : verum } <> {} & ( for y being set st y in { (NIC ((),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 ;
NIC ((),0) in { (NIC ((),l)) where l is Nat : verum } ;
hence { (NIC ((),l)) where l is Nat : verum } <> {} ; :: thesis: for y being set st y in { (NIC ((),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 ((),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 ((),l)) where l is Nat : verum } ; :: thesis: x in y
then consider l being Nat such that
A6: y = NIC ((),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 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 by CARD_3:107;
j <> j + 1 ;
then A8: a <> t1 by ;
then A9: v . a = j by FUNCT_4:84;
A10: v . t1 = k2 by ;
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 ;
A13: IC v = l by ;
x = k2 + 2 by A2
.= |.(v . (DataLoc (j,1))).| + 2 by
.= IC (Exec ((),v)) by ;
hence x in y by ; :: thesis: verum
end;
hence x in JUMP () by SETFAM_1:def 1; :: thesis: verum