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 Element of 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
set ;
( 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 Element of 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
Object-Kind of
SCMPDS such that A2:
x = IC (Following (ProgramPart s2),s2)
and A3:
IC s2 = 8
and A4:
(ProgramPart s2) /. 8
= a,
k1 >=0_goto 5
;
set l1 = 5;
NIC (a,k1 >=0_goto 5),5
in { (NIC (a,k1 >=0_goto 5),l) where l is Element of 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
Object-Kind of
SCMPDS such that A5:
x = IC (Following (ProgramPart s1),s1)
and A6:
IC s1 = 5
and A7:
(ProgramPart s1) /. 5
= a,
k1 >=0_goto 5
;
consider m2 being
Element of
NAT such that A8:
m2 = IC s2
and A9:
ICplusConst s2,5
= abs (m2 + 5)
by SCMPDS_2:def 20;
consider m1 being
Element of
NAT such that A10:
m1 = IC s1
and A11:
ICplusConst s1,5
= abs (m1 + 5)
by SCMPDS_2:def 20;
Y:
(ProgramPart s2) /. (IC s2) = s2 . (IC s2)
by COMPOS_1:38;
Z:
(ProgramPart s1) /. (IC s1) = s1 . (IC s1)
by COMPOS_1:38;
y:
(ProgramPart s2) . (IC s2) = s2 . (IC s2)
by COMPOS_1:2;
z:
(ProgramPart s1) . (IC s1) = s1 . (IC s1)
by COMPOS_1:2;
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 A12:
s1 . (DataLoc (s1 . a),k1) >= 0
and A13:
s2 . (DataLoc (s2 . a),k1) >= 0
;
b1 in {} A14:
x =
(Exec (a,k1 >=0_goto 5),s2) . (IC SCMPDS )
by A2, A3, A4, Y, y, AMI_1:131
.=
abs (m2 + 5)
by A9, A13, SCMPDS_2:69
;
x =
(Exec (a,k1 >=0_goto 5),s1) . (IC SCMPDS )
by A5, A6, A7, Z, z, AMI_1:131
.=
abs (m1 + 5)
by A11, A12, SCMPDS_2:69
;
then
(
((5 + 2) - 2) + 5
= ((8 + 2) - 2) + 5 or
((5 + 2) - 2) + 5
= - (((8 + 2) - 2) + 5) )
by A6, A10, A3, A8, A14, ABSVALUE:45;
hence
x in {}
;
verum end; suppose that A15:
s1 . (DataLoc (s1 . a),k1) < 0
and A16:
s2 . (DataLoc (s2 . a),k1) < 0
;
b1 in {} A17:
x =
(Exec (a,k1 >=0_goto 5),s2) . (IC SCMPDS )
by A2, A3, A4, Y, y, AMI_1:131
.=
succ 8
by A3, A16, SCMPDS_2:69
;
x =
(Exec (a,k1 >=0_goto 5),s1) . (IC SCMPDS )
by A5, A6, A7, Z, z, AMI_1:131
.=
succ 5
by A6, A15, SCMPDS_2:69
;
hence
x in {}
by A17;
verum end; suppose that A18:
s1 . (DataLoc (s1 . a),k1) < 0
and A19:
s2 . (DataLoc (s2 . a),k1) >= 0
;
b1 in {} reconsider n1 = 5 as
Element of
NAT ;
set w1 =
n1;
A20:
x =
(Exec (a,k1 >=0_goto 5),s2) . (IC SCMPDS )
by A2, A3, A4, Y, y, AMI_1:131
.=
abs (m2 + 5)
by A9, A19, SCMPDS_2:69
;
x =
(Exec (a,k1 >=0_goto 5),s1) . (IC SCMPDS )
by A5, A6, A7, Z, z, AMI_1:131
.=
succ n1
by A6, A18, SCMPDS_2:69
.=
n1 + 1
;
then
(
n1 + 1
= m2 + 5 or
n1 + 1
= - (m2 + 5) )
by A20, ABSVALUE:1;
hence
x in {}
by A3, A8;
verum end; suppose that A21:
s1 . (DataLoc (s1 . a),k1) >= 0
and A22:
s2 . (DataLoc (s2 . a),k1) < 0
;
b1 in {} reconsider n2 = 8 as
Element of
NAT ;
A23:
x =
(Exec (a,k1 >=0_goto 5),s2) . (IC SCMPDS )
by A2, A3, A4, Y, y, AMI_1:131
.=
succ n2
by A3, A22, SCMPDS_2:69
.=
n2 + 1
;
set w2 =
n2;
x =
(Exec (a,k1 >=0_goto 5),s1) . (IC SCMPDS )
by A5, A6, A7, Z, z, AMI_1:131
.=
abs (m1 + 5)
by A11, A21, SCMPDS_2:69
;
then
(
n2 + 1
= m1 + 5 or
n2 + 1
= - (m1 + 5) )
by A23, ABSVALUE:1;
hence
x in {}
by A6, A10;
verum end;
end;
thus
{} c= JUMP (a,k1 >=0_goto 5)
by XBOOLE_1:2; verum