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) = {} )
assume A1: k2 <> 5 ; :: thesis: 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 Instruction-Location of SCMPDS : verum } ;

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

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 {}
set x1 = ((- k2) + (abs k2)) + 4;
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 = inspos ((abs k2) + x1);
NIC (a,k1 <=0_goto k2),(inspos ((abs k2) + x1)) in { (NIC (a,k1 <=0_goto k2),l) where l is Instruction-Location of SCMPDS : verum } ;
then x in NIC (a,k1 <=0_goto k2),(inspos ((abs k2) + x1)) by A2, SETFAM_1:def 1;
then consider s1 being State of SCMPDS such that
A5: x = IC (Following s1) and
A6: IC s1 = inspos ((abs k2) + x1) and
A7: s1 . (inspos ((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;
A10: m1 = (abs k2) + x1 by A6, A8;
set l2 = inspos (((abs k2) + x1) + x1);
NIC (a,k1 <=0_goto k2),(inspos (((abs k2) + x1) + x1)) in { (NIC (a,k1 <=0_goto k2),l) where l is Instruction-Location of SCMPDS : verum } ;
then x in NIC (a,k1 <=0_goto k2),(inspos (((abs k2) + x1) + x1)) by A2, SETFAM_1:def 1;
then consider s2 being State of SCMPDS such that
A11: x = IC (Following s2) and
A12: IC s2 = inspos (((abs k2) + x1) + x1) and
A13: s2 . (inspos (((abs k2) + x1) + x1)) = a,k1 <=0_goto k2 ;
consider m2 being Element of NAT such that
A14: m2 = IC s2 and
A15: ICplusConst s2,k2 = abs (m2 + k2) by SCMPDS_2:def 20;
A16: m2 = ((abs k2) + x1) + x1 by A12, A14;

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

A20: x = (Exec (a,k1 <=0_goto k2),s1) . (IC SCMPDS ) by A5, A6, A7, AMI_1:131
.= abs (m1 + k2) by A9, A18, SCMPDS_2:68 ;
A21: x = (Exec (a,k1 <=0_goto k2),s2) . (IC SCMPDS ) by A11, A12, A13, AMI_1:131
.= abs (m2 + k2) by A15, A19, 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 A10, A16, A20, A21, 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 Lm5; :: thesis: verum

end;

end;

end;

end;

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

A24: x = (Exec (a,k1 <=0_goto k2),s1) . (IC SCMPDS ) by A5, A6, A7, AMI_1:131
.= Next (inspos ((abs k2) + x1)) by A6, A22, SCMPDS_2:68 ;
x = (Exec (a,k1 <=0_goto k2),s2) . (IC SCMPDS ) by A11, A12, A13, AMI_1:131
.= Next (inspos (((abs k2) + x1) + x1)) by A12, A23, SCMPDS_2:68 ;
hence x in {} by A3, ABSVALUE:44, A24; :: thesis: verum

end;

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

reconsider n1 = inspos ((abs k2) + x1) as Element of NAT ;
set w1 = n1;
A29: x = (Exec (a,k1 <=0_goto k2),s1) . (IC SCMPDS ) by A5, A6, A7, AMI_1:131
.= succ n1 by A6, A25, SCMPDS_2:68
.= n1 + 1 ;
A30: x = (Exec (a,k1 <=0_goto k2),s2) . (IC SCMPDS ) by A11, A12, A13, AMI_1:131
.= abs (m2 + k2) by A15, A26, SCMPDS_2:68 ;
thus x in {} :: thesis: verum

proof

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

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

then ((abs k2) + x1) + 1 = ((abs k2) + x1) + (x1 + k2) by A16;
hence x in {} by Lm6; :: thesis: verum

end;

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

hence x in {} by A4, A16, Lm7; :: thesis: verum

end;

end;

end;

end;

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

reconsider n2 = inspos (((abs k2) + x1) + x1) as Element of NAT ;
set w2 = n2;
A35: x = (Exec (a,k1 <=0_goto k2),s1) . (IC SCMPDS ) by A5, A6, A7, AMI_1:131
.= abs (m1 + k2) by A9, A31, SCMPDS_2:68 ;
A36: x = (Exec (a,k1 <=0_goto k2),s2) . (IC SCMPDS ) by A11, A12, A13, AMI_1:131
.= succ n2 by A12, A32, SCMPDS_2:68
.= n2 + 1 ;
thus x in {} :: thesis: verum

proof

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

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

hence x in {} by A1, A10, Lm8; :: thesis: verum

end;

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

hence x in {} by A4, A10, Lm9; :: thesis: verum

end;

end;

end;

end;

end;

end;

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