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 Instruction-Location of SCMPDS : verum } ;
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: {} c= JUMP (a,k1 <=0_goto 5)
let x be
set ;
:: 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 nl1 = 5;
set nl2 = 8;
set l1 =
inspos 5;
NIC (a,k1 <=0_goto 5),
(inspos 5) in { (NIC (a,k1 <=0_goto 5),l) where l is Instruction-Location of SCMPDS : verum }
;
then
x in NIC (a,k1 <=0_goto 5),
(inspos 5)
by A1, SETFAM_1:def 1;
then consider s1 being
State of
SCMPDS such that A2:
x = IC (Following s1)
and A3:
IC s1 = inspos 5
and A4:
s1 . (inspos 5) = a,
k1 <=0_goto 5
;
consider m1 being
Element of
NAT such that A5:
m1 = IC s1
and A6:
ICplusConst s1,5
= abs (m1 + 5)
by SCMPDS_2:def 20;
A7:
m1 = 5
by A3, A5;
set l2 =
inspos 8;
NIC (a,k1 <=0_goto 5),
(inspos 8) in { (NIC (a,k1 <=0_goto 5),l) where l is Instruction-Location of SCMPDS : verum }
;
then
x in NIC (a,k1 <=0_goto 5),
(inspos 8)
by A1, SETFAM_1:def 1;
then consider s2 being
State of
SCMPDS such that A8:
x = IC (Following s2)
and A9:
IC s2 = inspos 8
and A10:
s2 . (inspos 8) = a,
k1 <=0_goto 5
;
consider m2 being
Element of
NAT such that A11:
m2 = IC s2
and A12:
ICplusConst s2,5
= abs (m2 + 5)
by SCMPDS_2:def 20;
A13:
m2 = 8
by A9, A11;
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 A14:
s1 . (DataLoc (s1 . a),k1) <= 0
and A15:
s2 . (DataLoc (s2 . a),k1) <= 0
;
:: thesis: b1 in {} A16:
x =
(Exec (a,k1 <=0_goto 5),s1) . (IC SCMPDS )
by A2, A3, A4, AMI_1:131
.=
abs (m1 + 5)
by A6, A14, SCMPDS_2:68
;
x =
(Exec (a,k1 <=0_goto 5),s2) . (IC SCMPDS )
by A8, A9, A10, AMI_1:131
.=
abs (m2 + 5)
by A12, A15, SCMPDS_2:68
;
then
( 5
+ 5
= 8
+ 5 or 5
+ 5
= - (8 + 5) )
by A7, A13, A16, ABSVALUE:45;
hence
x in {}
;
:: thesis: verum end; suppose that A17:
s1 . (DataLoc (s1 . a),k1) > 0
and A18:
s2 . (DataLoc (s2 . a),k1) > 0
;
:: thesis: b1 in {} A19:
x =
(Exec (a,k1 <=0_goto 5),s1) . (IC SCMPDS )
by A2, A3, A4, AMI_1:131
.=
Next (inspos 5)
by A3, A17, SCMPDS_2:68
;
x =
(Exec (a,k1 <=0_goto 5),s2) . (IC SCMPDS )
by A8, A9, A10, AMI_1:131
.=
Next (inspos 8)
by A9, A18, SCMPDS_2:68
;
hence
x in {}
by A19;
:: thesis: verum end; suppose that A20:
s1 . (DataLoc (s1 . a),k1) > 0
and A21:
s2 . (DataLoc (s2 . a),k1) <= 0
;
:: thesis: b1 in {} reconsider n1 =
inspos 5 as
Element of
NAT ;
set w1 =
n1;
A24:
x =
(Exec (a,k1 <=0_goto 5),s1) . (IC SCMPDS )
by A2, A3, A4, AMI_1:131
.=
succ n1
by A3, A20, SCMPDS_2:68
.=
n1 + 1
;
x =
(Exec (a,k1 <=0_goto 5),s2) . (IC SCMPDS )
by A8, A9, A10, AMI_1:131
.=
abs (m2 + 5)
by A12, A21, SCMPDS_2:68
;
then
(
n1 + 1
= m2 + 5 or
n1 + 1
= - (m2 + 5) )
by A24, ABSVALUE:1;
hence
x in {}
by A13;
:: thesis: verum end; suppose that A25:
s1 . (DataLoc (s1 . a),k1) <= 0
and A26:
s2 . (DataLoc (s2 . a),k1) > 0
;
:: thesis: b1 in {} reconsider n2 =
inspos 8 as
Element of
NAT ;
set w2 =
n2;
A29:
x =
(Exec (a,k1 <=0_goto 5),s1) . (IC SCMPDS )
by A2, A3, A4, AMI_1:131
.=
abs (m1 + 5)
by A6, A25, SCMPDS_2:68
;
x =
(Exec (a,k1 <=0_goto 5),s2) . (IC SCMPDS )
by A8, A9, A10, AMI_1:131
.=
succ n2
by A9, A26, SCMPDS_2:68
.=
n2 + 1
;
then
(
n2 + 1
= m1 + 5 or
n2 + 1
= - (m1 + 5) )
by A29, ABSVALUE:1;
hence
x in {}
by A7;
:: thesis: verum end;
end;
thus
{} c= JUMP (a,k1 <=0_goto 5)
by XBOOLE_1:2; :: thesis: verum