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 (Following (ProgramPart s1),s1) and
A6: IC s1 = (abs k2) + x1 and
A7: (ProgramPart s1) /. ((abs k2) + x1) = a,k1 <=0_goto k2 ;
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 (Following (ProgramPart s2),s2) and
A11: IC s2 = ((abs k2) + x1) + x1 and
A12: (ProgramPart s2) /. (((abs k2) + x1) + x1) = a,k1 <=0_goto k2 ;
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;
Y: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by AMI_1:150;
Z: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by AMI_1:150;

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 = (Exec (a,k1 <=0_goto k2),s2) . (IC SCMPDS ) by A10, A11, A12, AMI_1:131, Y
.= abs (m2 + k2) by A14, A16, SCMPDS_2:68 ;
A18: x = (Exec (a,k1 <=0_goto k2),s1) . (IC SCMPDS ) by A5, A6, A7, AMI_1:131, Z
.= abs (m1 + k2) by A9, A15, SCMPDS_2:68 ;
thus x in {} :: thesis: verum

proof

per cases ( ((abs k2) + x1) + k2 = (((abs k2) + x1) + x1) + 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) + k2 = (((abs k2) + x1) + x1) + 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 = (Exec (a,k1 <=0_goto k2),s2) . (IC SCMPDS ) by A10, A11, A12, AMI_1:131, Y
.= succ (((abs k2) + x1) + x1) by A11, A20, SCMPDS_2:68 ;
x = (Exec (a,k1 <=0_goto k2),s1) . (IC SCMPDS ) by A5, A6, A7, AMI_1:131, Z
.= succ ((abs k2) + x1) by A6, A19, SCMPDS_2:68 ;
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 = (Exec (a,k1 <=0_goto k2),s2) . (IC SCMPDS ) by A10, A11, A12, AMI_1:131, Y
.= abs (m2 + k2) by A14, A23, SCMPDS_2:68 ;
A25: x = (Exec (a,k1 <=0_goto k2),s1) . (IC SCMPDS ) by A5, A6, A7, AMI_1:131, Z
.= succ n1 by A6, A22, SCMPDS_2:68
.= 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 = (Exec (a,k1 <=0_goto k2),s2) . (IC SCMPDS ) by A10, A11, A12, AMI_1:131, Y
.= succ n2 by A11, A27, SCMPDS_2:68
.= n2 + 1 ;
set w2 = n2;
A29: x = (Exec (a,k1 <=0_goto k2),s1) . (IC SCMPDS ) by A5, A6, A7, AMI_1:131, Z
.= abs (m1 + k2) by A9, A26, SCMPDS_2:68 ;
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