let a be Int_position; :: thesis: for k1 being Integer holds JUMP ((a,k1) <=0_goto 5) = {}
let k1 be Integer; :: thesis: JUMP ((a,k1) <=0_goto 5) = {}
set k2 = 5;
set i = (a,k1) <=0_goto 5;
set X = { (NIC (((a,k1) <=0_goto 5),l)) where l is Nat : verum } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {} c= JUMP ((a,k1) <=0_goto 5)

set nl2 = 8;
set nl1 = 5;
let x be object ; :: thesis: ( x in JUMP ((a,k1) <=0_goto 5) implies b₁ in {} )
assume A1: x in JUMP ((a,k1) <=0_goto 5) ; :: thesis: b₁ in {}
set l2 = 8;
NIC (((a,k1) <=0_goto 5),8) in { (NIC (((a,k1) <=0_goto 5),l)) where l is Nat : verum } ;
then x in NIC (((a,k1) <=0_goto 5),8) by A1, SETFAM_1:def 1;
then consider s2 being Element of product (the_Values_of SCMPDS) such that
A2: x = IC (Exec (((a,k1) <=0_goto 5),s2)) and
A3: IC s2 = 8 ;
set l1 = 5;
NIC (((a,k1) <=0_goto 5),5) in { (NIC (((a,k1) <=0_goto 5),l)) where l is Nat : verum } ;
then x in NIC (((a,k1) <=0_goto 5),5) by A1, SETFAM_1:def 1;
then consider s1 being Element of product (the_Values_of SCMPDS) such that
A4: x = IC (Exec (((a,k1) <=0_goto 5),s1)) and
A5: IC s1 = 5 ;
consider m2 being Element of NAT such that
A6: m2 = IC s2 and
A7: ICplusConst (s2,5) = |.(m2 + 5).| by SCMPDS_2:def 18;
consider m1 being Element of NAT such that
A8: m1 = IC s1 and
A9: ICplusConst (s1,5) = |.(m1 + 5).| by SCMPDS_2:def 18;

per cases ( ( s1 . (DataLoc ((s1 . a),k1)) <= 0 & s2 . (DataLoc ((s2 . a),k1)) <= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) > 0 & s2 . (DataLoc ((s2 . a),k1)) > 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) > 0 & s2 . (DataLoc ((s2 . a),k1)) <= 0 ) or ( s1 . (DataLoc ((s1 . a),k1)) <= 0 & s2 . (DataLoc ((s2 . a),k1)) > 0 ) ) ;

suppose that A10: s1 . (DataLoc ((s1 . a),k1)) <= 0 and
A11: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; :: thesis: b₁ in {}

A12: x = |.(m2 + 5).| by A2, A7, A11, SCMPDS_2:56;
x = |.(m1 + 5).| by A4, A9, A10, SCMPDS_2:56;
then ( 5 + 5 = 8 + 5 or 5 + 5 = - (8 + 5) ) by A5, A8, A3, A6, A12, ABSVALUE:28;
hence x in {} ; :: thesis: verum

end;

suppose that A13: s1 . (DataLoc ((s1 . a),k1)) > 0 and
A14: s2 . (DataLoc ((s2 . a),k1)) > 0 ; :: thesis: b₁ in {}

A15: x = 8 + 1 by A2, A3, A14, SCMPDS_2:56;
x = 5 + 1 by A4, A5, A13, SCMPDS_2:56;
hence x in {} by A15; :: thesis: verum

end;

suppose that A16: s1 . (DataLoc ((s1 . a),k1)) > 0 and
A17: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; :: thesis: b₁ in {}

reconsider n1 = 5 as Element of NAT ;
set w1 = n1;
A18: x = |.(m2 + 5).| by A2, A7, A17, SCMPDS_2:56;
x = n1 + 1 by A4, A5, A16, SCMPDS_2:56
.= n1 + 1 ;
then ( n1 + 1 = m2 + 5 or n1 + 1 = - (m2 + 5) ) by A18, ABSVALUE:1;
hence x in {} by A3, A6; :: thesis: verum

end;

suppose that A19: s1 . (DataLoc ((s1 . a),k1)) <= 0 and
A20: s2 . (DataLoc ((s2 . a),k1)) > 0 ; :: thesis: b₁ in {}

reconsider n2 = 8 as Element of NAT ;
A21: x = n2 + 1 by A2, A3, A20, SCMPDS_2:56
.= n2 + 1 ;
set w2 = n2;
x = |.(m1 + 5).| by A4, A9, A19, SCMPDS_2:56;
then ( n2 + 1 = m1 + 5 or n2 + 1 = - (m1 + 5) ) by A21, ABSVALUE:1;
hence x in {} by A5, A8; :: thesis: verum

end;

end;

end;

thus {} c= JUMP ((a,k1) <=0_goto 5) ; :: thesis: verum