let a be Int_position ; :: thesis: for k2, k1 being Integer st k2 <> 5 holds
JUMP ((a,k1) >=0_goto k2) = {}
let k2, k1 be Integer; :: thesis: ( k2 <> 5 implies JUMP ((a,k1) >=0_goto k2) = {} )
set i = (a,k1) >=0_goto k2;
set X = { (NIC (((a,k1) >=0_goto k2),l)) where l is Element of NAT : verum } ;
assume A1: k2 <> 5 ; :: thesis: JUMP ((a,k1) >=0_goto k2) = {}

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

set x1 = ((- k2) + (abs k2)) + 4;
let x be set ; :: thesis: ( x in JUMP ((a,k1) >=0_goto k2) implies b₁ in {} )
assume A2: x in JUMP ((a,k1) >=0_goto k2) ; :: thesis: b₁ in {}
A3: ((- k2) + (abs k2)) + 4 > ((- k2) + (abs k2)) + 0 by XREAL_1:8;
then A4: ((- k2) + (abs k2)) + 4 > 0 by ABSVALUE:44;
then reconsider x1 = ((- k2) + (abs k2)) + 4 as Element of NAT by INT_1:16;
set nl1 = (abs k2) + x1;
set nl2 = ((abs k2) + x1) + x1;
set l1 = (abs k2) + x1;
set l2 = ((abs k2) + x1) + x1;
NIC (((a,k1) >=0_goto k2),((abs k2) + x1)) in { (NIC (((a,k1) >=0_goto k2),l)) where l is Element of NAT : verum } ;
then x in NIC (((a,k1) >=0_goto k2),((abs k2) + x1)) by A2, 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 k2),s1)) and
A6: IC s1 = (abs k2) + x1 ;
consider m1 being Element of NAT such that
A8: m1 = IC s1 and
A9: ICplusConst (s1,k2) = abs (m1 + k2) by SCMPDS_2:def 20;
NIC (((a,k1) >=0_goto k2),(((abs k2) + x1) + x1)) in { (NIC (((a,k1) >=0_goto k2),l)) where l is Element of NAT : verum } ;
then x in NIC (((a,k1) >=0_goto k2),(((abs k2) + x1) + x1)) by A2, SETFAM_1:def 1;
then consider s2 being Element of product the Object-Kind of SCMPDS such that
A10: x = IC (Exec (((a,k1) >=0_goto k2),s2)) and
A11: IC s2 = ((abs k2) + x1) + x1 ;
consider m2 being Element of NAT such that
A13: m2 = IC s2 and
A14: ICplusConst (s2,k2) = abs (m2 + k2) 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 A15: s1 . (DataLoc ((s1 . a),k1)) >= 0 and
A16: s2 . (DataLoc ((s2 . a),k1)) >= 0 ; :: thesis: b₁ in {}

A17: x = abs (m2 + k2) by A10, A14, A16, SCMPDS_2:69;
A18: x = abs (m1 + k2) by A5, A9, A15, SCMPDS_2:69;
thus x in {} :: thesis: verum

proof

per cases ( ((((abs k2) + x1) + 2) - 2) + k2 = (((((abs k2) + x1) + x1) + 2) - 2) + k2 or ((((abs k2) + x1) + 2) - 2) + k2 = - ((((((abs k2) + x1) + x1) + 2) - 2) + k2) ) by A6, A8, A11, A13, A18, A17, ABSVALUE:45;

suppose ((((abs k2) + x1) + 2) - 2) + k2 = (((((abs k2) + x1) + x1) + 2) - 2) + k2 ; :: thesis: x in {}

hence x in {} by A3, ABSVALUE:44; :: thesis: verum

end;

suppose ((((abs k2) + x1) + 2) - 2) + k2 = - ((((((abs k2) + x1) + x1) + 2) - 2) + k2) ; :: thesis: x in {}

hence x in {} by Lm4; :: thesis: verum

end;

end;

end;

end;

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

A21: x = succ (((abs k2) + x1) + x1) by A10, A11, A20, SCMPDS_2:69;
x = succ ((abs k2) + x1) by A5, A6, A19, SCMPDS_2:69;
hence x in {} by A3, A21, ABSVALUE:44; :: thesis: verum

end;

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

reconsider n1 = (abs k2) + x1 as Element of NAT ;
set w1 = n1;
A24: x = abs (m2 + k2) by A10, A14, A23, SCMPDS_2:69;
A25: x = succ n1 by A5, A6, A22, SCMPDS_2:69
.= n1 + 1 ;
thus x in {} :: thesis: verum

proof

per cases ( n1 + 1 = m2 + k2 or n1 + 1 = - (m2 + k2) ) by A25, A24, ABSVALUE:1;

suppose n1 + 1 = m2 + k2 ; :: thesis: x in {}

then ((abs k2) + x1) + 1 = ((abs k2) + x1) + (x1 + k2) by A11, A13;
hence x in {} by Lm5; :: thesis: verum

end;

suppose n1 + 1 = - (m2 + k2) ; :: thesis: x in {}

hence x in {} by A4, A11, A13, Lm6; :: thesis: verum

end;

end;

end;

end;

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

reconsider n2 = ((abs k2) + x1) + x1 as Element of NAT ;
A28: x = succ n2 by A10, A11, A27, SCMPDS_2:69
.= n2 + 1 ;
set w2 = n2;
A29: x = abs (m1 + k2) by A5, A9, A26, SCMPDS_2:69;
thus x in {} :: thesis: verum

proof

per cases ( n2 + 1 = m1 + k2 or n2 + 1 = - (m1 + k2) ) by A29, A28, ABSVALUE:1;

suppose n2 + 1 = m1 + k2 ; :: thesis: x in {}

hence x in {} by A1, A6, A8, Lm7; :: thesis: verum

end;

suppose n2 + 1 = - (m1 + k2) ; :: thesis: x in {}

hence x in {} by A4, A6, A8, Lm8; :: thesis: verum

end;

end;

end;

end;

end;

end;

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