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 } ;
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 object ; :: thesis: ( x in JUMP ((a,k1) >=0_goto 5) implies b1 in {} )
assume A1: x in JUMP ((a,k1) >=0_goto 5) ; :: thesis: b1 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 ;
then consider s2 being Element of product 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 ;
then consider s1 being Element of product 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 ) ) ;
suppose that A10: s1 . (DataLoc ((s1 . a),k1)) >= 0 and
A11: s2 . (DataLoc ((s2 . a),k1)) >= 0 ; :: thesis: b1 in {}
A12: x = |.(m2 + 5).| by ;
x = |.(m1 + 5).| by ;
then ( ((5 + 2) - 2) + 5 = ((8 + 2) - 2) + 5 or ((5 + 2) - 2) + 5 = - (((8 + 2) - 2) + 5) ) by ;
hence x in {} ; :: thesis: verum
end;
suppose that A13: s1 . (DataLoc ((s1 . a),k1)) < 0 and
A14: s2 . (DataLoc ((s2 . a),k1)) < 0 ; :: thesis: b1 in {}
A15: x = 8 + 1 by ;
x = 5 + 1 by ;
hence x in {} by A15; :: thesis: verum
end;
suppose that A16: s1 . (DataLoc ((s1 . a),k1)) < 0 and
A17: s2 . (DataLoc ((s2 . a),k1)) >= 0 ; :: thesis: b1 in {}
reconsider n1 = 5 as Element of NAT ;
set w1 = n1;
A18: x = |.(m2 + 5).| by ;
x = n1 + 1 by
.= n1 + 1 ;
then ( n1 + 1 = m2 + 5 or n1 + 1 = - (m2 + 5) ) by ;
hence x in {} by A3, A6; :: thesis: verum
end;
suppose that A19: s1 . (DataLoc ((s1 . a),k1)) >= 0 and
A20: s2 . (DataLoc ((s2 . a),k1)) < 0 ; :: thesis: b1 in {}
reconsider n2 = 8 as Element of NAT ;
A21: x = n2 + 1 by
.= n2 + 1 ;
set w2 = n2;
x = |.(m1 + 5).| by ;
then ( n2 + 1 = m1 + 5 or n2 + 1 = - (m1 + 5) ) by ;
hence x in {} by A5, A8; :: thesis: verum
end;
end;
end;
thus {} c= JUMP ((a,k1) >=0_goto 5) ; :: thesis: verum