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:19;
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, Lm2;
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:23;
set t =
[1,(j + 1)];
set s = the
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 3
.=
[1,(j + 1)]
by ABSVALUE:def 1
;
reconsider t1 =
[1,(j + 1)] as
Int_position by AMI_2:24, SCMPDS_2:3;
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 ) by MEMSTR_0:def 3;
set I =
return a;
reconsider u = the
n -started State of
SCMPDS as
Element of
product the
Object-Kind of
SCMPDS by CARD_3:107;
A7:
IC u = n
by MEMSTR_0:def 8;
set g = (
a,
t1)
--> (
j,
k2);
reconsider v =
u +* ((a,t1) --> (j,k2)) as
Element of
product the
Object-Kind of
SCMPDS by CARD_3:107;
j <> j + 1
;
then A8:
a <> t1
by A4, ZFMISC_1:27;
then A9:
v . a = j
by FUNCT_4:84;
A10:
v . t1 = k2
by A8, FUNCT_4:84;
A11:
dom ((a,t1) --> (j,k2)) = {a,t1}
by FUNCT_4:62;
(
a <> IC &
t1 <> IC )
by SCMPDS_2:43;
then A12:
not
IC in dom ((a,t1) --> (j,k2))
by A11, TARSKI:def 2;
A13:
IC v = l
by A7, A12, FUNCT_4:11;
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 21, SCMPDS_2:58
;
hence
x in y
by A6, A13;
verum end;
hence
x in JUMP (return a)
by SETFAM_1:def 1; verum