let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N
for k being Element of NAT
for d being data-only FinPartState of S holds (IncrIC d,k) | NAT = {}
let S be non empty stored-program halting IC-Ins-separated definite realistic AMI-Struct of N; :: thesis: for k being Element of NAT
for d being data-only FinPartState of S holds (IncrIC d,k) | NAT = {}
let k be Element of NAT ; :: thesis: for d being data-only FinPartState of S holds (IncrIC d,k) | NAT = {}
let d be data-only FinPartState of S; :: thesis: (IncrIC d,k) | NAT = {}
A1: dom (IncrIC d,k) = (dom d) \/ (dom (Start-At ((IC d) + k),S)) by FUNCT_4:def 1;
A2: dom d c= Data-Locations S by AMI_1:139;
NAT misses Data-Locations S by Th15;
then A3: dom d misses NAT by A2, XBOOLE_1:63;
dom (Start-At ((IC d) + k),S) misses NAT by AMI_1:134;
then dom (IncrIC d,k) misses NAT by A1, A3, XBOOLE_1:70;
hence (IncrIC d,k) | NAT = {} by RELAT_1:95; :: thesis: verum