let a be Int_position; :: thesis: for l being Element of NAT holds NIC ((),l) = { k where k is Nat : k > 1 }
let l be Element of NAT ; :: thesis: NIC ((),l) = { k where k is Nat : k > 1 }
set s = the State of SCMPDS;
set X = { k where k is Nat : k > 1 } ;
set i = return a;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { k where k is Nat : k > 1 } c= NIC ((),l)
let x be object ; :: thesis: ( x in NIC ((),l) implies x in { k where k is Nat : k > 1 } )
assume x in NIC ((),l) ; :: thesis: x in { k where k is Nat : k > 1 }
then consider s being Element of product such that
A1: x = IC (Exec ((),s)) and
IC s = l ;
reconsider k = x as Element of NAT by A1;
A2: |.(s . (DataLoc ((s . a),1))).| + 2 >= 0 + 2 by XREAL_1:6;
k >= 1 + 1 by ;
then k > 1 by NAT_1:13;
hence x in { k where k is Nat : k > 1 } ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : k > 1 } or x in NIC ((),l) )
set I = return a;
reconsider n = l as Element of NAT ;
assume x in { k where k is Nat : k > 1 } ; :: thesis: x in NIC ((),l)
then consider k being Nat such that
A3: x = k and
A4: k > 1 ;
reconsider k2 = k - 2 as Element of NAT by ;
reconsider u = the n -started State of SCMPDS as Element of product by CARD_3:107;
A5: IC u = n by MEMSTR_0:def 11;
a in SCM-Data-Loc by AMI_2:def 16;
then consider j being Nat such that
A6: a = [1,j] by AMI_2:23;
set t = [1,(j + 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;
A7: DataLoc (j,1) = [1,|.(j + 1).|]
.= [1,(j + 1)] by ABSVALUE:def 1 ;
set g = (a,t1) --> (j,k2);
reconsider v = u +* ((a,t1) --> (j,k2)) as Element of product by CARD_3:107;
A8: dom ((a,t1) --> (j,k2)) = {a,[1,(j + 1)]} by FUNCT_4:62;
j <> j + 1 ;
then A9: a <> [1,(j + 1)] by ;
then A10: v . a = j by FUNCT_4:84;
( a <> IC & t1 <> IC ) by SCMPDS_2:43;
then A11: not IC in dom ((a,t1) --> (j,k2)) by ;
A12: IC v = l by ;
A13: v . [1,(j + 1)] = k2 by ;
x = k2 + 2 by A3
.= |.(v . (DataLoc (j,1))).| + 2 by
.= IC (Exec ((),v)) by ;
hence x in NIC ((),l) by A12; :: thesis: verum