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 Th31;
NAT misses Data-Locations S by Th51;
then A3: dom d misses NAT by A2, XBOOLE_1:63;
dom (Start-At (((IC d) + k),S)) misses NAT by Th26;
then dom (IncrIC (d,k)) misses NAT by A1, A3, XBOOLE_1:70;
hence ProgramPart (IncrIC (d,k)) = {} by RELAT_1:95; :: thesis: verum