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 AMI_1:def 11;
reconsider I =
return a as
Element of the
Object-Kind of
SCMPDS . l by AMI_1:def 14;
X:
((IC SCMPDS ) .--> il1) +* (l .--> (return a)) is the
Object-Kind of
SCMPDS -compatible PartState of
SCMPDS
;
(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 X, PBOOLE:155;
A7:
u . (IC SCMPDS ) =
IC u
by AMI_1:def 15
.=
n
by AMI_1:129
;
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;
(
l <> a &
l <> t1 )
by SCMPDS_2:53;
then
(
u . n = return a & not
n in dom (a,t1 --> j,k2) )
by A11, AMI_1:129, TARSKI:def 2;
then A12:
v . l = return a
by FUNCT_4:12;
(
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 =
v . (IC SCMPDS )
by AMI_1:def 15
.=
l
by A7, A13, FUNCT_4:12
;
X:
(ProgramPart v) /. (IC v) = v . (IC v)
by AMI_1:150;
x =
k2 + 2
by A2
.=
(abs (v . (DataLoc j,1))) + 2
by A10, A5, ABSVALUE:def 1
.=
(Exec (return a),v) . (IC SCMPDS )
by A9, SCMPDS_1:def 23, SCMPDS_2:70
.=
IC (Following (ProgramPart v),v)
by A12, A14, AMI_1:131
;
hence
x in y
by A6, A12, A14, X;
verum end;
hence
x in JUMP (return a)
by SETFAM_1:def 1; verum