let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for k being Element of NAT
for d being data-only PartState of S holds ProgramPart (IncrIC d,k) = {}
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for k being Element of NAT
for d being data-only PartState of S holds ProgramPart (IncrIC d,k) = {}
let k be Element of NAT ; :: thesis: for d being data-only PartState of S holds ProgramPart (IncrIC d,k) = {}
let d be data-only PartState of S; :: thesis: ProgramPart (IncrIC d,k) = {}
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 Th139;
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 Th134;
then dom (IncrIC d,k) misses NAT by A1, A3, XBOOLE_1:70;
hence ProgramPart (IncrIC d,k) = {} by RELAT_1:95; :: thesis: verum