for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated Mem-Struct over N
for s being State of S
for p being PartState of S st p +* (Start-At (k,S)) c= s holds
IC s = k