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 } ;

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)

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

set nl1 = 5;

let x be object ; :: thesis: ( x in JUMP ((a,k1) <=0_goto 5) implies b_{1} in {} )

assume A1: x in JUMP ((a,k1) <=0_goto 5) ; :: thesis: b_{1} 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;

end;set nl1 = 5;

let x be object ; :: thesis: ( x in JUMP ((a,k1) <=0_goto 5) implies b

assume A1: x in JUMP ((a,k1) <=0_goto 5) ; :: thesis: b

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 ) )
;

end;

suppose that A10:
s1 . (DataLoc ((s1 . a),k1)) <= 0
and

A11: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; :: thesis: b_{1} in {}

A11: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; :: thesis: b

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;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

suppose that A13:
s1 . (DataLoc ((s1 . a),k1)) > 0
and

A14: s2 . (DataLoc ((s2 . a),k1)) > 0 ; :: thesis: b_{1} in {}

A14: s2 . (DataLoc ((s2 . a),k1)) > 0 ; :: thesis: b

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;x = 5 + 1 by A4, A5, A13, SCMPDS_2:56;

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

suppose that A16:
s1 . (DataLoc ((s1 . a),k1)) > 0
and

A17: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; :: thesis: b_{1} in {}

A17: s2 . (DataLoc ((s2 . a),k1)) <= 0 ; :: thesis: b

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;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

suppose that A19:
s1 . (DataLoc ((s1 . a),k1)) <= 0
and

A20: s2 . (DataLoc ((s2 . a),k1)) > 0 ; :: thesis: b_{1} in {}

A20: s2 . (DataLoc ((s2 . a),k1)) > 0 ; :: thesis: b

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;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