let a be Int_position; JUMP (return a) = { k where k is Nat : k > 1 }
set A = { k where k is Nat : k > 1 } ;
set i = return a;
set X = { (NIC ((return a),l)) where l is Nat : verum } ;
JUMP (return a) c= NIC ((return a),0)
by AMISTD_1:19;
hence
JUMP (return a) c= { k where k is Nat : k > 1 }
by Th4; XBOOLE_0:def 10 { k where k is Nat : k > 1 } c= JUMP (return a)
let x be object ; TARSKI:def 3 ( not x in { k where k is Nat : k > 1 } or x in JUMP (return a) )
assume A1:
x in { k where k is Nat : k > 1 }
; x in JUMP (return a)
now ( { (NIC ((return a),l)) where l is Nat : verum } <> {} & ( for y being set st y in { (NIC ((return a),l)) where l is Nat : verum } holds
x in y ) )consider k being
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 Nat : verum }
;
hence
{ (NIC ((return a),l)) where l is Nat : verum } <> {}
;
for y being set st y in { (NIC ((return a),l)) where l is Nat : verum } holds
x in y
a in SCM-Data-Loc
by AMI_2:def 16;
then consider j being
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 Nat : verum } implies x in y )A5:
DataLoc (
j,1) =
[1,|.(j + 1).|]
.=
[1,(j + 1)]
by ABSVALUE:def 1
;
[1,(j + 1)] in SCM-Data-Loc
by AMI_2:24;
then reconsider t1 =
[1,(j + 1)] as
Int_position by AMI_2:def 16;
assume
y in { (NIC ((return a),l)) where l is Nat : verum }
;
x in ythen consider l being
Nat such that A6:
y = NIC (
(return a),
l)
;
reconsider n =
l as
Element of
NAT by ORDINAL1:def 12;
set I =
return a;
reconsider u = the
n -started State of
SCMPDS as
Element of
product (the_Values_of SCMPDS) by CARD_3:107;
A7:
IC u = n
by MEMSTR_0:def 11;
set g = (
a,
t1)
--> (
j,
k2);
reconsider v =
u +* ((a,t1) --> (j,k2)) as
Element of
product (the_Values_of SCMPDS) by CARD_3:107;
j <> j + 1
;
then A8:
a <> t1
by A4, XTUPLE_0:1;
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
.=
|.(v . (DataLoc (j,1))).| + 2
by A10, A5, ABSVALUE:def 1
.=
IC (Exec ((return a),v))
by A9, SCMPDS_2:58, SCMPDS_I:def 14
;
hence
x in y
by A6, A13;
verum end;
hence
x in JUMP (return a)
by SETFAM_1:def 1; verum