let a be Int_position; :: thesis: for l being Element of NAT holds NIC ((return a),l) = { k where k is Nat : k > 1 }

let l be Element of NAT ; :: thesis: NIC ((return a),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;

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 ((return a),l)

then consider k being Nat such that

A3: x = k and

A4: k > 1 ;

reconsider k2 = k - 2 as Element of NAT by A4, Lm2;

reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) 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 (the_Values_of SCMPDS) 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 A6, XTUPLE_0:1;

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 A8, TARSKI:def 2;

A12: IC v = l by A5, A11, FUNCT_4:11;

A13: v . [1,(j + 1)] = k2 by A9, FUNCT_4:84;

x = k2 + 2 by A3

.= |.(v . (DataLoc (j,1))).| + 2 by A13, A7, ABSVALUE:def 1

.= IC (Exec ((return a),v)) by A10, SCMPDS_2:58, SCMPDS_I:def 14 ;

hence x in NIC ((return a),l) by A12; :: thesis: verum

let l be Element of NAT ; :: thesis: NIC ((return a),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 ((return a),l)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Nat : k > 1 } or x in NIC ((return a),l) )let x be object ; :: thesis: ( x in NIC ((return a),l) implies x in { k where k is Nat : k > 1 } )

assume x in NIC ((return a),l) ; :: thesis: x in { k where k is Nat : k > 1 }

then consider s being Element of product (the_Values_of SCMPDS) such that

A1: x = IC (Exec ((return a),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 A2, A1, SCMPDS_2:58, SCMPDS_I:def 14;

then k > 1 by NAT_1:13;

hence x in { k where k is Nat : k > 1 } ; :: thesis: verum

end;assume x in NIC ((return a),l) ; :: thesis: x in { k where k is Nat : k > 1 }

then consider s being Element of product (the_Values_of SCMPDS) such that

A1: x = IC (Exec ((return a),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 A2, A1, SCMPDS_2:58, SCMPDS_I:def 14;

then k > 1 by NAT_1:13;

hence x in { k where k is Nat : k > 1 } ; :: thesis: verum

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 ((return a),l)

then consider k being Nat such that

A3: x = k and

A4: k > 1 ;

reconsider k2 = k - 2 as Element of NAT by A4, Lm2;

reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) 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 (the_Values_of SCMPDS) 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 A6, XTUPLE_0:1;

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 A8, TARSKI:def 2;

A12: IC v = l by A5, A11, FUNCT_4:11;

A13: v . [1,(j + 1)] = k2 by A9, FUNCT_4:84;

x = k2 + 2 by A3

.= |.(v . (DataLoc (j,1))).| + 2 by A13, A7, ABSVALUE:def 1

.= IC (Exec ((return a),v)) by A10, SCMPDS_2:58, SCMPDS_I:def 14 ;

hence x in NIC ((return a),l) by A12; :: thesis: verum