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 Element of 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 set ; :: 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 Element of 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 Object-Kind 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 Element of 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 Object-Kind of SCMPDS such that
A5: x = IC (Exec (((a,k1) <>0_goto 5),s1)) and
A6: IC s1 = 5 ;
consider m2 being Element of NAT such that
A8: m2 = IC s2 and
A9: ICplusConst (s2,5) = abs (m2 + 5) by SCMPDS_2:def 20;
consider m1 being Element of NAT such that
A10: m1 = IC s1 and
A11: ICplusConst (s1,5) = abs (m1 + 5) by SCMPDS_2:def 20;

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 A12: s1 . (DataLoc ((s1 . a),k1)) <> 0 and
A13: s2 . (DataLoc ((s2 . a),k1)) <> 0 ; :: thesis: b₁ in {}

A14: x = abs (m2 + 5) by A2, A9, A13, SCMPDS_2:67;
x = abs (m1 + 5) by A5, A11, A12, SCMPDS_2:67;
then ( 5 + 5 = 8 + 5 or 5 + 5 = - (8 + 5) ) by A6, A10, A3, A8, A14, ABSVALUE:45;
hence x in {} ; :: thesis: verum

end;

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

A17: x = succ 8 by A2, A3, A16, SCMPDS_2:67;
x = succ 5 by A5, A6, A15, SCMPDS_2:67;
hence x in {} by A17; :: thesis: verum

end;

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

reconsider n1 = 5 as Element of NAT ;
set w1 = n1;
A20: x = abs (m2 + 5) by A2, A9, A19, SCMPDS_2:67;
x = succ n1 by A5, A6, A18, SCMPDS_2:67
.= n1 + 1 ;
then ( n1 + 1 = m2 + 5 or n1 + 1 = - (m2 + 5) ) by A20, ABSVALUE:1;
hence x in {} by A3, A8; :: thesis: verum

end;

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

reconsider n2 = 8 as Element of NAT ;
A23: x = succ n2 by A2, A3, A22, SCMPDS_2:67
.= n2 + 1 ;
set w2 = n2;
x = abs (m1 + 5) by A5, A11, A21, SCMPDS_2:67;
then ( n2 + 1 = m1 + 5 or n2 + 1 = - (m1 + 5) ) by A23, ABSVALUE:1;
hence x in {} by A6, A10; :: thesis: verum

end;

end;

end;

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