let a be Int_position; for k1 being Integer holds JUMP ((a,k1) <=0_goto 5) = {}
let k1 be Integer; 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 TARSKI:def 3,
XBOOLE_0:def 10 {} c= JUMP ((a,k1) <=0_goto 5)
set nl2 = 8;
set nl1 = 5;
let x be
object ;
( x in JUMP ((a,k1) <=0_goto 5) implies b1 in {} )assume A1:
x in JUMP ((a,k1) <=0_goto 5)
;
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 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 ) )
;
suppose that A10:
s1 . (DataLoc ((s1 . a),k1)) <= 0
and A11:
s2 . (DataLoc ((s2 . a),k1)) <= 0
;
b1 in {} 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 {}
;
verum end;
end;
thus
{} c= JUMP ((a,k1) <=0_goto 5)
; verum