let a be Int_position ; JUMP (return a) = { k where k is Element of NAT : k > 1 }
set A = { k where k is Element of NAT : k > 1 } ;
set i = return a;
set X = { (NIC ((return a),l)) where l is Element of NAT : verum } ;
JUMP (return a) c= NIC ((return a),0)
by AMISTD_1:58;
hence
JUMP (return a) c= { k where k is Element of NAT : k > 1 }
by Th10; XBOOLE_0:def 10 { k where k is Element of NAT : k > 1 } c= JUMP (return a)
let x be set ; TARSKI:def 3 ( not x in { k where k is Element of NAT : k > 1 } or x in JUMP (return a) )
assume A1:
x in { k where k is Element of NAT : k > 1 }
; x in JUMP (return a)
now consider k being
Element of
NAT such that A2:
x = k
and A3:
k > 1
by A1;
reconsider k2 =
k - 2 as
Element of
NAT by A3, Lm1;
NIC (
(return a),
0)
in { (NIC ((return a),l)) where l is Element of NAT : verum }
;
hence
{ (NIC ((return a),l)) where l is Element of NAT : verum } <> {}
;
for y being set st y in { (NIC ((return a),l)) where l is Element of NAT : verum } holds
x in y
a in SCM-Data-Loc
by SCMPDS_2:def 2;
then consider j being
Element of
NAT such that A4:
a = [1,j]
by AMI_2:32;
set t =
[1,(j + 1)];
consider s being
State of
SCMPDS;
let y be
set ;
( y in { (NIC ((return a),l)) where l is Element of NAT : verum } implies x in y )A5:
DataLoc (
j,1) =
[1,(abs (j + 1))]
by SCMPDS_2:def 4
.=
[1,(j + 1)]
by ABSVALUE:def 1
;
reconsider t1 =
[1,(j + 1)] as
Int_position by AMI_2:33, SCMPDS_2:9;
assume
y in { (NIC ((return a),l)) where l is Element of NAT : verum }
;
x in ythen consider l being
Element of
NAT such that A6:
y = NIC (
(return a),
l)
;
reconsider n =
l as
Element of
NAT ;
reconsider il1 =
l as
Element of
ObjectKind (IC SCMPDS) by COMPOS_1:def 6;
reconsider I =
return a as
Element of the
Object-Kind of
SCMPDS . l by COMPOS_1:def 8;
(
(IC SCMPDS),
l)
--> (
il1,
I)
= ((IC SCMPDS) .--> il1) +* (l .--> I)
by FUNCT_4:def 4;
then reconsider u =
s +* (((IC SCMPDS),l) --> (il1,(return a))) as
Element of
product the
Object-Kind of
SCMPDS by PBOOLE:155;
A7:
u . (IC SCMPDS) =
IC u
.=
n
by EXTPRO_1:26
;
set g = (
a,
t1)
--> (
j,
k2);
reconsider v =
u +* ((a,t1) --> (j,k2)) as
Element of
product the
Object-Kind of
SCMPDS by PBOOLE:155;
j <> j + 1
;
then A8:
a <> t1
by A4, ZFMISC_1:33;
then A9:
v . a = j
by FUNCT_4:89;
A10:
v . t1 = k2
by A8, FUNCT_4:89;
A11:
dom ((a,t1) --> (j,k2)) = {a,t1}
by FUNCT_4:65;
(
a <> IC SCMPDS &
t1 <> IC SCMPDS )
by SCMPDS_2:52;
then A13:
not
IC SCMPDS in dom ((a,t1) --> (j,k2))
by A11, TARSKI:def 2;
A14:
IC v = l
by A7, A13, FUNCT_4:12;
x =
k2 + 2
by A2
.=
(abs (v . (DataLoc (j,1)))) + 2
by A10, A5, ABSVALUE:def 1
.=
IC (Exec ((return a),v))
by A9, SCMPDS_1:def 23, SCMPDS_2:70
;
hence
x in y
by A6, A14;
verum end;
hence
x in JUMP (return a)
by SETFAM_1:def 1; verum