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 p being program-free PartState of S
for k being Element of NAT holds ProgramPart (IncrIC (p,k)) = {}
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for p being program-free PartState of S
for k being Element of NAT holds ProgramPart (IncrIC (p,k)) = {}
let p be program-free PartState of S; :: thesis: for k being Element of NAT holds ProgramPart (IncrIC (p,k)) = {}
let k be Element of NAT ; :: thesis: ProgramPart (IncrIC (p,k)) = {}
thus ProgramPart (IncrIC (p,k)) = (ProgramPart p) +* (ProgramPart (Start-At (((IC p) + k),S))) by FUNCT_4:75
.= (ProgramPart p) +* {} by Th135
.= ProgramPart p by FUNCT_4:22
.= {} by Def29 ; :: thesis: verum