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)

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 ) )

hence
x in JUMP (return a)
by SETFAM_1:def 1; :: thesis: verumx 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;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